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

Security analysis of Kerberos protocol based on SPEAR Ⅱ

作　　者：张琛[1] 郜晓亮[1] 

机构地区：[1]国防科学技术大学电子科学与工程学院,湖南长沙410073

出　　处：《系统工程与电子技术》2015年第10期2292-2297,共6页Systems Engineering and Electronics

基　　金：国家自然科学基金(61302091)资助课题

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

关 键 词：形式化验证 SPEAR Ⅱ KERBEROS认证 协议安全性 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]