Using a PVS Embedding of CSP to Verify Authentication Protocols.
Tools
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.
![]()
|
Text
tphols97.pdf - Accepted version Manuscript Available under License : See the attached licence file. Download (237kB) |
|
![]() |
Text (licence)
licence.txt Download (1kB) |
Official URL: http://dx.doi.org/10.1007/BFb0028390
Abstract
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 : |
|
||||||||||||||||
Related URLs : | |||||||||||||||||
Additional Information : | The original publication is available at http://www.springerlink.com | ||||||||||||||||
Depositing User : | Symplectic Elements | ||||||||||||||||
Date Deposited : | 12 Jan 2012 13:20 | ||||||||||||||||
Last Modified : | 06 Jul 2019 05:08 | ||||||||||||||||
URI: | http://epubs.surrey.ac.uk/id/eprint/7228 |
Actions (login required)
![]() |
View Item |
Downloads
Downloads per month over past year