Modeling and Verifying the Authentication Service Exchange of the Public-Key Kerberos Protocol
LI Zhou-jun · Computer Engineering and Science · 2008
Public-Key Kerberos is a widely deployed protocol.This paper models and verifies the authentication service exchange of Public-Key Kerberos(PKINIT)by SPVT which finds a man-in-the-middle attack.This flaw allows an attacker to impersonate the key distribution center and end-servers to deceive the clients and steal key data.It is the first time to check this attack automatically by the security protocol verification tool.The result is important in the verification of sophisticated protocols.With the help of SPVT,the flaws can be found as soon as possible.It also argues that SPVT is an effective verification tool in modeling and verifying sophisticated protocols.