Abstract
We present results from a recent project analyzing Kerberos 5. The main expected properties of this protocol, namely confidentiality and authentication, hold throughout the protocol. Our analysis also highlights a number of behaviors that do not follow the script of the protocol, although they do not appear harmful for the principals involved. We obtained these results by formalizing Kerberos 5 at two levels of detail in the multiset rewriting formalism MSR and by adapting an inductive proof methodology pioneered by Schneider. Our more detailed specification takes into account encryption types, flags and options, error messages, and a few timestamps.
Scedrov, Butler, and Jaggard were partially supported by the DoD University Research Initiative (URI) program administered by the Office of Naval Research under Grant N00014-01-1-0795, and by NSF Grant CCR-0098096. Cervesato was partially supported by NRL under contract N00173-00-C-2086. This paper was written while Cervesato was visiting Princeton University.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Kohl, J., Neuman, C.: The Kerberos Network Authentication Service (V5) (1993) Network Working Group Request for Comments: 1510
Neuman, B.C., Ts’o, T.: Kerberos: An Authentication Service for Computer Networks. IEEE Communications 32, 33–38 (1994)
Neuman, C., Kohl, J., Ts’o, T., Raeburn, K., Yu, T.: The Kerberos Network Authentication Service (V5) (2001) Internet draft (expires May 20, 2002)
Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: A Formal Analysis of Some Properties of Kerberos 5 Using MSR. In: Proceedings of the 15th Computer Security Foundations Workshop, pp. 175–190. IEEE Computer Society Press, Los Alamitos (2002)
Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: A formal analysis of some properties of kerberos 5 using MSR. Technical Report CIS-MS-04-04, University of Pennsylvania, Department of Computer and Information Science, p. 59 (2004), Available from: ftp://ftp.cis.upenn.edu/pub/papers/scedrov/ms-cis-04-04.pdf/ps
Bella, G., Riccobene, E.: Formal Analysis of the Kerberos Authentication System. J. Universal Comp. Sci. 3, 1337–1381 (1997)
Bella, G.: Inductive Verification of Cryptographic Protocols. PhD thesis, University of Cambridge (2000)
Bella, G., Paulson, L.C.: Using Isabelle to Prove Properties of the Kerberos Authentication System. In: Orman, H., Meadows, C. (eds.) Proc. of DIMACS 1997, Workshop on Design and Formal Verification of Security Protocols (CD-ROM) (1997)
Bella, G., Paulson, L.C.: Kerberos Version IV: Inductive Analysis of the Secrecy Goals. In: Quisquater, J.-J., Deswarte, Y., Meadows, C., Gollmann, D. (eds.) ESORICS 1998. LNCS, vol. 1485, pp. 361–375. Springer, Heidelberg (1998)
Bella, G., Paulson, L.C.: Mechanising BAN Kerberos by the Inductive Method. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427. Springer, Heidelberg (1998)
Mitchell, J.C., Mitchell, M., Stern, U.: Automated Analysis of Cryptographic Protocols Using Murϕ. In: Proc. of the IEEE Symposium on Security and Privacy, pp. 141–153. IEEE Computer Society Press, Los Alamitos (1997)
Cervesato, I., Durgin, N.A., Lincoln, P., Mitchell, J., Scedrov, A.: A Meta-notation for Protocol Analysis. In: Proc. of the Twelfth IEEE Computer Security Foundations Workshop, pp. 55–69 (1999)
Cervesato, I.: Typed Multiset Rewriting Specifications of Security Protocols. In: Proc. of the First Irish Conference on the Mathematical Foundations of Computer Science and Information Technology–MFCSIT 2000. Elsevier ENTCS 40 (2000)
Cervesato, I.: Typed MSR: Syntax and Examples. In: Proc. of the First International Workshop on Mathematical Methods, Models and Architectures for Computer Network Security — MMM 2001. Springer, Heidelberg (2001), St. Petersburg, Russia, 21–23 May 2001
Durgin, N.A., Lincoln, P.D., Mitchell, J.C., Scedrov, A.: Multiset Rewriting and the Complexity of Bounded Security Protocols, pages 63 (2002) (manuscript)
Schneider, S.: Verifying Authentication Protocols in CSP. IEEE Transactions on Software Engineering 24, 741–758 (1998)
Neuman, C.: Personal communication (2002)
Neuman, C., Yu, T., Hartman, S., Raeburn, K.: The Kerberos Network Authentication Service (V5) (2004) Internet draft (expires August 15, 2004), http://www.ietf.org/internet-drafts/draft-ietf-krb-wg-kerberos-clarifications-05.txt
Jeffrey, A.: Personal communication (2002)
Raeburn, K.: Personal communication (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A. (2004). Verifying Confidentiality and Authentication in Kerberos 5. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds) Software Security - Theories and Systems. ISSS 2003. Lecture Notes in Computer Science, vol 3233. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-37621-7_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-37621-7_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23635-1
Online ISBN: 978-3-540-37621-7
eBook Packages: Springer Book Archive