Specifying Kerberos 5 cross-realm authentication

ABSTRACT

Cross-realm authentication is a useful and interesting component of Kerberos aimed at enabling secure access to services astride organizational boundaries. We present a formalization of Kerberos 5 cross-realm authentication in MSR, a specification language based on multiset rewriting. We also adapt the Dolev-Yao intruder model to the cross-realm setting and prove an important property for a critical field in a cross-realm ticket. Finally, we document several failures of authentication and confidentiality in the presence of compromised intermediate realms. Although the current Kerberos specifications disclaim responsibility for these vulnerabilities, the associated security implications must be highlighted for system administrators to decide whether to adopt this technology and to aid designers with future development.

REFERENCES

• 1: A Secure European System for Applications in a Multi-vendor Environment, URL ON THIS PAGE.
• 2: G. Bella, Inductive Verification of Cryptographic Protocols, Ph.D. thesis, University of Cambridge, March 2000, URL BELOW.
• 3: Giampaolo Bella , Lawrence C. Paulson, Kerberos Version 4: Inductive Analysis of the Secrecy Goals, Proceedings of the 5th European Symposium on Research in Computer Security, p.361-375, September 16-18, 1998
• 4: G. Bella and E. Riccobene, Formal Analysis of the Kerberos Authentication System, J. Universal Comp. Sci. 3 (1997), no. 12, 1337--1381.
• 5: Andrew Birrell, Butler W. Lampson, Roger M. Needham, and Michael D. Schroeder, A Global Authentication Service without Global Trust, IEEE Symposium on Security and Privacy, 1986, pp. 223--230.
• 6: Frederick Butler , Iliano Cervesato , Aaron D. Jaggard , Andre Scedrov, A Formal Analysis of Some Properties of Kerberos 5 Using MSR, Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW'02), p.175, June 24-26, 2002
• 7: Frederick Butler, Iliano Cervesato, Aaron D. Jaggard, and Andre Scedrov, A Formal Analysis of Some Properties of Kerberos 5 Using MSR, Tech. Report MS-CIS-04-04, University of Pennsylvania Department of Computer and Information Science, April 2004, URL BELOW.
• 8: USC CCSS, The Kerberos Network Authentication Service, URL BELOW.
• 9: I. Cervesato, Typed MSR: Syntax and Examples, Proc. of the First International Workshop on Mathematical Methods, Models and Architectures for Computer Network Security --- MMM'01, Springer-Verlag, 2001, St. Petersburg, Russia, 21-23 May 2001.
• 10: Iliano Cervesato, Catherine Meadows, and Paul Syverson, Dolev-Yao is no better than Machiavelli, First Workshop on Issues in the Theory of Security --- WITS'00 (Geneva, Switzerland) (P. Degano, ed.), 2000.
• 11: D. Dolev and A. C. Yao, On the Security of Public-Key Protocols, IEEE Trans. on Information Theory 2 (1983), no. 29, 198--208.
• 12: Nancy Durgin , Patrick Lincoln , John Mitchell , Andre Scedrov, Multiset rewriting and the complexity of bounded security protocols, Journal of Computer Security, v.12 n.2, p.247-311, May 2004
• 13: Jason Garman, Kerberos: The Definitive Guide, O'Reilly & Associates, Inc., Sebastopol, CA, 2003
• 14: Virgil D. Gligor, Shyh-Wei Luan, and Joe Pato, On Inter-Realm Authentication in Large Distributed Systems, Journal of Computer Security 2 (1993), no. 2-3, 137--158.
• 15: Sam Hartman, Personal communications, September 2004.
• 16: M.I. Kanovich, M. Okada, and A. Scedrov, Specifying Real-Time Finite-State Systems in Linear Logic, Proc. COTIC '98 (Nice, France), Electronic Notes in Theoretical Computer Science 16(1), 1998.
• 17: J. Kohl and C. Neuman, The Kerberos Network Authentication Service (V5), September 1993, Network Working Group Request for Comments: 1510, URL BELOW.
• 18: J. C. Mitchell , M. Mitchell , U. Stern, Automated analysis of cryptographic protocols using Mur/spl phi/, Proceedings of the 1997 IEEE Symposium on Security and Privacy, p.141, May 04-07, 1997
• 19: Roger M. Needham , Michael D. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, v.21 n.12, p.993-999, Dec. 1978 [doi>10.1145/359657.359659]
• 20: B. Clifford Neuman and Theodore Ts'o, Kerberos: An Authentication Service for Computer Networks, IEEE Communications 32 (1994), no. 9, 33--38.
• 21: Clifford Neuman, John Kohl, Theodore Ts'o, Tom Yu, Sam Hartman, and Ken Raeburn, The Kerberos Network Authentication Service (V5), September 7 2004, Internet draft, expires 7 March 2005, URL BELOW.
• 22: Steve Schneider, Verifying Authentication Protocols in CSP, IEEE Transactions on Software Engineering, v.24 n.9, p.741-758, September 1998 [doi>10.1109/32.713329]
• 23: Mark-Oliver Stehr, Iliano Cervesato, and Stefan Reich, An execution environment for the MSR cryptoprotocol specification language, URL BELOW.