Analysis for Threat Models and Improvement Scheme of 5G AKA Protocol Based on Petri-net

Using 5G Authentication and Key Agreement (AKA) protocol in communication is extremely critical to ensure the security of personal data. In this paper, we apply formal method and automated verification tools to analyze the security properties of 5G AKA protocol. Petri net is applied to model the protocol for its advantages such as having graphical nature and firm mathematical foundation. CPN Tools is used for verification. Based on the reasonable assumptions in this paper, two attack methods mainly occurring in wireless channel and utilizing fake serving network (SN) are proposed. Our automated analysis identifies the effectiveness of each attack method. Finally, in order to improve the reliability of the 5G AKA protocol, we give an enhancement scheme with provably secure fixes. In our novel scheme, the unique id (UNI) is designed for reinforcing the security of messages transmitted in wireless channel, while the challenge-response authentication mechanism is used for ensuring the security of SN.