Design And Formal Verification Of 5G Authentication Protocol

The mobile communication network is an important infrastructure of the country,which is rooted in social production and life.The issuance of the national 5G commercial license in June 2019 means the arrival of the 5G era,and it also means that the security of 5G network has become the focus of the current society.The rapid advancement of network technology will inevitably bring new security risks and challenges.Cyber attackers attack the 5G network for various purposes,like eavesdropping,counterfeiting,forgery,tampering and so on.And obtain illegal benefits.The authentication mechanism is the first line of defense to protect the security of the mobile communication network.While inheriting the 4G network authentication mechanism,the security of 5G network has also been optimized and enhanced,and is committed to providing users with a safer business environment and stricter privacy of data protection service.However,consulting research materials related to 5G network security,it is found that the current5 G AKA authentication protocol still has security loopholes in terms of privacy and confidentiality.The main purpose of this article is to explain the security vulnerabilities of the 5G AKA protocol through formal analysis,and to propose a targeted modification plan.At the same time,based on the original protocol,design a security reinforcement protocol that is resistant to flooding attacks and has a higher security level,and through formal analysis Prove the security of the security reinforcement program.The main work of this paper includes the following three aspects:(1)Security analysis: Summarize the security goals of the 5G AKA protocol by analyzing common authentication protocol attack scenarios and 5G security standards.Based on the security objectives,the security of the 5G AKA protocol is analyzed,and the existing security vulnerabilities in the 5G AKA protocol are explained.These vulnerabilities may lead to attacks including fake users,establishment of fake base stations,and eavesdropping to obtain user privacy.(2)Protocol design: Based on the results of security analysis,this paper proposes a key agreement scheme based on the Puzzle mechanism to resist flooding attacks and the asymmetric key agreement algorithm ECDH(Elliptic Curve Diffie–Hellman key Exchange)to secure the original agreement Reinforced design,the purpose is to enhance the security of the 5G AKA protocol.(3)Formal Analysis: This paper uses the formal verification tool Tamarin to complete the modeling and formal security analysis of the protocol before and after the reinforcement.Combining with the multiple hidden security risks of the 5G AKA protocol before the transformation,compare the analysis results of the protocol after the transformation.It proves that the security enhancement of the reinforcement solution can resist a variety of attack scenarios including man-in-the-middle attacks,establishment of pseudo base stations,and replay attacks to obtain user privacy,and provide perfect forward secrecy.In addition,this article also conducts a simple comparison and analysis of the 5G AKA protocol before and after reinforcement in terms of performance.It is found that the protocol overhead after the transformation has increased,but this article believes that it is worthwhile to exchange lightweight calculations for higher security of the protocol.