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