TY - GEN
T1 - A Formal Analysis of Emergency Communication System Based on Model Checking
AU - Liu, Meichen
AU - Li, Hai
N1 - Publisher Copyright:
© 2023 IEEE.
PY - 2023
Y1 - 2023
N2 - Emergency communication system is utilized widely to serve professional mobile communication for public security. Strict inspections must be conducted to ensure the system's high reliability, as inherent protocol complexities and design flaws may cause logical vulnerabilities in protocol implementation. In this paper, we investigate the security of the emergency communication, taking the TETRA system as an example. Specifically, we analyze two critical procedures (i.e., registration and call control) of the TETRA system. As a result, we uncover several potential flaws in the system. Furthermore, to expose vulnerabilities, we apply model checking to the automatic analysis of the TETRA system using the tool NuSMV. At last, we verified our findings in the real TETRA testbed environment. The results show that the attacks can induce service disruption, and the proposed method is feasible to TETRA system analysis.
AB - Emergency communication system is utilized widely to serve professional mobile communication for public security. Strict inspections must be conducted to ensure the system's high reliability, as inherent protocol complexities and design flaws may cause logical vulnerabilities in protocol implementation. In this paper, we investigate the security of the emergency communication, taking the TETRA system as an example. Specifically, we analyze two critical procedures (i.e., registration and call control) of the TETRA system. As a result, we uncover several potential flaws in the system. Furthermore, to expose vulnerabilities, we apply model checking to the automatic analysis of the TETRA system using the tool NuSMV. At last, we verified our findings in the real TETRA testbed environment. The results show that the attacks can induce service disruption, and the proposed method is feasible to TETRA system analysis.
KW - NuSMV
KW - TETRA system
KW - emergency communication
KW - model checking
KW - protocol security
UR - http://www.scopus.com/inward/record.url?scp=85168306319&partnerID=8YFLogxK
U2 - 10.1109/ICEIEC58029.2023.10200747
DO - 10.1109/ICEIEC58029.2023.10200747
M3 - Conference contribution
AN - SCOPUS:85168306319
T3 - ICEIEC 2023 - Proceedings of 2023 IEEE 13th International Conference on Electronics Information and Emergency Communication
SP - 22
EP - 26
BT - ICEIEC 2023 - Proceedings of 2023 IEEE 13th International Conference on Electronics Information and Emergency Communication
A2 - Wenzheng, Li
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 13th IEEE International Conference on Electronics Information and Emergency Communication, ICEIEC 2023
Y2 - 14 July 2023 through 16 July 2023
ER -