10.3969/j.issn.1007-130X.2008.11.003
公钥Kerberos协议的认证服务过程的建模与验证
公钥Kerberos协议是目前广泛使用的一类认证协议.本文使用安全协议验证工具SPVT对公钥Kerberos协议(PKINIT)的认证服务过程进行了形式化的建模与验证.SPVT自动地检测出PKINIT存在一个中间人攻击,该攻击可使攻击者假冒密钥发布中心和终端服务器,骗取用户信任,窃取重要数据.本文首次使用验证工具检测出公钥Kerberos协议的攻击,该攻击的自动检测对大型复杂协议的自动验证具有重大意义.借助于SPVT,人们能尽早发现协议缺陷.这充分说明,SPVT能够对大型复杂安全协议进行建模与验证,是一个有效的协议验证工具.
公钥Kerberos协议、SPVT、形式化建模、验证
30
TP309(计算技术、计算机技术)
国家自然科学基金资助项目60473057,90604007,60703075,90718017;高等学校博士学科专项科研基金资助项目20070006055
2008-11-25(万方平台首次上网日期,不代表论文的发表时间)
共5页
9-12,18