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

摘要：

公钥Kerberos协议是目前广泛使用的一类认证协议。本文使用安全协议验证工具SPVT对公钥Kerberos协议(PKINIT)的认证服务过程进行了形式化的建模与验证.SPVT自动地检测出PKINIT存在一个中间人攻击,该攻击可使攻击者假冒密钥发布中心和终端服务器,骗取用户信任,窃取重要数据.本文首次使用验证工具检测出公钥Kerberos协议的攻击,该攻击的自动检测对大型复杂协议的自动验证具有重大意义。借助于SPVT,人们能尽早发现协议缺陷.这充分说明,SPVT能够对大型复杂安全协议进行建模与验证,是一个有效的协议验证工具.

关键词： 公钥协议 形式化建模 认证协议 安全协议 协议验证

作者: 周倜 李梦君 李舟军

作者单位: 国防科技大学计算机学院,湖南,长沙,410073 国防科技大学计算机学院,湖南,长沙,410073;北京航空航天大学计算机学院,北京,100083

会议类型: 国内会议

会议名称: 2008年全国理论计算机科学学术年会

会议地点: 西安

会议语种:中文

页码: 9-12,18

在线出版日期: 2008-09-19（万方平台首次上网日期，不代表论文的发表时间）