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

• 作者: 周倜 李梦君 李舟军
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 公钥Kerberos协议 SPVT 形式化建模 验证
• 年，卷（期）: 2008,（11）
• 所属期刊栏目: 计算机网络与安全
• 页码范围: 9-12,18
• 页数: 5页
• 分类号: TP309
• 字数: 5452字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2008.11.003

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李舟军	国防科技大学计算机学院	136	2221	23.0	43.0
3	周倜	国防科技大学计算机学院	8	33	3.0	5.0
4	李梦君	国防科技大学计算机学院	21	193	8.0	13.0