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

DUAN Ran, XU Nai-yang, HU Ai-qun. 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]	SHEN Xiuyu, JI Weifeng. Optimization of Cost of Edge-Cloud Collaborative Computing Offloading Considering Security [J]. Netinfo Security, 2024, 24(7): 1110-1121.
[2]	ZHAO Xinqiang, FAN Bo, ZHANG Dongju. Research on APT Attack Defense System Based on Threat Discovery [J]. Netinfo Security, 2024, 24(7): 1122-1128.
[3]	WEN Wen, LIU Qinju, KUANG Lin, REN Xuejing. Research and Scheme Design of Cyber Threat Intelligence Sharing under Privacy Protection System [J]. Netinfo Security, 2024, 24(7): 1129-1137.
[4]	GUO Xiangxin, LIN Jingqiang, JIA Shijie, LI Guangzheng. Security Analysis of Cryptographic Application Code Generated by Large Language Model [J]. Netinfo Security, 2024, 24(6): 917-925.
[5]	LING Zhi, YANG Ming, YU Jiangyin. Research on Power Security Trading Platform Based on IPFS and Blockchain Technology [J]. Netinfo Security, 2024, 24(6): 968-976.
[6]	ZHANG Changlin, TONG Xin, TONG Hui, YANG Ying. A Survey of Large Language Models in the Domain of Cybersecurity [J]. Netinfo Security, 2024, 24(5): 778-793.
[7]	WANG Wei, HU Yongtao, LIU Qingtao, WANG Kailun. Research on Softwaization Techniques for ERT Trusted Root Entity in Railway Operation Environment [J]. Netinfo Security, 2024, 24(5): 794-801.
[8]	LIU Sinuo, RUAN Shuhua, CHEN Xingshu, ZHENG Tao. An eBPF-Based Threat Observability System for Cloud-Oriented Environment [J]. Netinfo Security, 2024, 24(4): 534-544.
[9]	ZHANG Yanshuo, YUAN Yuqi, LI Liqiu, YANG Yatao, QIN Xiaohong. Periodically Deniable Ring Signature Scheme Based on SM2 Digital Signature Algorithm [J]. Netinfo Security, 2024, 24(4): 564-573.
[10]	LIU Feng, JIANG Jiaqi, HUANG Hao. Security Overview of Cryptocurrency Trading Media and Processes [J]. Netinfo Security, 2024, 24(3): 330-351.
[11]	YANG Zhipeng, LIU Daidong, YUAN Junyi, WEI Songjie. Research on Network Local Security Situation Fusion Method Based on Self-Attention Mechanism [J]. Netinfo Security, 2024, 24(3): 398-410.
[12]	HUANG Haiyan, AI Yuxin, LIANG Linlin, LI Zan. Analysis of Physical Layer Security Performance in RSMA Wireless Communication Systems under Eavesdropper Attacks [J]. Netinfo Security, 2024, 24(2): 252-261.
[13]	YAN Hailong, WANG Shulan. Design and Implementation of Integrated Service Platform for Real Estate Registration Based on Domestic Cryptographic Technology [J]. Netinfo Security, 2024, 24(2): 303-308.
[14]	ZHANG Bowen, LI Dong, ZHAO Yizhu, YU Junqing. Research on Endogenous Security Mechanism of Cloud Network Driven by IPv6 Address [J]. Netinfo Security, 2024, 24(1): 113-120.
[15]	PU Junyan, LI Yahui, ZHOU Chunjie. Cross-Domain Dynamic Security Risk Analysis Method of Industrial Control System Based on Probabilistic Attack Graph [J]. Netinfo Security, 2023, 23(9): 85-94.