基于SPEAR Ⅱ的Kerberos协议安全性分析

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

Security analysis of Kerberos protocol based on SPEAR Ⅱ

Kerberos authentication is one of the information security technologies for the cloud computing security. The formal verification of the Kerberos protocol helps to discover and avoid the protocol design flaws and attacks. An automatic tool named SPEAR Ⅱ for modeling and analyzing security protocols is used to analyze the security of the Kerberos protocol. Firstly, three attack scenarios such as eavesdropping, replay and tampering are designed and characteristics of communication partners in each scenario are researched. Then, several hypothesizes are proposed, which are used as the input of a Prolog based analyzer in SPEAR Ⅱ to reason the working of the Kerberos protocol. The results show that the Kerberos protocol can keep the key safety between legal communication partners in the eavesdropping and replay attack scenarios, but the attacker can use a fake key to communicate with a legal user in the tampering attack scenario.