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 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)
Additional Information:	The original publication is available at http://www.springerlink.com
Related URLs:	Publisher
Divisions:	Faculty of Engineering and Physical Sciences > Computing Science
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