About the journal

• Home page
• Contact information
• Aims and scope
• Indexing information
• Editorial policies
• ComSIS consortium
• Journal boards
• Managing board

For authors

• Information for contributors
• Paper submission
• Article submission through OJS
• Copyright transfer form
• Download section

For readers

• Forthcoming articles
• Current issue
• Archive

For reviewers

• View and review submissions

News

• Journal's Facebook page
• Calls for special issues
• New issue notification

Applying SPIN Checker on 5G EAP-TLS Authentication Protocol Analysis

Qianli Wang¹

1. Software School, East China JiaoTong University,
   Nanchang, China
   qianjustice2@163.com

Abstract

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.

Key words

5G EAP-TLS; SPIN; Formal Analysis; Model Checking

Digital Object Identifier (DOI)

https://doi.org/10.2298/CSIS230611068W

Publication information

Volume 21, Issue 1 (January 2024)
Year of Publication: 2024
ISSN: 2406-1018 (Online)
Publisher: ComSIS Consortium

Full text

Available in PDF
Portable Document Format

How to cite

Wang, Q.: Applying SPIN Checker on 5G EAP-TLS Authentication Protocol Analysis. Computer Science and Information Systems, Vol. 21, No. 1, 21–36. (2024), https://doi.org/10.2298/CSIS230611068W