Research On Formal Verification Of 5G Protocol Based On EAP Framework

As a key component of the 5G network security architecture,the authentication protocol plays the first role in ensuring the confidentiality of user data and other communication security.However,with the increasing ability of attackers and the increasing complexity of the protocol itself,attacks against authentication protocols emerge in an endless stream.It is difficult to find the loopholes in the protocol only by manual identification,while the formal analysis method can effectively detect the potential loopholes in the protocol,and can realize automatic analysis.Therefore,this paper adopts a formal method to study 5G related protocols,mainly to formally analyze and verify the EAP-TLS protocol and EAP-AKA’ protocol under the EAP framework.The main research work is as follows:1.The formal model of EAP-TLS protocol and security properties with Pro Verif were researched in this paper,in which security properties such as the mutual authentication between user equipment and network,and confidentiality between KSEAF(security anchor key)and SUPI(Subscriber Permanent Identity).The verification results are analyzed to determine the reasons for the security flaws,and give the corresponding attack paths.Finally,based on the asymmetric key encryption method and message identification in cryptography,the possibility of improving the security flaw is discussed.2.Formal verification and analysis of the newly introduced EAP-AKA’ protocol in the5 G system.Firstly,the channel and EAP-AKA’ protocol are formally modeled,and then the security properties are formally described.Using Pro Verif to verify the confidentiality of KSEAF and SUPI in the protocol,as well as the security properties such as mutual authentication between the user equipment and the network.The verification results are further analyzed,the security of EAP-AKA’ protocol is discussed,and it is proved that EAP-AKA’ protocol satisfies the confidentiality of session keys and the mutual authentication between user equipment and network.3.An authentication method based on asymmetric key encryption and message identification in EAP-AKA’ protocol is proposed,and formal verification and analysis of the method.The verification results show that the method guarantees the confidentiality of the protocol session key and the authentication between the user equipment and the network.