Using a PVS Embedding of CSP to Verify Authentication Protocols.

B Dutertre; S Schneider

doi:10.1007/BFb0028390

Back

Using a PVS Embedding of CSP to Verify Authentication Protocols.

Conference presentation

Open access

Peer reviewed

Using a PVS Embedding of CSP to Verify Authentication Protocols.

B Dutertre and S Schneider

Lecture Notes in Computer Science, Vol.1275, pp.121-136

10th International Conference on Theorem Proving in Higher Order Logics (Murray Hill, NJ, USA, 19/08/1997 - 22/08/1997)

1997

DOI: https://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.

Files and links (3)

pdf

tphols97232.11 kBDownload View

TextSRIDA, Open Access

url

http://dx.doi.org/10.1007/BFb0028390View

Published (Version of record)

url

http://dx.doi.org/10.1007/BFb0028390View

Metrics

258 File views/ downloads

18 Record Views

Details

Title: Using a PVS Embedding of CSP to Verify Authentication Protocols.
Creators: B Dutertre
S Schneider
Contributors: EL Gunter
AP Felty
Springer (null)
Publication Details: Lecture Notes in Computer Science, Vol.1275, pp.121-136
Conference: 10th International Conference on Theorem Proving in Higher Order Logics (Murray Hill, NJ, USA, 19/08/1997 - 22/08/1997)
Date published: 1997
Date submitted: 20/08/2011
Identifiers: 99512349302346
Academic Unit: Department of Computer Science
Resource Type: Conference presentation

Using a PVS Embedding of CSP to Verify Authentication Protocols.

Abstract

Files and links (3)

Metrics

Details

Usage Policy