关键词: 公钥Kerberos协议 SPVT形式化建模 验证

Abstract:

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 protocoIs. With the help of SPVT, the flaws can be found as soon as possible. It also argues that SPVT is an effect   ive verification tool in modeling and verifying sophisticated protocols.

Key words: Public-Key kerberos protocol, SPVT, formal modeling, verification