摘要
公钥Kerberos协议是目前广泛使用的一类认证协议。本文使用安全协议验证工具SPVT对公钥Kerberos协议(PKINIT)的认证服务过程进行了形式化的建模与验证。SPVT自动地检测出PKINIT存在一个中间人攻击,该攻击可使攻击者假冒密钥发布中心和终端服务器,骗取用户信任,窃取重要数据。本文首次使用验证工具检测出公钥Kerberos协议的攻击,该攻击的自动检测对大型复杂协议的自动验证具有重大意义。借助于SPVT,人们能尽早发现协议缺陷。这充分说明,SPVT能够对大型复杂安全协议进行建模与验证,是一个有效的协议验证工具。
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 effective verification tool in modeling and verifying sophisticated protocols.
出处
《计算机工程与科学》
CSCD
2008年第11期9-12,18,共5页
Computer Engineering & Science
基金
国家自然科学基金资助项目(60473057,90604007,60703075,90718017)
高等学校博士学科专项科研基金资助项目(20070006055)
