论文部分内容阅读
Kerberos 认证是云计算安全采用的信息安全技术之一，对 Kerberos 协议进行形式化验证可以有效发现和避免协议设计缺陷和攻击。采用一种自动安全协议建模和分析工具 SPEAR Ⅱ对 Kerberos 协议的安全性进行了分析。首先设计了窃听、重放和篡改攻击场景并分析了以上场景中通信主体的特点，在此基础上提出推理假设，然后通过 SPEAR Ⅱ中基于 Prolog 的分析引擎从协议假设条件推导到协议目标。结果表明，Kerberos 协议可以抵抗窃听和重放攻击，保护合法用户密钥的安全，但在篡改攻击下，若信任主体被攻陷，则攻击者可以通过伪造密钥骗取合法用户的信任，并与合法用户建立通信。