## 1 Introduction  
The 5 th Generation Mobile Communication [1] plays a pivotal role in the 4 th Industrial Revolution as well as in the digital transformation paradigm. It accelerates innovations and the integration of state-of-the-art technologies, thereby significantly transforming our daily lives.  
Beyond merely enhancing transmission speeds, 5G addresses the structural limitations of existing networks and drives the development of innovative application services through the deployment of advanced technologies. Accordingly, as shown in Figure 1, the emergence of 5G convergence applications (5G CAPps) utilizing the key characteristics of 5G networks is expected to provide optimized and specialized services to users, thereby driving a paradigm shift in application innovation [2].  
Obviously, robust security is of utmost importance to the 5G cApps environment and paves the way for Beyond 5G and 6G technologies [3]. In particular, a strong and seamless authentication scheme while making great use of existing 5G security standards is preferable to minimize overhead costs. For example, the Authentication and Key Management for Application (AKMA) [4], which was proposed by 3 GPP, offers a seamless authentication process between UE and Application Function (AF) using the security credentials of the former that were generated from the 5G primary authentication [5]. AKMA employs Ua* protocol to securely transmit UE's AKMA identifiers to AFs, either acting as a 5G cAPP or as a middleman. As a strong candidate for the Ua* protocol, Transport Layer Security (TLS) [6] is recommended. Because the Ua* protocol should be secured with AKMA credentials, both the session resumption feature of TLS 1.2 and the Pre-Shared Key (PSK) options of TLS 1.3 can be considered for AKMA. Note that the PSK option of TLS 1.3 includes three modes: PSK-only, PSK-(EC)DHE, and 0-RTT (0 Round-Trip Time). Therefore, for the successful adoption of AKMA, it is necessary to study how to seamlessly integrate AKMA with the aforementioned TLS options. Motivated by this, we conduct comprehensive and systematic research on applying TLS 1.3 PSK modes to AKMA through formal security verification and experimental performance evaluation. This paper focuses on the latest TLS version, TLS 1.3.  
The major contributions of this paper are summarized as follows:  
* We studied how to integrate the three TLS 1.3 PSK modes into the Ua* protocol of AKMA.
* We applied ProVerif [7] to formally and rigorously verify the previously mentioned integration. For this, the ProVerif model was designed and coded with the unbounded session option.
* Finally, we analyzed and compared the applicability and feasibility of combining AKMA with TLS 1.3 PSK modes through experiments while carefully examining the trade-off between efficiency and security.  
The rest of the paper is organized as follows: Section 3 provides an overview of AKMA and TLS 1.3, followed by a description of each PSK mode. Sections 4 and 5 outline the TLS 1.3 AKMA and its formal verification using ProVerif. Section 6 presents the experimental scenarios and performance evaluation results. Finally, the paper is concluded in Section 7.  
Figure 1: Key characteristic and features of 5G network.