CAJ | 학술논문

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