University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Using a PVS Embedding of CSP to Verify Authentication Protocols.

Dutertre, B and Schneider, S (1997) Using a PVS Embedding of CSP to Verify Authentication Protocols. In: 10th International Conference on Theorem Proving in Higher Order Logics, 1997-08-19 - 1997-08-22, Murray Hill, NJ, USA.

tphols97.pdf - Accepted version Manuscript
Available under License : See the attached licence file.

Download (237kB)
[img] Text (licence)

Download (1kB)


This paper presents an application of PVS to the verification of security protocols. The objective is to provide mechanical support for a verification method described in [14]. The PVS formalization consists of a semantic embedding of CSP and of a collection of theorems and proof rules for reasoning about authentication properties. We present an application to the Needham-Schroeder public key protocol.

Item Type: Conference or Workshop Item (UNSPECIFIED)
Divisions : Faculty of Engineering and Physical Sciences > Computer Science
Authors : Dutertre, B and Schneider, S
Date : 1997
DOI : 10.1007/BFb0028390
Contributors :
ContributionNameEmailORCID, EL, AP,
Related URLs :
Additional Information : The original publication is available at
Depositing User : Symplectic Elements
Date Deposited : 12 Jan 2012 13:20
Last Modified : 06 Jul 2019 05:08

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800