A Formal Analysis of The Modified 5G EAP-TLS Protocol
TL;DR
A detailed description of the steps in the modified EAP-TLS protocol is presented, which addresses issues by directly binding the digital certificate to the subscriber’s SUCI identity to prevent user impersonation, binding the session key to both the certificate and the identity to ensure resistance against Man-in-The-Middle attacks, and introducing a nonce value to prevent the reuse of old packets in replay attacks.
Abstract
The 5G EAP-TLS protocol is one of the three protocols standardised by 3GPP for use in 5G networks. Although this protocol inherently ensures security, authentication, and data integrity, recent studies have shown that it still faces several vulnerabilities, including Man-in-The-Middle attacks, user impersonation, and replay attacks. This paper presents a detailed description of the steps in the modified EAP-TLS protocol, which addresses these issues by directly binding the digital certificate to the subscriber’s SUCI identity to prevent user impersonation, binding the session key to both the certificate and the identity to ensure resistance against Man-in-The-Middle attacks, and introducing a nonce value to prevent the reuse of old packets in replay attacks. The paper employs the Proverif tool as a formal verification approach to evaluate the security of the modified 5G EAP-TLS protocol. The verification outcomes indicate that the proposed protocol satisfies the specified security properties, including the confidentiality of the session key (KSESSION), the subscriber identity (SUPI), the pre-master key (RPREKEY), as well as other relevant security requirements.