Geodesic
Applying SPIN Checker on 5G EAP-TLS Authentication Protocol Analysis
Computer Science and Information Systems, Tome 21 (2024) no. 1.

Voir la notice de l'article provenant de la source Computer Science and Information Systems website

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.
Keywords: 5G EAP-TLS; SPIN; Formal Analysis; Model Checking 
@article{CSIS_2024_21_1_a5,
     author = {Qianli Wang},
     title = {Applying {SPIN} {Checker} on {5G} {EAP-TLS} {Authentication} {Protocol} {Analysis}},
     journal = {Computer Science and Information Systems},
     publisher = {mathdoc},
     volume = {21},
     number = {1},
     year = {2024},
     url = {http://geodesic.mathdoc.fr/item/CSIS_2024_21_1_a5/}
}
TY  - JOUR
AU  - Qianli Wang
TI  - Applying SPIN Checker on 5G EAP-TLS Authentication Protocol Analysis
JO  - Computer Science and Information Systems
PY  - 2024
VL  - 21
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/CSIS_2024_21_1_a5/
ID  - CSIS_2024_21_1_a5
ER  - 
%0 Journal Article
%A Qianli Wang
%T Applying SPIN Checker on 5G EAP-TLS Authentication Protocol Analysis
%J Computer Science and Information Systems
%D 2024
%V 21
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/CSIS_2024_21_1_a5/
%F CSIS_2024_21_1_a5
Qianli Wang. Applying SPIN Checker on 5G EAP-TLS Authentication Protocol Analysis. Computer Science and Information Systems, Tome 21 (2024) no. 1. http://geodesic.mathdoc.fr/item/CSIS_2024_21_1_a5/