Security Verification And Improvement Of 5G AKA Protocol Based On Petri Net

5G has been widely used in several domains of life.The widespread utilization of5 G technology not only has a remarkable influence on the mobile communication,but can also resolve the conundrums widely existing in industry.Ensuring the security of 5G Authentication and Key Agreement(5G AKA)is utmost important in the context of the upcoming widespread use of 5G.It is an important protocol for verifying the identities of communication parties and ensuring the security of the communication process.Compared with scenarios of 3G and 4G,5G AKA has optimized the encryption algorithm and authentication process to ensure the security of communication.On the one hand,it adopts complex encryption algorithm to ensure the security of messages,which makes messages cannot be obtained by an attacker in plaintext.On the other hand,the authentication response requires two-level network verification,which verifying the legitimacy of user equipment and reducing the risk of forgery of the serving network.However,messages need to be transmitted in wireless channel during the authentication precess.Even the message cannot be obtained in plaintext,the attacker can still use this information to interfere with the authentication process.In addition,serving network could interfered by an attacker easily in 5G.Using simple verification method for the serving network no longer meets the security requirements.Formal verification method,Petri net,is adopted to model the 5G AKA protocol in our work.We analyzed the security properties of current vision of 5G AKA,designed three kinds of attack method mainly happened in wireless channel and serving network.Using AUTN reply attack,the attacker could obtain location information by utilizing the response of user equipment.SQN mismatch attack mainly uses the linear growth defect of the sequence number while bogus SN attack uses the shortcomings of insufficient verification of the serving network during the authentication process.Besides,we also give an improved scheme by adopting challenge response mechanism and designing Unique Identifier(UNI)for the AKA protocol.In our novel scheme,all entities could distinguish the source of messages.Messages sent by attackers are difficult to be transmitted in the network.Meanwhile,challenge response mechanism is used between home network and serving network.Serving network needs to obtain effective private information and respond correctly.Therefore,attack methods based on forged serving network are difficult to interfere the authentication process.In order to verify the security in all scenarios,we apply formal method and automated verification tools to test all possible states in the authentication process.With the advantages such as graphical nature,the simplicity of modelling and the firm mathematical foundation,Petri net is applied for the attack-driven modelling.In our work,Petri net is used to model the authentication process,attack methods and novel scheme.Through the reachability information and state space information of the model,the effectiveness of the attack method and our novel scheme are verified.According to the experimental analysis,several essential security properties are missing in the 5G AKA.It could be found that our novel scheme is resistant to many kinds of attacks based on wireless channel or serving network.