Research On Formal Analysis And Improvement Of 5G/5G-A Authentication Mechanism

The Fifth Generation(5G)mobile communication network is fully commercialized,promoting social and economic development and digital transformation,and mobile communication has entered a new era of rapid development While rapidly updating and iterating,communication networks are also facing increasingly severe security challenges and constantly suffering from various forms and types of malicious attacks.As the foundation and first security barrier of network security,the authentication mechanism has attracted much attention.However,throughout the development process of the mobile communication authentication mechanism,from the initial one-way authentication to the current two-way authentication,each update of the authentication mechanism is designed based on human experience,and it is worth thinking about whether there are still security risks in the absence of corresponding security certificates.At the same time,5G-Advanced networks are evolving towards space-space-ground integrated communication and ubiquitous connectivity,and the introduction of new access technologies such as satellite communication makes it difficult for the existing authentication mechanism to ensure the security of the switching process between networks,which brings more security challenges to the development of communication networks,and further research is needed.This paper studies the authentication mechanism of mobile communication network,analyzes the security of existing authentication mechanism based on formal verification theory,and designs an authentication mechanism to meet the security needs of mobile communication network development and evolution.(1)The existing 5G Authentication and Key Agreement(5G AKA)mechanism further enhances the Fourth Generation(4G)network authentication mechanism based on human experience,and there is no complete security theory analysis,and there are still security risks.In this paper,a formal analysis model of 5G AKA is constructed by combing the process,security attributes and security assumptions of the 5G authentication mechanism.Based on this model,this paper uses the formal theories such as Lowe classification,stage modeling and observation equivalence to model and analyze security attributes such as authentication attributes,secret attributes and unlinkability,and further designs a verification scheme to minimize security assumptions to find the mapping relationship between security attributes and security assumptions.The formal verification results show that the existing 5G authentication mechanism has security risks such as replay attacks,session link attacks,and relay attacks,and cannot meet the forward security of keys,which is difficult to provide a secure access environment for mobile users.(2)Aiming at the security threats faced by existing 5G authentication mechanisms such as session linkability,replay attacks and forward secrecy,this paper proposes a more secure access authentication scheme.The proposed scheme uses random number dynamic filling technology to avoid link attacks caused by identity length differences,and ensures the privacy of identity information through encryption technology.Then,by adding the challenge answering mechanism of random numbers,the replay protection ability of the session is enhanced,and the key negotiation is based on fresh random numbers,which optimizes the existing vertical key system and provides forward security for the keys in the system.At the same time,by verifying the time difference of the message,the threat of the system from relay attacks is effectively reduced,and the key update mechanism is further designed to provide fresh keys for the system.Finally,based on the formal verification tool,this paper establishes the formal model of the proposed scheme.The proposed scheme can prevent the security threats existing in the 5G authentication mechanism,and provide a secure access environment for mobile users.(3)To solve the problem that the existing handover authentication mechanism cannot cope with the security problems caused by the introduction of new technologies such as satellite communications,this paper designs a more secure and lightweight handover authentication scheme.The proposed scheme transfers the handover authentication function to the access node,and the user and the satellite can complete mutual authentication through only two interactions,which effectively reduces the delay of switching authentication.At the same time,in order to avoid signaling congestion caused by concurrent requests from users,the scheme supports batch switching authentication of users,which further reduces the computing overhead of authentication.This paper also designs a key update scheme to regularly update the system key to prevent key leakage and revoke user forgery attacks,and ensure the security of the system.Finally,this paper also establishes a formal model of the proposed scheme,which verifies that the scheme can meet the security attributes such as confidentiality,authentication,and unlinkability.Numerical results also show that the proposed scheme only requires low switching authentication delay and communication overhead,which ensures the efficient switching of users in the system.