Using a PVS Embedding of CSP to Verify Authentication Protocols.
Tools
Tools
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.
![[img]](/style/images/fileicons/application_pdf.png)
| PDF - Accepted Version Available under License : See the attached licence file. 232Kb | |
![[img]](/style/images/fileicons/text_plain.png) | Plain Text (licence) 1516b |
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) |
|---|---|
| Additional Information: | The original publication is available at http://www.springerlink.com |
| Divisions: | Faculty of Engineering and Physical Sciences > Computing Science |
| Related URLs: | |
| ID Code: | 7228 |
| Deposited By: | Symplectic Elements |
| Deposited On: | 12 Jan 2012 13:20 |
| Last Modified: | 16 Feb 2013 16:10 |
Document Downloads
Repository Staff Only: item control page