Research on Authentication Protocol Security Based on Formal Verification Tool

doi:10.3969/j.issn.1671-1122.2015.07.011

Abstract

Abstract:

With the rapid development of the Internet services, the computer network has been the main approach to interchange of information. The Internet brings convenience to people, while also brings about privacy leakage and further more monetary loss. People devotes to themselves to protect information security in which authentication protocol is in major. Formal analysis assists protocol-design and covers the bug of protocol security. Formal analysis includes model checking, theorem proving and belief logic. AVISPA includes model checking and some else formal analysis, and also can be automatic. SPAN makes the function of AVISPA vivid and localization which is described as Message Sequence Charts. Choose SPAN to analyze SSL protocol and Kerberos protocol. It turns out that SSL protocol tends to suffer from falsify certification and the public key system isn’t secure on Kerberos protocol. To improve SSL protocol, make users not believe in SSL certification and provide the intruder from fetching public-key for encrypting certification; to improve Kerberos protocol, public-key replacing symmetric-key keeps other keys safe even if the intruder crack one key.

Key words: authentication protocol, security, SPAN, SSL protocol, Kerberos protocol

CLC Number:

TP309

Ran DUAN, Nai-yang XU, Ai-qun HU. Research on Authentication Protocol Security Based on Formal Verification Tool[J]. Netinfo Security, 2015, 15(7): 71-76.

Figures/Tables 9

References 10

[1]	Nachiketh R. Potlapally, Srivaths Ravi, Anand Raghunathan, Niraj K. Jha. A Study of the Energy Consumption Characteristics of Crytographic Algorithms and Security Protocols[J]. IEEE Transactions on mobile computing, 2006,5(2): 128-143.
[2]	Luca Vigano.Automated Security Protocol Analysis With the AVISPA Tool[C]//Electronic Notes in Theoretical Computer Science. Zurich:Elsevier,2006: 61-86.
[3]	Stefanos Gritzalis, Diomidis Spinellis.A taxonomy of flaws and related protocol analysis tools[C]//The 16th International Conference on Computer Safety, Reliability and Security. London:Springer-Verlag, 1997:123-137.
[4]	Xu Wei, Ma Yan, Liu Nan, Wu Dong-ying.A Formal Method for Analyzing Fair Exchange Protocols[C]//2009 WASE International Conference on Information Engineering. Taiyuan:IEEE,2009:645-652.
[5]	Laifeng Lu, Jianfeng Ma.Formal Analysis Model of Security Protocol Based on PCL[C]//2010 International Conference on Computer Application and System Modeling. Taiyuan:IEEE,2010:658-660.
[6]	Takahiro Minamikawa, Tatsuhiro Tsuchiya, Tohru Kikuno.Towards Automated Verification of Distributed Consensus Protocols[C]//2009 16th Asia-Pacific Software Engineering Conference. Penang:IEEE, 2009:276-291.
[7]	Peter Bokor, Johannes Kinder, Marco Serafini, Neeraj Suri.Efficient Model Checking of Fault-Tolerant Distributed Protocols[C]//2011 IEEE/IFIP 41st International Conference. Hong Kong:IEEE, 2011:63-72.
[8]	AVISPA Team. AVISPA V1.1 UserManual[N]. Information Society Technologies, 2014-1-20.
[9]	Wang Zhenzhong, Wang Yao.An Improvement SSL Protocol Application Research[C]//2011 International Conference on Electronic & Mechanical Engineering and Information Technology. Heilongjiang:IEEE, 2011:4010-4013.
[10]	Abdelmajid N.T., Hossain M.A., Shepherd, Mahmoud. Improved Kerberos Security Protocol Evaluation using Modified BAN Logic[C]//2010 10th IEEE Internatioinal Conference on Computer and Information Technology. Bradford:IEEE, 2010:1610-1615.

[1]	Jianwei LIU, Yiran HAN, Bin LIU, Beiyuan YU. Research on 5G Network Slicing Security Model [J]. Netinfo Security, 2020, 20(4): 1-11.
[2]	Zhizhou FU, Liming WANG, Ding TANG, Shuguang ZHANG. HBase Secondary Ciphertext Indexing Method Based on Homomorphic Encryption [J]. Netinfo Security, 2020, 20(4): 55-64.
[3]	Zhiyan ZHAO, Xiaomo JI. Research on the Intelligent Fusion Model of Network Security Situation Awareness [J]. Netinfo Security, 2020, 20(4): 87-93.
[4]	Ning LI, Bochao LI. Token-based UTM Architecture for Mobile Internet [J]. Netinfo Security, 2020, 20(3): 18-28.
[5]	Xinglong ZHANG, Yuting LI, Qingfeng CHENG, Lulu GUO. A Browser Security Model for Preventing TLS Protocol Downgrade Attacks [J]. Netinfo Security, 2020, 20(3): 65-74.
[6]	Shuilin LI, Guobang ZHU, Chunling FAN, Guangyong CHEN. Research on a New Scoring Algorithm of Testing and Evaluation for Classified Cybersecurity Protection [J]. Netinfo Security, 2020, 20(2): 1-6.
[7]	Xiao WANG, Jun ZHAO, Jianbiao ZHANG. Research on Dynamic Monitoring Mechanism for Virtual Machine Based on Trusted Software Base [J]. Netinfo Security, 2020, 20(2): 7-13.
[8]	Weimin LANG, Han ZHANG, Yifeng ZHAO, Jinfang YAO. A Blockchain-based Behavior Regulation and Activities Management Scheme for Internet of Things [J]. Netinfo Security, 2020, 20(2): 22-29.
[9]	Mengmeng YAO, Li TANG, Yongxing LING, Weidong XIAO. Formal Analysis of Security Protocol Based on Strand Space [J]. Netinfo Security, 2020, 20(2): 30-36.
[10]	Lu YU, Senlin LUO. A Method of Internal Intrusion Detection of Database in RBAC Mode [J]. Netinfo Security, 2020, 20(2): 83-90.
[11]	Tao JING, Wei WAN. Research on a P2P Network Communication Behavior Analytical Method for Status Migration Attribute-oriented [J]. Netinfo Security, 2020, 20(1): 16-25.
[12]	Die HU, Dongtang MA, Ming GONG, Zhao MA. A Physical Layer Security Authentication Method Based on PUF [J]. Netinfo Security, 2020, 20(1): 61-66.
[13]	Chonghua WANG, Jun LI, Xuehong CHEN. Research on Industrial Internet Platform Security Protection [J]. Netinfo Security, 2019, 19(9): 6-10.
[14]	Guogang ZHENG. Implementation Methods and Technical Measures for Security Inspection of Important Information Systems [J]. Netinfo Security, 2019, 19(9): 16-20.
[15]	Meng LI. Mobile Application Security Construction of the National Medical Products Administration [J]. Netinfo Security, 2019, 19(9): 46-50.