A Coloured Petri Nets Model of the 5G Authentication and Key Agreement Protocol

Abstract

Background: The security in 5G networks must safeguard network functions and other components responsible for end-to-end communications, intending to provide confidentiality, integrity, availability, authenticity, and non-repudiation. Some security functions that protect 5G networks are part of relevant protocols such as the 5G Authentication and Key Agreement (5G-AKA). However, the 5G-AKA protocol has some limitations, becoming susceptible to attacks such as replay and man-in-the-middle. Results: Aiming to analyze the 5G-AKA protocol regarding security properties and help to identify possible vulnerabilities and threats, we used coloured Petri nets to model the protocol's components, their interactions, and an example of an attack scenario. We validated the model using simulations and the model-checking technique. Conclusions: This model may help improve the security of 5G networks by validating properties and behaviors using simulations and formal verification. The proposed 5G-AKA model can be a relevant tool for identifying vulnerabilities and proposing mitigation measures for different 5G topologies.