公钥Kerberos协议的认证服务过程的建模与验证  

Modeling and Verifying the Authentication Service Exchange of the Public-Key Kerberos Protocol

作　　者：周倜[1] 李梦君[1] 李舟军[1,2] 

机构地区：[1]国防科技大学计算机学院,湖南长沙410073 [2]北京航空航天大学计算机学院,北京100083

出　　处：《计算机工程与科学》2008年第11期9-12,18,共5页Computer Engineering & Science

基　　金：国家自然科学基金资助项目(60473057,90604007,60703075,90718017);高等学校博士学科专项科研基金资助项目(20070006055)

摘　　要：公钥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.

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

分 类 号：TP309[自动化与计算机技术—计算机系统结构]