Security analysis of Kerberos protocol based on SPEAR II

被引：0

作者：

Zhang, Chen ^{[1
]}

Gao, Xiao-Liang ^{[1
]}

机构：

[1] School of Electronic Science and Engineering, National University of Defense Technology, Changsha

来源：

Xi Tong Gong Cheng Yu Dian Zi Ji Shu/Systems Engineering and Electronics | 2015年 / 37卷 / 10期

关键词：

Formal verification; Kerberos authentication; Protocol security; SPEAR II;

D O I：

10.3969/j.issn.1001-506X.2015.10.16

中图分类号：

学科分类号：

摘要：

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 II 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 II 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. ©, 2015, Chinese Institute of Electronics. All right reserved.

引用

页码：2292 / 2297

页数：5

共 17 条

[11]

Basin D., Cremers C., Know your enemy: Compromising adversaries in protocol analysis, ACM Transactions on Information and System Security, 17, 2, pp. 1-31, (2014)

[12]

Avalle M., Pironti A., Sisto R., Formal verification of security protocol implementations: A survey, Formal Aspects of Computing, 26, 1, pp. 99-123, (2014)

[13]

Kremer S., Kunnemann R., Automated analysis of security protocols with global state, Proc. of the IEEE Symposium on Security and Privacy, pp. 163-178, (2014)

[14]

Wang E.J., An novel BAN-liked logic for security protocol analysis and its automatic implementation, (2011)

[15]

Saul E., Hutchison A., Enhanced security protocol engineering through a unified multidimensional framework, IEEE Journal on Selected Areas in Communications, 21, 1, pp. 62-76, (2003)

[16]

Dong L., Chen K.F., Cryptographic protocol: Security analysis based on trusted freshness, pp. 341-343, (2012)

[17]

Backes M., Cervesato I., Jaggard A.D., Et al., Cryptographically sound security proofs for basic and public-key kerberos, International Journal of Information Security, 10, 2, pp. 107-134, (2011)

← 1 2 →