Formal Analysis of 5G EAP-TLS 1.3

As the fifth-generation mobile network communication technology, 5G supports a wider range of application scenarios with faster speed and lower latency, so the importance of its security cannot be underestimated. Authentication protocols play a crucial role in security as the first safeguard of 5G networks. We provide a formal model of the 5G EAP-TLS 1.3 authentication protocol and perform an automated security analysis using ProVerif, a symbol-based formal verification tool, and our results show that there are some potential flaws in the current protocol design that will cause the protocol to violate the security goals that need to be guaranteed in the standard. To the best of our knowledge, this is the first formal verification study on the 5G EAP-TLS 1.3 protocol.