A Formal Analysis of The Modified 5G EAP-TLS Protocol
DOI:
https://doi.org/10.54654/isj.v2i28.6385Keywords:
5G security, EAP-TLS, proverif, formal verificationTóm tắt
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.
Downloads
References
GPP TS 33.501 version 18.10.0 Release 18, "TS 133 501 - V18.10.0 - 5G; Security architecture and procedures for 5G System".
J. P. Mattsson and M. Sethi, "EAP-TLS 1.3: Using the Extensible Authentication Protocol with TLS 1.3", Internet Engineering Task Force, Request for Comments RFC 9190, 2022. DOI: 10.17487/RFC9190.
E. Rescorla, "The Transport Layer Security (TLS) Protocol Version 1.3", Internet Engineering Task Force, Request for Comments RFC 8446, 2018. DOI: 10.17487/RFC8446.
G. A. Tuan, N. H. Ha, D. N. Quang, L. H. Ton, and T. T. Hieu, "Weak Links in Smart Surveillance: An Empirical Security Evaluation of Evil Twin Attacks on IoT Cameras", Journal of Science and Technology on Information security, no. 3, vol. 26, pp. 62–69, 2025, DOI: 10.54654/isj.v3i26.1163.
D. Simon, R. Hurst, and B. D. Aboba, "The EAP-TLS Authentication Protocol", Internet Engineering Task Force, Request for Comments RFC 5216, 2008. DOI: 10.17487/RFC5216.
D. Basin, J. Dreier, L. Hirschi, S. Radomirović, R. Sasse, and V. Stettler, "A Formal Analysis of 5G Authentication", Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pp. 1383–1396, 2018. DOI: 10.1145/3243734.3243846.
J. Zhang, L. Yang, W. Cao, and Q. Wang, "Formal Analysis of 5G EAP-TLS Authentication Protocol Using Proverif", IEEE Access, vol. 8, pp. 23674–23688, 2020, DOI: 10.1109/ACCESS.2020.2969474.
N. Zhu, J. Xu, and B. Cui, "Formal Analysis of 5G EAP-TLS 1.3", Advances in Internet, Data & Web Technologies, vol. 193, L. Barolli, Ed., in Lecture Notes on Data Engineering and Communications Technologies, vol. 193. , Cham: Springer Nature Switzerland, pp. 140–151, 2024. DOI: 10.1007/978-3-031-53555-0_14.
M. Shi, J. Chen, Z. Ma, K. He, M. Jia, and R. Du, "A Formal Analysis of 5G EAP-TLS Protocol", IEEE Trans. Netw., vol. 33, no. 5, pp. 2179–2191, 2025, DOI: 10.1109/TON.2025.3556374.
B. Blanchet, "Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif", Foundations and Trends® in Privacy and Security, vol. 1, no. 1–2, pp. 1–135, Oct. 2016, DOI: 10.1561/3300000004.
B. Blanchet, "The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm", Electron. Proc. Theor. Comput. Sci., vol. 373, pp. 14–22, 2022, DOI: 10.4204/EPTCS.373.2.
B. Blanchet, B. Smyth, V. Cheval, and M. Sylvestre, "ProVerif 2.05: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial", 2023.
C. J. F. Cremers, "Unbounded verification, falsification, and characterization of security protocols by pattern refinement", Proceedings of the 15th ACM conference on Computer and communications security, pp. 119–128, 2008. DOI: 10.1145/1455770.1455787.
L. V. Thinh, "Paradigms in Security Protocol Verification: A Multi-Tool Analysis’, Journal of Science and Technology on Information security, no. 3, vol 23, pp. 62–81, 2024, DOI: 10.54654/isj.v3i23.1059.
D. Dolev and A. Yao, ‘On the security of public key protocols", IEEE Transactions on Information Theory, vol. 29, no. 2, pp. 198–208, 1983, DOI: 10.1109/TIT.1983.1056650.
Downloads
Published
How to Cite
Issue
Section
License
Open Access Policy
The Journal of Science and Technology on Information Security provides open access to its published articles to broaden opportunities for high-quality research findings to be available and widely disseminated free of charge, contributing to the greater exchange of knowledge.
Open access statement: CTUJoS permits everyone to read, download, copy, distribute, print, search, or link to the full texts of the published articles without registration, price barriers, or asking for permission from the Journal or the author.
Proposed Policy for Journals That Offer Delayed Open Access
Authors who publish with this journal agree to the following terms:
1. Authors retain copyright and grant the journal right of first publication, with the work [SPECIFY PERIOD OF TIME] after publication simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
2. Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
3. Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work (See The Effect of Open Access).
