Abstract
This paper details an approach to verifying time dependent authentication properties of security protocols. We discuss the introduction of time into the Communicating Sequential Processes (CSP) protocol verification framework of [11]. The embedding of CSP in the theorem prover PVS (Prototype Verification System) is extended to incorporate event-based time, retaining the use of the existing rank function approach to verify such properties. An example analysis is demonstrated using the Wide-Mouthed Frog protocol.
Chapter PDF
Similar content being viewed by others
References
Bella, G., Paulson, L.C.: Using Isabelle to prove properties of the kerberos authentication system. In: DIMACS Workshop on Design and Formal Verification of Security Protocols (1997)
Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Transactions on Computer Systems 8 (1989)
Clark, J., Jacob, J.: On the security of recent protocols. Information Processing Letters 56(3), 151–155 (1995)
Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2) (1983)
Dutertre, B., Schneider, S.: Embedding CSP in PVS. an application to authentication protocols. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275. Springer, Heidelberg (1997)
Lowe, G.: Casper: A compiler for the analysis of security protocols. In: Proceedings of the 10th IEEE Computer Security Foundations Workshop (1997)
Meadows, C.: Language generation and verification in the NRL Protocol Analyzer. In: Proceedings of the 10th IEEE Computer Security Foundations Workshop (1996)
Meadows, C.: Personal communication (2000)
Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Paulson, L.C.: Isabelle: A Generic Theorem Prover. Springer, Heidelberg (1994)
Schneider, S.A.: Verifying authentication protocols in CSP. IEEE Transactions on Software Engineering (1998)
Schneider, S.A.: Timewise refinement for communicating processes. Science of Computer Programming 28 (1997)
Schneider, S.A.: Concurrent and Real-time Systems. Wiley, Chichester (1999)
Thayer, J., Herzog, J.C., Guttman, J.D.: Strand spaces: Proving security protocols correct. Journal of Computer Security (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Evans, N., Schneider, S. (2000). Analysing Time Dependent Security Properties in CSP Using PVS. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds) Computer Security - ESORICS 2000. ESORICS 2000. Lecture Notes in Computer Science, vol 1895. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10722599_14
Download citation
DOI: https://doi.org/10.1007/10722599_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41031-7
Online ISBN: 978-3-540-45299-7
eBook Packages: Springer Book Archive