Formal Verification of 5G-EAP-TLS Authentication Protocol

In mobile communication networks, the security of users' data depends on the guarantees provided by the authentication protocols. For the next generation of mobile network (i.e., 5G network), the 5G-EAP-TLS protocol has been proposed for this purpose. However, it is still unknown whether this protocol provides the claimed security guarantees or not. To fill this gap, we provide in this work the first formal model of 5G-EAP-TLS protocol and conduct a thorough analysis based on Scyther model checker. Secondly, we identify several design flaws in the protocol, which may jeopardize the security goals and result in severe security vulnerabilities when implemented in real systems. To our knowledge, this is the first study on the formal verification of 5G-EAP-TLS protocol.