Toward an Era of Secure 5G Convergence Applications: Formal Security Verification of 3GPP AKMA with TLS 1.3 PSK Option

The 5th Generation Mobile Communication (5G) plays a significant role in the Fourth Industrial Revolution (4IR), facilitating significant improvements and innovations in various fields. The 3rd Generation Partnership Project (3GPP) is currently standardizing the Authentication and Key Management for Application (AKMA) system for the 5G convergence applications (5G cAPPs). The Transport Layer Security (TLS) is recommended as the application-specific Ua* protocol between User Equipment (UE) and Application Function (AF) to securely transmit the AKMA identifiers of UE as well as guarantee traffic protection. Among TLS protocols, session resumption in TLS 1.2 and the Pre-Shared Key (PSK) modes of TLS 1.3 are particularly desirable for Ua*. Unfortunately, the integration of PSK options of TLS 1.3, namely PSK-only, PSK-(EC)DHE, and 0-RTT (0 Round-Trip Time) modes, with AKMA has not yet been thoroughly investigated; hence, security, performance, compatibility, and effectiveness remain uncertain. In response, this paper explores the integration of the TLS 1.3 PSK options with AKMA and investigates the said metrics by conducting formal security verification and emulating exemplary applications. According to the formal verification and experimental results, the PSK-(EC)DH mode shows a security strength trade-off with efficiency. On the one hand, the 0-RTT mode demonstrates better efficiency but exhibits drawbacks on forward secrecy and replay attacks. The result suggests that 0-RTT mode has to be approved to ensure seamless integration of the TLS 1.3 PSK option with AKMA. In addition, adjustment on the AKMA architecture is also imperative to enhance security level.