{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T03:32:07Z","timestamp":1771471927324,"version":"3.50.1"},"reference-count":26,"publisher":"National Library of Serbia","issue":"1","license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ComSIS","COMPUT SCI INF SYST","COMPUT SCI INFORM SY","COMPUTER SCI INFORM","COMSIS J"],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:p>Currently, there is relatively little formal analysis and verification work on the 5G EAP-TLS authentication protocol. In this paper, we use the model checker SPIN to perform a formal analysis of the 5G EAP-TLS authentication protocol. Firstly, we analyze the process of the 5G EAP-TLS authentication protocol and abstract it to obtain a formal model of the protocol. Then, we describe the construction of the protocol model based on the Promela language. The unique feature of this paper is the replacement of the hash value of the 5G EAP-TLS authentication protocol with the message content field encrypted by an unknown subject public key. This is because the Promela language in SPIN has an eval function that can check the value of each field. This can replace the function of the hash function and make the Promela model construction more portable. The paper analyzes the attack paths of the protocol and reveals design flaws that undermine the expected identity authentication attributes and secret consistency of the protocol. The results not only provide a comprehensive understanding of the security properties of the 5G EAP-TLS authentication protocol but also offer valuable insights and guidance for the verification of the protocol's security properties, security design, and optimization of protocol implementation and interoperability.<\/jats:p>","DOI":"10.2298\/csis230611068w","type":"journal-article","created":{"date-parts":[[2023,11,3]],"date-time":"2023-11-03T13:47:36Z","timestamp":1699019256000},"page":"21-36","source":"Crossref","is-referenced-by-count":2,"title":["Applying SPIN checker on 5G EAP-TLS authentication protocol analysis"],"prefix":"10.2298","volume":"21","author":[{"given":"Qianli","family":"Wang","sequence":"first","affiliation":[{"name":"Software School, East China JiaoTong University, Nanchang, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1078","reference":[{"key":"ref1","doi-asserted-by":"crossref","unstructured":"Zhang, J., Yang, L., Cao, W., & Wang, Q. (2020). Formal analysis of 5G EAP-TLS authentication protocol using proverif. IEEE access, 8, 23674-23688. https:\/\/doi.org\/10.1109\/ACCESS.2020.2969474","DOI":"10.1109\/ACCESS.2020.2969474"},{"key":"ref2","unstructured":"3GPP. (2020). Security architecture and procedures for 5G system. Technical Specification (TS) 3GPP TS 33.501 V17. 0.0 (2020-2012)."},{"key":"ref3","doi-asserted-by":"crossref","unstructured":"Dierks, T., & Rescorla, E. (2008). The transport layer security (TLS) protocol version 1.2 (No. rfc5246). https:\/\/doi.org\/10.17487\/RFC5246","DOI":"10.17487\/rfc5246"},{"key":"ref4","doi-asserted-by":"crossref","unstructured":"Basin, D., Cremers, C., Miyazaki, K., Radomirovic, S., & Watanabe, D. (2014). Improving the security of cryptographic protocol standards. IEEE Security & Privacy, 13(3), 24-31. https:\/\/doi.org\/10.1109\/MSP.2013.162","DOI":"10.1109\/MSP.2013.162"},{"key":"ref5","unstructured":"Hirschi, L., Sasse, R., & Dreier, J. (2019). Security issues in the 5G standard and how formal methods come to the rescue. ERCIM News. https:\/\/hal.science\/hal-02268822"},{"key":"ref6","doi-asserted-by":"crossref","unstructured":"Basin, D., Cremers, C., & Meadows, C. (2018). Model checking security protocols. Handbook of Model Checking, 727-762. https:\/\/doi.org\/10.1007\/978-3-319-10575-8_22","DOI":"10.1007\/978-3-319-10575-8_22"},{"key":"ref7","doi-asserted-by":"crossref","unstructured":"Lowe, G. (1995). An attack on the Needham\u2212 Schroeder public\u2212 key authentication protocol. Information processing letters, 56(3). https:\/\/doi.org\/10.1016\/0020-0190(95)00144-2","DOI":"10.1016\/0020-0190(95)00144-2"},{"key":"ref8","doi-asserted-by":"crossref","unstructured":"Mitchell, J. C., Mitchell, M., & Stern, U. (1997, May). Automated analysis of cryptographic protocols using mur\/spl phi. In Proceedings. 1997 IEEE Symposium on Security and Privacy (Cat. No. 97CB36097) (pp. 141-151). IEEE. https:\/\/doi.org\/10.1109\/SECPRI.1997.601329","DOI":"10.1109\/SECPRI.1997.601329"},{"key":"ref9","doi-asserted-by":"crossref","unstructured":"Song, D. X. (1999, June). Athena: a new efficient automatic checker for security protocol analysis. In Proceedings of the 12th IEEE Computer Security Foundations Workshop (pp. 192-202). IEEE. https:\/\/doi.org\/10.1109\/CSFW.1999.779773","DOI":"10.1109\/CSFW.1999.779773"},{"key":"ref10","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Jha, S., & Marrero, W. (2000). Verifying security protocols with Brutus. ACM Transactions on Software Engineering and Methodology (TOSEM), 9(4), 443-487.  https:\/\/doi.org\/10.1145\/363516.363528","DOI":"10.1145\/363516.363528"},{"key":"ref11","doi-asserted-by":"crossref","unstructured":"Armando, A., & Compagna, L. (2004). SATMC: a SAT-based model checker for security protocols. In Logics in Artificial Intelligence: 9th European Conference, JELIA 2004, Lisbon, Portugal, September 27-30, 2004. Proceedings 9 (pp. 730-733). Springer Berlin Heidelberg. https:\/\/doi.org\/10.1007\/978-3-540-30227-8_68","DOI":"10.1007\/978-3-540-30227-8_68"},{"key":"ref12","doi-asserted-by":"crossref","unstructured":"Basin, D., M\u00f6dersheim, S., & Vigano, L. (2005). OFMC: A symbolic model checker for security protocols. International Journal of Information Security, 4, 181-208.  https:\/\/doi.org\/10.1007\/s10207-004-0055-7","DOI":"10.1007\/s10207-004-0055-7"},{"key":"ref13","doi-asserted-by":"crossref","unstructured":"Cortier, V., Delaune, S., & Lafourcade, P. (2006). A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security, 14(1), 1-43.  https:\/\/doi.org\/10.3233\/JCS-2006-14101","DOI":"10.3233\/JCS-2006-14101"},{"key":"ref14","doi-asserted-by":"crossref","unstructured":"Blanchet, B. (2016). Modeling and verifying security protocols with the applied pi calculus and ProVerif. Foundations and Trends\u00ae in Privacy and Security, 1(1-2), 1-135.  http:\/\/dx.doi.org\/10.1561\/3300000004","DOI":"10.1561\/3300000004"},{"key":"ref15","doi-asserted-by":"crossref","unstructured":"Cremers, C., Horvat, M., Hoyland, J., Scott, S., & van der Merwe, T. (2017, October). A comprehensive symbolic analysis of TLS 1.3. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (pp. 1773-1788).  https:\/\/doi.org\/10.1145\/3133956.3134063","DOI":"10.1145\/3133956.3134063"},{"key":"ref16","unstructured":"Chen Liping, Xu Peng, Wang Danchen & Xu Yang. (2022).Formal Verification Research of EAP-TLS Protocol. Computer Science (S2), pp. 685-689. https:\/\/doi.org\/10.11896\/jsjkx.211100111"},{"key":"ref17","unstructured":"Wang Yuedong, Xiong Yan, Huang Wenchao & Wu Jianshuang.(2021). A Formal Analysis Scheme for 5G Private Network Authentication Protocol. Information Network Security(09),1-7. http:\/\/netinfo-security.org\/CN\/10.3969\/j.issn.1671-1122.2021.09.001"},{"key":"ref18","doi-asserted-by":"crossref","unstructured":"Holzmann, G. J. (1997). The model checker SPIN. IEEE Transactions on software engineering, 23(5), 279-295. https:\/\/doi.org\/10.1109\/32.588521","DOI":"10.1109\/32.588521"},{"key":"ref19","doi-asserted-by":"crossref","unstructured":"Maggi, P., & Sisto, R. (2002). Using SPIN to verify security properties of cryptographic protocols. In Model Checking Software: 9th International SPIN Workshop Grenoble, France, April 11-13, 2002 Proceedings 9 (pp. 187-204). Springer Berlin Heidelberg.  https:\/\/doi.org\/10.1007\/3-540-46017-9_14","DOI":"10.1007\/3-540-46017-9_14"},{"key":"ref20","doi-asserted-by":"crossref","unstructured":"Chen, S., Fu, H., & Miao, H. (2016, June). Formal verification of security protocols using Spin. In 2016 IEEE\/ACIS 15th international conference on computer and information science (ICIS) (pp. 1-6). IEEE. https:\/\/doi.org\/10.1109\/ICIS.2016.7550830","DOI":"10.1109\/ICIS.2016.7550830"},{"key":"ref21","doi-asserted-by":"crossref","unstructured":"Xiao, M., Song, W., Yang, K., OuYang, R., & Zhao, H. (2022). Formal Analysis of the Security Protocol with Timestamp Using SPIN. Computational Intelligence and Neuroscience, 2022. https:\/\/doi.org\/10.1155\/2022\/2420590","DOI":"10.1155\/2022\/2420590"},{"key":"ref22","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Leue, S., & Lluch-Lafuente, A. (2004). Directed explicit-state model checking in the validation of communication protocols. International journal on software tools for technology transfer, 5, 247-267. https:\/\/doi.org\/10.1007\/s10009-002-0104-3","DOI":"10.1007\/s10009-002-0104-3"},{"key":"ref23","doi-asserted-by":"crossref","unstructured":"Ninet, T., Legay, A., Maillard, R., Traonouez, L. M., & Zendra, O. (2019, August). Model checking the IKEv2 protocol using Spin. In 2019 17th International Conference on Privacy, Security and Trust (PST) (pp. 1-7). IEEE. https:\/\/doi.org\/10.1109\/PST47121.2019.8949057","DOI":"10.1109\/PST47121.2019.8949057"},{"key":"ref24","doi-asserted-by":"crossref","unstructured":"Galaudage, S., Talbot, C., Nagar, T., Jain, D., Thrane, E., & Mandel, I. (2021). Building better spin models for merging binary black holes: evidence for nonspinning and rapidly spinning nearly aligned subpopulations. The Astrophysical Journal Letters, 921(1), L15. https:\/\/doi.org\/10.3847\/2041-8213\/ac2f3c","DOI":"10.3847\/2041-8213\/ac2f3c"},{"key":"ref25","doi-asserted-by":"crossref","unstructured":"Liu, M. Z., Wu, T. W., S\u00e1nchez, M. S., Valderrama, M. P., Geng, L. S., & Xie, J. J. (2021). Spin-parities of the P c (4440) and P c (4457) in the one-boson-exchange model. Physical Review D, 103(5), 054004. https:\/\/doi.org\/10.1103\/PhysRevD.103.054004","DOI":"10.1103\/PhysRevD.103.054004"},{"key":"ref26","doi-asserted-by":"crossref","unstructured":"Nyangaresi, V. O., Abduljabbar, Z. A., & Abduljabbar, Z. A. (2021, December). Authentication and Key Agreement Protocol for Secure Traffic Signaling in 5G Networks. In 2021 IEEE 2nd International Conference on Signal, Control and Communication (SCC) (pp. 188-193). IEEE. https:\/\/doi.org\/10.1109\/SCC53769.2021.9768338","DOI":"10.1109\/SCC53769.2021.9768338"}],"container-title":["Computer Science and Information Systems"],"original-title":[],"language":"en","deposited":{"date-parts":[[2024,7,30]],"date-time":"2024-07-30T07:22:33Z","timestamp":1722324153000},"score":1,"resource":{"primary":{"URL":"https:\/\/doiserbia.nb.rs\/Article.aspx?ID=1820-02142300068W"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024]]}},"URL":"https:\/\/doi.org\/10.2298\/csis230611068w","relation":{},"ISSN":["1820-0214","2406-1018"],"issn-type":[{"value":"1820-0214","type":"print"},{"value":"2406-1018","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]}}}