Formal Analysis Of 5G AKA Protocol Based On Logic Of Events

The emergence of new architectures,services and technologies in 5G networks poses new threats and challenges to network security.In order to guarantee the security of mobile communication networks and to protect the rights and interests of operators as well as the majority of network users,it is first necessary to carry out mutual authentication between the user and the network provider,the success of which is related to the ability to communicate safely.Unpredicted potential risks will be posed if the security properties of the network protocol are not verified in a complex network environment.The use of formal methods to analyze the security of network security protocols is recognized as one of the most effective methods in the world today.Logic of events(LoET)belongs to theorem proving,one of the formal methods,and is based on the design of message automata.LoET defines for all possible protocol actions,and provides new proof rules for the operation of the protocol by assigning keys,challenge numbers and different types of messages to the protocol interaction process.This paper uses LoET to investigate the 5G AKA protocol.The existing LoET is improved by extending the event classes and axiom systems in LoET.The extended LoET is also used to analyze the security properties of the 5G AKA protocol and to make the event logic theory applicable to the new generation of mobile communication network protocols.The main contributions of this paper are as follows.1.Based on LoET,extend the Event Class in logic of events by adding two new protocol actions,Compute and Retrieve;based on the extended Event Class,redefine has in the flow relation axiom;two concepts MatchingF and ComMatch are introduced to provide support for extending the causal axiom;extend the compute axiom AxiomC with a complete exposition of the matching of protocol actions.2.Based on the above improved LoET,the security of the 5G AKA based 5G network related authentication protocol is analyzed,the formal representation of keys,challenge numbers and protocol messages in the 5G AKA protocol is given along with a formal description of the protocol actions;the mutual authentication process of the 5G AKA protocol is defined using basic sequences and the basic sequences are ordered to formally portray the authentication properties of the 5 G AKA protocol;finally,the authentication properties of the 5G AKA protocol are analyzed using the LoET axiom system.3.Using improved LoET,the 5G AKA protocol is abstracted for the first time via LoET based on the 5G AKA security implementation principle to conclude that the 5G AKA protocol is secure under reasonable assumptions,showing that LoET can be used to prove the authenticity of cryptographic protocols related to mobile communication networks.