## 5 Security Analysis  
In this section, we perform a systematic and comprehensive security analysis of the three modes of AKMA TLS 1.3 PSK using formal verification. The verification process adheres to the ISO/IEC 29128-1:2023 standard [13], which facilitates the mathematical proof of correct operations in cryptographic protocols and the identification of potential vulnerabilities. Tools that comply with standards, such as AVISPA [14], Scyther [15], ProVerif, and Tamarin [16], have been introduced, and various authentication protocols have been verified using these tools [5; 17; 18; 19; 20; 21]. For this purpose, we utilize ProVerif, a state-of-the-art formal verification tool that supports robust verification processes. ProVerif offers exceptional performance and scalability, and its support for attack trace graphs enhances the ease of understanding and diagnosing the causes of potential attacks. Notably, ProVerif's capability to perform 'unbounded' verification, the strongest level specified by the standard, enables a more in-depth and thorough security assessment. The modeling in ProVerif is structured into three primary stages: declarations, process macros, and the main process. As depicted in Algorithm 1, we begin by declaring types, constants, variables, channels, and security verification queries essential for the protocol analysis. Subsequently, we modularly model the UE, AF, and AAnF as process macros in Algorithms 2-4, respectively, facilitating organized and reusable representations of these entities. The main process, illustrated in Algorithms 5 and 6, handles critical operations such as cryptographic key generation and the invocation of subprocesses. To thoroughly verify perfect forward secrecy, we model both unverified and verified versions within the main process. Our verification focuses on essential security requirements, including confidentiality, integrity, mutual authentication, key exchange, perfect forward secrecy, and resistance to replay attacks. For each of these requirements, we define specific queries as outlined in Table 2, enabling targeted and effective analysis of the protocol's security properties. Due to space limitations within this paper, detailed explanations of the ProVerif modeling are condensed; however, the complete and detailed models are publicly available on GitHub (the full ProVerif models can be accessed at [[https://github.com/yonghoko/ProVerif/tree/main/](https://github.com/yonghoko/ProVerif/tree/main/)]([https://github.com/yonghoko/ProVerif/tree/main/](https://github.com/yonghoko/ProVerif/tree/main/)) accessed on 22 November 2024). ```
(* Channel specification *)  free c: channel. free sp: channel [private]. (* Type specification *)  type G, exponent, label, keyid, key. (* Application Data specification *)  free App Data1, App Data2, App Data3: bitstring [private]. (* TLS 1.3 Label specification *)  const p b binder, c traffic ; label. ``` (* Queries specification *)  event S_STEP1_C_to_S(keyid, key, bitstring, bitstring, bitstring). event E_STEP1_C_to_S(keyid, key, bitstring, bitstring, bitstring). event S_STEP2_S_to_C(keyid, key, label, bitstring). event S_STEP3_C_to_S(keyid, key, label, bitstring). event E_STEP3_C_to_S(keyid, key, label, bitstring). ```
(* Security requirements verification *)  query kid: keyid, psk: key, rand: bitstring, binder: bitstring,  ClientHello: bitstring;  Qi: inj-event(E_STEP1_C_to_S(kid, psk, rand, binder, ClientHello)) ==> inj-event(S_STEP1_C_to_S(kid, psk, rand, binder, ClientHello)). query kid: keyid, k: key, Ib_finished: label, aead_finished: bitstring;
``````
Q2:inj-event(E_STEP2_S_to_C(kid, k, lb_finished, aead_finished)) ==>inj-event(S_STEP2_S_to_C(kid, k, lb_finished, aead_finished)). query kid: keyid, k: key, lb_finished: label, aead_finished: bitstring; Q3:inj-event(E_STEP3_C_to_S(kid, k, lb_finished, aead_finished)) ==>inj-event(S_STEP3_C_to_S(kid, k, lb_finished, aead_finished)). (* Secrecy verification *) Q4:query attacker(App Data1). Q5:query attacker(App Data2). Q6:query attacker(App Data3).