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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. H. Brackin. Deciding Cryptographic Protocol Adequacy with HOL: The Implementation. In TPHOLs'96. Springer-Verlag, LNCS 1125, 1996.
J. Bryans and S. Schneider. Mechanical Verification of the full Needham-Schroeder public key protocol. Technical report, Royal Holloway, University of London, 1997.
M. Burrows, M, Abadi, and R. Needham. A Logic of Authentication. Technical Report 39, Digital Equipment Corporation, System Research Center, 1989.
A. J. Camilleri. Mechanizing CSP trace theory in higher order logic. IEEE Transactions on Software Engineering, 16(9):993–1004, 1990.
J. Crow, S. Owre, 1 Rushby, N. Shankar, and M. Srivas. A tutorial introduction to PVS. In Workshop on Industrial-Strength Formal Specification Techniques, 1995.
B. Dutertre and S. Schneider. Embedding CSP in PVS. An Application to Authentication Protocols. Technical report, Royal Holloway, CSD-TR-97-12.
C. A R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.
R. Kemmerer, C. Meadows, and Millen J. Three systems for cryptographic analysis. Journal of Cryptology, 7(2), 1994.
G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. In Proc. of TACAS'96. Springer-Verlag, LNCS 1055, 1996.
R. M. Needham and M. D. Schroeder. Using Encryption for Authentication in Large Networks of Computers. Comm. of the ACM, 21(12):990–999, 1978.
S. Owre, N. Shankar, and J. M. Rushby. The PVS Specification Language. Computer Science Lab., SRI International, 1993.
L. Paulson. Proving Properties of Security Protocols by Induction. Technical Report TR409, Computer Laboratory, University of Cambridge, 1996.
S. Schneider. Security Properties and CSP. In IEEE Symposium on Security and Privacy, 1996.
S. Schneider. Using CSP for protocol analysis: the Needham-Schroeder Public Key Protocol. Technical Report CSD-TR-96-14, Royal Holloway, 1996..
J. U. Skakkebask and N. Shankar. Towards a duration calculus proof assistant in PVS. In Formal Techniques in Real-Time and Fault-Tolerant Systems. Springer-Verlag, LNCS 863, September 1994.
P. Syverson and P. van Oorschot. On Unifying Some Cryptographic Protocol Logics. In Proc. of the 19N IEEE 4M. on Research in Security and Privacy, 1994.
F. J. Thayer. An approach to process algebra using mWs. Technical Report MP-94B193, The mitre Corporation, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dutertre, B., Schneider, S. (1997). Using a PVS embedding of CSP to verify authentication protocols. In: Gunter, E.L., Felty, A. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1997. Lecture Notes in Computer Science, vol 1275. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028390
Download citation
DOI: https://doi.org/10.1007/BFb0028390
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63379-2
Online ISBN: 978-3-540-69526-4
eBook Packages: Springer Book Archive