Breaking and fixing public-key Kerberos

被引:33
作者
Cervesato, Iliano [2 ]
Jaggard, Aaron D. [3 ]
Scedrov, Andre [1 ]
Tsay, Joe-Kai [1 ]
Walstad, Christopher [4 ]
机构
[1] Univ Penn, Dept Math, Philadelphia, PA 19104 USA
[2] Carnegie Mellon Univ Qatar, Doha, Qatar
[3] Rutgers State Univ, DIMACS, Piscataway, NJ 08854 USA
[4] Univ Penn, Sch Engn & Appl Sci, Philadelphia, PA 19104 USA
基金
美国国家科学基金会;
关键词
computer security; authentication protocols; Kerberos; PKINIT; man-in-the-middle attack; protocol verification;
D O I
10.1016/j.ic.2007.05.005
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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. (C) 2007 Elsevier Inc. All rights reserved.
引用
收藏
页码:402 / 424
页数:23
相关论文
共 46 条
[1]   Analyzing security protocols with secrecy types and logic programs [J].
Abadi, M ;
Blanchet, B .
JOURNAL OF THE ACM, 2005, 52 (01) :102-146
[2]   Prudent engineering practice for cryptographic protocols [J].
Abadi, M ;
Needham, R .
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1996, 22 (01) :6-15
[3]  
ANLAUFF M, 2006, P FCS ARSPA 2006
[4]  
[Anonymous], ENCRYPTION CHECKSUM
[5]  
[Anonymous], 1996, LNCS
[6]  
Armando A, 2005, LECT NOTES COMPUT SC, V3576, P281
[7]  
Backes M, 2006, LECT NOTES COMPUT SC, V4189, P362
[8]  
Backes M., 2003, P 10 ACM C COMP COMM, P220, DOI DOI 10.1145/948109.948140
[9]  
Blanchet B, 2002, LECT NOTES COMPUT SC, V2477, P342
[10]   An efficient cryptographic protocol verifier based on prolog rules [J].
Blanchet, B .
14TH IEEE COMPUTER SECURITY FOUNDATIONS WORKSHOP, PROCEEDINGS, 2001, :82-96