A Formal Analysis of 5G EAP-TLS Protocol

The emergence of private 5G networks has garnered significant attention from enterprises. To ensure the security of communication devices within these networks, the 3GPP group proposed the 5G Extensible Authentication Protocol-Transport Layer Security (EAP-TLS). Despite its critical role, the security of 5G EAP-TLS has not been systematically studied. In this paper, we present the first comprehensive formal model of the 5G EAP-TLS protocol, detailing its flow and incorporating all parties and the certificate distribution mechanism as defined by the 5G specification. Additionally, we extract and interpret the security requirements outlined in the specification. Using the automated symbolic tool Tamarin, we analyze the protocol’s security goals and identify potential vulnerabilities. We propose and verify solutions to these issues, enhancing the protocol’s security. This work provides a foundational understanding and improvements for securing private 5G networks.