## 5 Security Analysis
### Result  
Figures 11-13 show the verification results of the three modes of the AKMA TLS 1.3 PSK protocol.  
To check if perfect forward secrecy holds, ProVerif discloses the long-term key \(K_{AKMA}\) in phase 1. In the case of the PSK-only mode, formal verification results indicate that an attacker who obtains the long-term key can recover the past session key and intercept all communication data. On the other hand, the PSK-(EC)DHE and 0-RTT modes do not allow past session keys to be regenerated, even if \(K_{AKMA}\) is compromised. However, in the case of the 0-RTT mode, an attacker can capture and store the ClientHello message and, if managing to obtain \(K_{AKMA}\), retrieve the piggybacked application data. As a result, the PSK-(EC)DHE mode ensures perfect forward secrecy, the 0-RTT mode provides limited perfect forward secrecy, and the PSK-only mode does not ensure perfect forward secrecy. Figure 14 demonstrates an attack breaking perfect forward secrecy in the PSK-Only mode.  
Additionally, all modes--PSK-only, PSK-(EC)DHE, and 0-RTT--are vulnerable to replay attacks. For the PSK-only, PSK-(EC)DHE, and 0-RTT modes, as shown in Figure 15, the server accepts the ClientHello message without being able to verify its freshness, responding to the sender as usual. In this scenario, an attacker who intercepts the message can repeatedly send the same message to the server as if it were a legitimate ClientHello message, causing excessive overhead and leading to a signaling-level replay attack. On the other hand, the 0-RTT mode is vulnerable to data-level replay attacks, including the attack described above, as app data are piggybacked within the ClientHello message.  
Table 3 provides a comparison of the three AKMA TLS 1.3 PSK modes. The verification results show that all three modes are vulnerable to replay attacks. Additionally, the PSK  
\begin{table}
\begin{tabular}{c c} \hline \hline
**Security Requirement** & **Verification Query** \\ \hline \multirow{3}{*}{Confidentiality} & Q4: attacker(App Data1) \\  & Q5: attacker(App Data2) \\  & Q6: attacker(App Data3) \\ \hline \multirow{3}{*}{Integrity} & Q1: inj-event(E\_STEP1\_C\_to\_S) == inj event(S\_STEP1\_C\_to\_S) \\  & Q2: inj-event(E\_STEP2\_S\_to\_C) == inj event(S\_STEP2\_S\_to\_C) \\  & Q3: inj-event(E\_STEP3\_C\_to\_S) == inj-event(S\_STEP3\_C\_to\_S) \\ \hline \multirow{3}{*}{Mutual Authentication} & Q2: inj-event(E\_STEP2\_S\_to\_C) == inj-event(S\_STEP2\_S\_to\_C) \\  & & \& \\  & Q3: inj-event(E\_STEP3\_C\_to\_S) == inj-event(S\_STEP3\_C\_to\_S) \\ \hline \multirow{3}{*}{Secure Key Exchange} & Q2: inj-event(E\_STEP2\_S\_to\_C) == inj-event(S\_STEP2\_S\_to\_C) \\  & Q3: inj-event(E\_STEP3\_C\_to\_S) == inj-event(S\_STEP3\_C\_to\_S) \\ \hline \multirow{3}{*}{Perfect Forward Secrecy} & Q4: attacker(App Data1) \\  & Q5: attacker(App Data2) \\  & Q6: attacker(App Data3) \\ \hline \multirow{3}{*}{Defense against replay attack} & Q1: inj-event(E\_STEP1\_C\_to\_S) == inj-event(S\_STEP1\_C\_to\_S) \\  & Q2: inj-event(E\_STEP2\_S\_to\_C) == inj-event(S\_STEP2\_S\_to\_C) \\  & Q3: inj-event(E\_STEP3\_C\_to\_S) == inj-event(S\_STEP3\_C\_to\_S) \\ \hline \hline \end{tabular}
\end{table}
Table 2: Security requirements verification query.  
only mode does not support a perfect forward secrecy issue, and 0-RTT has a limited perfect forward secrecy problem for the Clienthello piggybacking application data. These findings suggest that improvements are needed for each mode to ensure a secure session connection.