Abstract
The version of Kerberos presented by Burrows et al. [5] is fully mechanised using the Inductive Method. Two models are presented, allowing respectively the leak of any session keys, and of expired session keys. Thanks to timestamping, the protocol provides the involved parties with strong guarantees in a realistically hostile environment. These guarantees are supported by the generic theorem prover Isabelle.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
G. Bella, L. C. Paulson. Using Isabelle to Prove Properties of the Kerberos Authentication System. In Proc. of Workshop on Design and Formal Verification of Security Protocols, Orman and Meadows (eds.), DIMACS, 1997.
S. M. Bellovin, M. Merritt. Limitations of the Kerberos authentication system. Computer Comm. Review, 20(5), 119–132, 1990.
D. Bolignano. Towards a Mechanization of Cryptographic Protocol Verification. In Proc. of Conference on Computer Aided Verification, Springer Verlag, 1997.
S. H. Brackin. A HOL Extension of GNY for Automatically Analyzing Cryptographic Protocols. In Proc. of Computer Security Foundations Workshop, IEEE Press, 1996.
M. Burrows, M. Abadi, R. M. Needham. A logic of authentication. Proceedings of the Royal Society of London, 426:233–271, 1989.
G. Lowe. Breaking and Fixing the Needham-Schroeder Pubfic-Key Protocol using FDR. In Tools and Algorithms for the Construction and Analysis of Systems, Margaria and Steffen (eds.), LNCS1055, Springer Verlag, 147–166, 1996.
G. Lowe. Casper: a Compiler for the Analysis of Security Protocols. Oxford University, Computing Laboratory, Technical Report, 1996.
C. Meadows. The NRL Protocol Analyzer: An Overview. Journal of Logic Programming, 26(2), 113–131, 1996.
J. C. Mitchell, M. Mitchell, U. Stern: Automated Analysis of Cryptographic Protocols Using Murphi. In Proc. of Symposium on Security and Privacy, IEEE Press, 1997.
R. M. Needham, M. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12), 993–999, 1978.
L. C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. LNCS 828.
L. C. Paulson. Proving properties of security protocols by induction. In Proc. of Computer Security Foundations Workshop, IEEE Press, 1997.
L. C. Paulson. Mechanized proofs for a recursive authentication protocol. In Proc. of Computer Security Foundations Workshop, IEEE Press, 1997.
L. C. Paulson. On Two Formal Analyses of the Yahalom Protocol. Cambridge University, Computer Laboratory, Technical Report No. 432, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bella, G., Paulson, L.C. (1998). Mechanising BAN Kerberos by the inductive method. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028763
Download citation
DOI: https://doi.org/10.1007/BFb0028763
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive