## 8 Conclusions  
In this paper, we study how the three TLS 1.3 PSK modes are applied as the Ua* protocol for AKMA as recommended by TS 33.535 and conduct a formal security analysis of these applications. The results reveal that all three modes are vulnerable to signaling-level replay attacks, as they lack values in the ClientHello message that ensure freshness. Specifically, the PSK-only mode is susceptible to confidentiality breaches due to the complete lack of perfect forward secrecy if the long-term key is compromised. For the 0-RTT mode, the perfect forward secrecy problem arises from the application data piggybacked in the ClientHello message, and it is vulnerable to data-level replay attacks. On the other hand, the PSK-(EC)DHE mode holds confidentiality, integrity, mutual authentication, secure key exchange, and perfect forward secrecy except for the vulnerability to replay attacks. It indicates that the PSK-(EC)DHE mode is the strongest among the three modes. However, compared with the PSK-only and PSK-(EC)DHE modes, the 0-RTT mode achieves significant efficiency in terms of both memory and CPU usage, owing to the simplified handshake process and minimized CPU load. Although there is a slight increase in memory usage due to the retrieval of previously stored session information, the overall overhead is considerably reduced. Therefore, enhancing the security requirements of the ClientHello message in the 0-RTT mode to ensure freshness could potentially address the forward secrecy and replay attack problems, making it the optimal option among the three modes by balancing security and efficiency trade-offs. However, as there are limitations in improving security solely within the 0-RTT mode, further research should focus on ensuring that the AKMA standard can fundamentally address these issues alongside improvements to the 0-RTT mode. Future work aims to perform formal verification from multiple perspectives by incorporating diverse tools such as AVISPA and Scyther, along with verification theories from other domains, such as BAN logic and SVO logic. This multidimensional approach is expected to offer a complementary validation layer that could capture subtle vulnerabilities potentially overlooked when using ProVerif alone. Additionally, while the AKMA protocol addresses security concerns within the 5G convergence environment, limitations may arise in resource-constrained contexts, such as IoT and Ambient Intelligence (AmI), particularly in achieving full forward secrecy, as explained in [24]. To address this, future work will focus on proposing an enhanced version of the PSK-Only or 0-RTT option within AKMA, optimized for minimal computational power. This improvement is anticipated to align the protocol closely with evolving networking contexts, thus supporting the industrial advancement of secure and efficient communication protocols. Moreover, AKMA demonstrates potential value in 5G IoT and edge computing scenarios, particularly in environments where continuous real-time communication is essential, such as remote surgery. This capability positions AKMA as a critical component in applications where maintaining seamless and secure communication is paramount. These prospective applications underscore the protocol's relevance in future 5G-driven domains, aligning it with the demands of high-stakes, latency-sensitive tasks and further enhancing its industrial applicability.