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	Text tphols97.pdf - Accepted version Manuscript Available under License : See the attached licence file. Download (237kB)
	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 :	Name Email ORCID Dutertre, B Schneider, S
Date :	1997
Identification Number :	10.1007/BFb0028390
Contributors :	Contribution Name Email ORCID http://www.loc.gov/loc.terms/relators/EDT Gunter, EL http://www.loc.gov/loc.terms/relators/EDT Felty, AP http://www.loc.gov/loc.terms/relators/PBL Springer,
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 :	31 Oct 2017 14:09
URI:	http://epubs.surrey.ac.uk/id/eprint/7228

Actions (login required)

View Item

Downloads