Security Analysis of Network Slicing-based Mission-Critical Services with Formal Verification Tool

Mission Critical Service is a service requiring high reliability and low latency, utilized in various fields such as automotive safety systems, disaster safety communications, and medical services. In particular, group communication is essential in disaster scenarios, where the secure delivery of information and user reliability are critical factors. This paper focuses on the user authentication and service authorization procedures for Mission Critical X (MCPTT, MCVideo, MCData), the core components of MCS. The OpenID Connect 1.0 protocol is employed as a key framework for authentication and identity verification, while the TLS protocol ensures the confidentiality and integrity of data. The application procedures of these protocols are elaborated, and the security of the TLS (Transport Layer Security) protocol used in Mission Critical X within the Mission Critical Service environment is analyzed using the formal verification tool BAN-Logic.