@inproceedings{064397680af84c82a62fa59426d90c4f,
title = "Analysis for Threat Models and Improvement Scheme of 5G AKA Protocol Based on Petri-net",
abstract = "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.",
keywords = "5G AKA, Petri net, formal verification",
author = "Zhiping Yan and Chonglin Gu and Hejiao Huang",
note = "Publisher Copyright: {\textcopyright} 2021 IEEE.; 21st IEEE International Conference on Communication Technology, ICCT 2021 ; Conference date: 13-10-2021 Through 16-10-2021",
year = "2021",
doi = "10.1109/ICCT52962.2021.9657852",
language = "英语",
series = "International Conference on Communication Technology Proceedings, ICCT",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "11--17",
booktitle = "2021 IEEE 21st International Conference on Communication Technology, ICCT 2021",
address = "美国",
}