×

Breaking and fixing public-key Kerberos. (English) Zbl 1147.68393

Summary: We report on a man-in-the-middle attack on PKINIT, the public key extension of the widely deployed Kerberos 5 authentication protocol. This flaw allows an attacker to impersonate Kerberos administrative principals (KDC) and end-servers to a client, hence breaching the authentication guarantees of Kerberos. It also gives the attacker the keys that the KDC would normally generate to encrypt the service requests of this client, hence defeating confidentiality as well. The discovery of this attack caused the IETF to change the specification of PKINIT and Microsoft to release a security update for some Windows operating systems. We discovered this attack as part of an ongoing formal analysis of the Kerberos protocol suite, and we have formally verified several possible fixes to PKINIT-including the one adopted by the IETF-that prevent our attack as well as other authentication and secrecy properties of Kerberos with PKINIT.

MSC:

68M12 Network protocols
68M10 Network design and communication in computer systems
68P25 Data encryption (aspects in computer science)

Software:

AVISPA
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] C. Neuman, T. Yu, S. Hartman, K. Raeburn, The Kerberos Network Authentication Service (V5). Available from: <http://www.ietf.org/rfc/rfc4120> (July 2005).; C. Neuman, T. Yu, S. Hartman, K. Raeburn, The Kerberos Network Authentication Service (V5). Available from: <http://www.ietf.org/rfc/rfc4120> (July 2005).
[2] M. Thomas, J. Vilhuber, Kerberized Internet Negotiation of Keys (KINK). Available from: <http://ietfreport.isoc.org/all-ids/draft-ietf-kink-kink-06.txt> (December 2003).; M. Thomas, J. Vilhuber, Kerberized Internet Negotiation of Keys (KINK). Available from: <http://ietfreport.isoc.org/all-ids/draft-ietf-kink-kink-06.txt> (December 2003).
[3] J. Kohl, C. Neuman, The Kerberos Network Authentication Service (V5). Available from: <http://www.ietf.org/rfc/rfc1510> (September 1993).; J. Kohl, C. Neuman, The Kerberos Network Authentication Service (V5). Available from: <http://www.ietf.org/rfc/rfc1510> (September 1993).
[4] Microsoft, Security Bulletin MS05-042. Available from: <http://www.microsoft.com/technet/security/bulletin/MS05-042.mspx> (August 2005).; Microsoft, Security Bulletin MS05-042. Available from: <http://www.microsoft.com/technet/security/bulletin/MS05-042.mspx> (August 2005).
[5] M. Strasser, A. Steffen, Kerberos PKINIT Implementation for Unix Clients, Tech. Rep., Zurich University of Applied Sciences Winterthur (2002).; M. Strasser, A. Steffen, Kerberos PKINIT Implementation for Unix Clients, Tech. Rep., Zurich University of Applied Sciences Winterthur (2002).
[6] T. Yu, S. Hartman, K. Raeburn, The perils of unauthenticated encryption: Kerberos version 4, in: Proc. NDSS’04, 2004.; T. Yu, S. Hartman, K. Raeburn, The perils of unauthenticated encryption: Kerberos version 4, in: Proc. NDSS’04, 2004.
[7] F. Butler, I. Cervesato, A.D. Jaggard, A. Scedrov, An analysis of some properties of Kerberos 5 using MSR, in: Proc. CSFW’02, 2002, pp. 175-190.; F. Butler, I. Cervesato, A.D. Jaggard, A. Scedrov, An analysis of some properties of Kerberos 5 using MSR, in: Proc. CSFW’02, 2002, pp. 175-190.
[8] Butler, F.; Cervesato, I.; Jaggard, A. D.; Scedrov, A.; Walstad, C., Formal Analysis of Kerberos 5, Theor. Comput. Sci., 367, 1-2, 57-87 (2006) · Zbl 1153.94448
[9] I. Cervesato, A.D. Jaggard, A. Scedrov, C. Walstad, Specifying Kerberos 5 cross-realm authentication, in: Proc. WITS’05, ACM Digital Lib., 2005, pp. 12-26.; I. Cervesato, A.D. Jaggard, A. Scedrov, C. Walstad, Specifying Kerberos 5 cross-realm authentication, in: Proc. WITS’05, ACM Digital Lib., 2005, pp. 12-26.
[10] Abadi, M.; Blanchet, B., Analyzing security protocols with secrecy types and logic programs, J. ACM, 52, 1, 102-146 (2005) · Zbl 1204.68030
[11] M. Anlauff, D. Pavlovic, R. Waldinger, S. Westfold, Proving authentication properties in the protocol derivation assistant, in: P. Degano, R. Küsters, L. Vigano (Eds.), Proc. FCS-ARSPA 2006, ACM, 2006, to appear URL: <ftp://ftp.kestrel.edu/pub/papers/pavlovic/FCS-ARSPA06.pdf>.; M. Anlauff, D. Pavlovic, R. Waldinger, S. Westfold, Proving authentication properties in the protocol derivation assistant, in: P. Degano, R. Küsters, L. Vigano (Eds.), Proc. FCS-ARSPA 2006, ACM, 2006, to appear URL: <ftp://ftp.kestrel.edu/pub/papers/pavlovic/FCS-ARSPA06.pdf>.
[12] B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, in: 14th IEEE Computer Security Foundations Workshop (CSFW-14), IEEE Computer Society, Cape Breton, Nova Scotia, Canada, 2001, pp.82-96.; B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, in: 14th IEEE Computer Security Foundations Workshop (CSFW-14), IEEE Computer Society, Cape Breton, Nova Scotia, Canada, 2001, pp.82-96.
[13] B. Blanchet, From secrecy to authenticity in security protocols, in: M. Hermenegildo, G. Puebla (Eds.), 9th International Static Analysis Symposium (SAS’02), vol. 2477 of Lecture Notes on Computer Science, Springer Verlag, Madrid, Spain, 2002, pp. 342-359.; B. Blanchet, From secrecy to authenticity in security protocols, in: M. Hermenegildo, G. Puebla (Eds.), 9th International Static Analysis Symposium (SAS’02), vol. 2477 of Lecture Notes on Computer Science, Springer Verlag, Madrid, Spain, 2002, pp. 342-359. · Zbl 1015.68070
[14] S.F. Doghmi, J.D. Guttman, F.J. Thayer, Searching for shapes in cryptographic protocols, in: Proc. TACAS 2007, 2007.; S.F. Doghmi, J.D. Guttman, F.J. Thayer, Searching for shapes in cryptographic protocols, in: Proc. TACAS 2007, 2007. · Zbl 1186.94435
[15] Viganò, L., Automated security protocol analysis with the AVISPA tool, Electr. Notes Theor. Comput. Sci., 155, 61-86 (2006)
[16] Armando, A.; Basin, D. A.; Boichut, Y.; Chevalier, Y.; Compagna, L.; Cuéllar, J.; Drielsma, P. H.; Héam, P.-C.; Kouchnarenko, O.; Mantovani, J.; Mödersheim, S.; von Oheimb, D.; Rusinowitch, M.; Santiago, J.; Turuani, M.; Viganó, L.; Vigneron, L., The AVISPA tool for the automated validation of internet security protocols and applications, (Etessami, K.; Rajamani, S. K., CAV. CAV, Lect. Notes Comput. Sci., vol. 3576 (2005), Springer), 281-285 · Zbl 1081.68523
[17] C. Cremers, Scyther—semantics and verification of security protocols, Ph.D. dissertation, Eindhoven University of Technology (2006).; C. Cremers, Scyther—semantics and verification of security protocols, Ph.D. dissertation, Eindhoven University of Technology (2006).
[18] Kemmerer, R.; Meadows, C.; Millen, J., Three systems for cryptographic protocol analysis, J. Cryptol., 7, 79-130 (1994) · Zbl 0814.94011
[19] C. Meadows, Analysis of the internet key exchange protocol using the NRL protocol analyzer, in: Proc. IEEE Symp. Security Privacy, 1999, pp. 216-231.; C. Meadows, Analysis of the internet key exchange protocol using the NRL protocol analyzer, in: Proc. IEEE Symp. Security Privacy, 1999, pp. 216-231.
[20] J.C. Mitchell, V. Shmatikov, U. Stern, Finite-state analysis of SSL 3.0, in: Proc. 7th USENIX Security Symp., 1998, pp. 201-216.; J.C. Mitchell, V. Shmatikov, U. Stern, Finite-state analysis of SSL 3.0, in: Proc. 7th USENIX Security Symp., 1998, pp. 201-216.
[21] M. Backes, I. Cervesato, A. D. Jaggard, A. Scedrov, J.-K. Tsay, Cryptographically sound security proofs for basic and public-key Kerberos, in: D. Gollmann, J. Meier, A. Sabelfeld (Eds.), Proc. ESORICS’06, Springer LNCS 4189, 2006, pp. 362-383.; M. Backes, I. Cervesato, A. D. Jaggard, A. Scedrov, J.-K. Tsay, Cryptographically sound security proofs for basic and public-key Kerberos, in: D. Gollmann, J. Meier, A. Sabelfeld (Eds.), Proc. ESORICS’06, Springer LNCS 4189, 2006, pp. 362-383.
[22] A.D. Jaggard, A. Scedrov, J.-K. Tsay, Computational sound mechanized proof of PKINIT for Kerberos, presented at FCC’07 (no proceedings) (2007).; A.D. Jaggard, A. Scedrov, J.-K. Tsay, Computational sound mechanized proof of PKINIT for Kerberos, presented at FCC’07 (no proceedings) (2007).
[23] B. Blanchet, A computationally sound mechanized prover for security protocols, in: IEEE Symposium on Security and Privacy, Oakland, CA, 2006, pp. 140-154.; B. Blanchet, A computationally sound mechanized prover for security protocols, in: IEEE Symposium on Security and Privacy, Oakland, CA, 2006, pp. 140-154.
[24] B. Blanchet, Computationally sound mechanized proofs of correspondence assertions, in: 20th IEEE Computer Security Foundations Symposium (CSF’07), IEEE, Venice, Italy, 2007, pp. 97-111.; B. Blanchet, Computationally sound mechanized proofs of correspondence assertions, in: 20th IEEE Computer Security Foundations Symposium (CSF’07), IEEE, Venice, Italy, 2007, pp. 97-111.
[25] IETF, Public Key cryptography for initial authentication in Kerberos, RFC 4556, Preliminary versions available as a sequence of Internet Drafts at: <http://tools.ietf.org/wg/krb-wg/draft-ietf-cat-kerberos-pk-init/> (1996-2006).; IETF, Public Key cryptography for initial authentication in Kerberos, RFC 4556, Preliminary versions available as a sequence of Internet Drafts at: <http://tools.ietf.org/wg/krb-wg/draft-ietf-cat-kerberos-pk-init/> (1996-2006).
[26] CERT, Vulnerability Note 477341. Available from: <http://www.kb.cert.org/vuls/id/477341> (2005).; CERT, Vulnerability Note 477341. Available from: <http://www.kb.cert.org/vuls/id/477341> (2005).
[27] I. Cervesato, A.D. Jaggard, A. Scedrov, J.-K. Tsay, C. Walstad, Breaking and fixing public-key Kerberos, in: Proceedings of ASIAN’06, 2006, pp. 164-178.; I. Cervesato, A.D. Jaggard, A. Scedrov, J.-K. Tsay, C. Walstad, Breaking and fixing public-key Kerberos, in: Proceedings of ASIAN’06, 2006, pp. 164-178. · Zbl 1147.68393
[28] J. De Clercq, M. Balladelli, Windows 2000 authentication, <http://www.windowsitlibrary.com/Content/617/06/6.html>, digital Press (2001).; J. De Clercq, M. Balladelli, Windows 2000 authentication, <http://www.windowsitlibrary.com/Content/617/06/6.html>, digital Press (2001).
[29] Cable Television Laboratories, Inc., PacketCable Security Specification, technical document PKT-SP-SEC-I11-040730 (2004).; Cable Television Laboratories, Inc., PacketCable Security Specification, technical document PKT-SP-SEC-I11-040730 (2004).
[30] Goldwasser, S.; Micali, S.; Rivest, R. L., A digital signature scheme secure against adaptive chosen message attacks, SIAM J. Comput., 17, 281-308 (1988) · Zbl 0644.94012
[31] I. Cervesato, Typed MSR: syntax and examples, in: Proc. MMM’01, Springer LNCS 2052, 2001, pp. 159-177.; I. Cervesato, Typed MSR: syntax and examples, in: Proc. MMM’01, Springer LNCS 2052, 2001, pp. 159-177. · Zbl 0986.68510
[32] Durgin, N. A.; Lincoln, P.; Mitchell, J.; Scedrov, A., Multiset rewriting and the complexity of bounded security protocols, J. Comp. Security, 12, 2, 247-311 (2004)
[33] Diffie, W.; van Oorschot, P. C.; Wiener, M. J., Authentication and authenticated key exchanges, Designs Codes Cryptogr., 2, 2, 107-125 (1992)
[34] R. Canetti, H. Krawczyk, Security analysis of IKE’s signature-based key-exchange protocol, in: Proc. CRYPTO’02, Springer LNCS 2442, 2002, pp. 143-161.; R. Canetti, H. Krawczyk, Security analysis of IKE’s signature-based key-exchange protocol, in: Proc. CRYPTO’02, Springer LNCS 2442, 2002, pp. 143-161. · Zbl 1026.94524
[35] D. Harkins, D. Carrel, The Internet key exchange (IKE). Available from: <http://www.ietf.org/rfc/rfc2409> (November 1998).; D. Harkins, D. Carrel, The Internet key exchange (IKE). Available from: <http://www.ietf.org/rfc/rfc2409> (November 1998).
[36] G. Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using FDR, in: Proc. TACAS’96, Springer LNCS 1055, 1996, pp. 147-166.; G. Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using FDR, in: Proc. TACAS’96, Springer LNCS 1055, 1996, pp. 147-166.
[37] Needham, R.; Schroeder, M., Using encryption for authentication in large networks of computers, Comm. ACM, 21, 12, 993-999 (1978) · Zbl 0387.68003
[38] Clark, J.; Jacob, J., On the security of recent protocols, Inform. Process. Lett., 56, 3, 151-155 (1995) · Zbl 1004.68503
[39] Hwang, T.; Chen, Y.-H., On the security of SPLICE/AS—the authentication system in WIDE internet, Inform. Process. Lett., 53, 2, 91-101 (1995) · Zbl 0875.68376
[40] Abadi, M.; Needham, R., Prudent engineering practice for cryptographic protocols, IEEE Trans. Software Eng., 22, 1, 6-15 (1996)
[41] K. Raeburn, Encryption and checksum specifications for Kerberos 5. Available from: <http://www.ietf.org/rfc/rfc3961.txt> (February 2005).; K. Raeburn, Encryption and checksum specifications for Kerberos 5. Available from: <http://www.ietf.org/rfc/rfc3961.txt> (February 2005).
[42] F. Butler, I. Cervesato, A.D. Jaggard, A. Scedrov, Confidentiality and authentication in Kerberos 5, Tech. Rep. MS-CIS-04-04, UPenn (2004).; F. Butler, I. Cervesato, A.D. Jaggard, A. Scedrov, Confidentiality and authentication in Kerberos 5, Tech. Rep. MS-CIS-04-04, UPenn (2004).
[43] I. Cervesato, A specification language for crypto-protocols based on multiset. Rewriting, dependent types and subsorting, in: G. Delzanno, S. Etalle, M. Gabbrielli (Eds.), Workshop on Specification, Analysis and Validation for Emerging Technologies—SAVE’01, Paphos, Cyprus, 2001, pp. 1-22.; I. Cervesato, A specification language for crypto-protocols based on multiset. Rewriting, dependent types and subsorting, in: G. Delzanno, S. Etalle, M. Gabbrielli (Eds.), Workshop on Specification, Analysis and Validation for Emerging Technologies—SAVE’01, Paphos, Cyprus, 2001, pp. 1-22.
[44] Dolev, D.; Yao, A., On the security of public-key protocols, IEEE Trans. Info. Theory, 2, 29, 198-208 (1983) · Zbl 0502.94005
[45] M. Backes, B. Pfitzmann, M. Waidner, A composable cryptographic library with nested operations, in: Proc. CCS’03, ACM, 2003, pp. 220-230.; M. Backes, B. Pfitzmann, M. Waidner, A composable cryptographic library with nested operations, in: Proc. CCS’03, ACM, 2003, pp. 220-230.
[46] C. Sprenger, M. Backes, D. Basin, B. Pfitzmann, M. Waidner, Cryptographically sound theorem proving, in: Proc., CSFW ’06, 2006, pp. 153-166.; C. Sprenger, M. Backes, D. Basin, B. Pfitzmann, M. Waidner, Cryptographically sound theorem proving, in: Proc., CSFW ’06, 2006, pp. 153-166.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.