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.

Preview	PDF tphols97.pdf - Accepted version Manuscript Available under License : See the attached licence file. Download (237kB)
	Plain Text (licence) licence.txt Download (1kB)

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 > Computing Science
Authors :	Authors Email ORCID Dutertre, B UNSPECIFIED UNSPECIFIED Schneider, S UNSPECIFIED UNSPECIFIED
Date :	1997
Identification Number :	10.1007/BFb0028390
Contributors :	Contribution Name Email ORCID Editor Gunter, EL UNSPECIFIED UNSPECIFIED Editor Felty, AP UNSPECIFIED UNSPECIFIED Publisher Springer, UNSPECIFIED UNSPECIFIED
Related URLs :	Publisher
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 :	23 Sep 2013 18:45
URI:	http://epubs.surrey.ac.uk/id/eprint/7228

Actions (login required)

View Item

Downloads