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 条

[1]

Singh N., Singh S., Agarwal S., An efficient approach for software protection in cloud computing, Proc. of the 4th International Conference on Communication Systems and Network Technologies, pp. 550-554, (2014)

[2]

Chiwande V.N., Tayal A.R., An approach to balance the load with security for distributed file system in cloud, Proc. of the International Conference on Electronic Systems, Signal Processing and Computing Technologies, pp. 266-270, (2014)

[3]

Hojabri M., Rao K.V., Innovation in cloud computing: Implementation of Kerberos version5 in cloud computing in order to enhance the security issues, Proc. of the International Conference on Information Communication and Embedded Systems, pp. 452-456, (2013)

[4]

Zhou M., Study of data security related to cloud computing, (2013)

[5]

Lee G., How to formally model features of network security protocols, International Journal of Security and Its Applications, 8, 1, pp. 423-432, (2014)

[6]

Comon L.H., Cortier V., How to prove security of communication protocols: A discussion on the soundness of formal models with regard to computational ones, Proc. of the 28th International Symposium on Theoretical Aspects of Computer Science, pp. 29-44, (2011)

[7]

Lei X.F., Song S.M., Liu W.B., Et al., A survey on computationally sound formal analysis of cryptographic protocols, Chinese Journal of Computers, 37, 5, pp. 993-994, (2014)

[8]

Brooks R., Husain B., Yun S.B., Et al., Security and performance evaluation of security protocols, Proc. of the 8th Annual Cyber Security and Information Intelligence Research Workshop: Federal Cyber Security R and D Program Thrusts, pp. 5-8, (2013)

[9]

Meier S., Schmidt B., Cremers C., Et al., The TAMARIN prover for the symbolic analysis of security protocols, Proc. of the 25th International Conference on Computer Aided Verification, pp. 696-701, (2013)

[10]

Meier S., Cremers C., Basin D., Efficient construction of machine-checked symbolic protocol security proofs, Journal of Computer Security, 21, 1, pp. 41-87, (2013)

← 1 2 →