# 5G-AKA-FS: A 5G Authentication and Key Agreement Protocol for Forward Secrecy
## 5 Formal Verification
### Formal Verification via ProVerif
#### 5.2.3 Assertions
The test results provide respectful data for a trade-off between security and resource consumption. #### 6.2.1 Computation Overhead

Table 5 summarizes the environment used in the experiment. The computation overhead for each protocol was measured by conducting 5000 test runs using the cryptography library in Python 3.10.11. As can be seen in a test result shown in Figure 5, 5G-AKA-related protocols have minor differences with 5G-AKA computation overhead. However, these protocols do not completely provide FS. The proposed protocol, with a computation overhead of 6.75 ms, provides FS and has resistance against LBA and AMS. Moreover, as can be seen in comparison with EAP-TLS1.3 and EAP-AKA\({}^{\prime}\)-FS, the increase in computation overhead for providing FS in the proposed protocol is low. The majority of the computation overhead is incurred by ECDH (Elliptic Curve Diffie-Hellman) and digital signature. To provide FS, the protocol must generate a fresh key every session, which 5G-AKA does not do on the HN side, so an increase in overhead to provide FS on protocols is mostly caused by adding fresh ECDH in the key generation phase. In EAP-AKA\({}^{\prime}\)-FS, HN and UE generate fresh ECDH keys in the challenge-response phase. However, the proposed protocol, with the reuse of the fresh ECDH key generated in the initiation phase. In Step 1.1, the proposed protocol computation overhead is optimized. Moreover, unlike EAP-TLS1.3, by a succession of 5G-AKA architecture, the proposed protocol does not require a digital signature. These are the reasons the proposed protocol has lower computation overhead than EAP-TLS1.3 and EAP-AKA\({}^{\prime}\)-FS. Considering that \begin{table}
\begin{tabular}{c c c c c c c} \hline \hline \multirow{2}{*}{**Protocol**} & \multicolumn{6}{c}{**Security Requirements**} \\ \cline{2-7}  & **AUTH** & **SKE** & **LUCS** & **LBA** & **AMS** & **FS** \\ \hline
5G-AKA [3] & & & & & \(\times\) & \(\bigcirc\) & \(\times\) \\ SUCI-AKA [20] & & & & \(\bigcirc\) & \(\times\) & \(\bigcirc\) & \(\times\) \\
5G-IPAKA [17] & & & \(\bigcirc\) & \(\times\) & \(\times\) & \(\times\) & \(\times\) \\
5 GKA-LCCO [21] & & & & \(\times\) & \(\bigcirc\) & \(\bigcirc\) & \(\times\) \\
5G-AKA\({}^{\prime}\)[16] & & & & \(\bigcirc\) & \(\times\) & \(\times\) & \(\times\) \\ EAP-TLS1.3 & & & & \(\times\) & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) \\ EAP-AKA\({}^{\prime}\)-FS & & & & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) & \(\bigcirc\) \\
5G-AKA-FS & & & & & & & \\ \hline \hline \end{tabular} \(\bigcirc\): Support; \(\times\): Not support;

\end{table} 
Table 4: Comparison in terms of security requirements with existing protocols. \begin{table}
\begin{tabular}{l l} \hline \hline Operating System & Windows 11 \\ CPU & 12 th Gen Intel(R) Core(TM) i7-12700 KF \\ GPU & NVIDIA GeForce RTX 3070 Ti \\ RAM & DDR4 64.0 GB \\ Program Language & Python 3.10.11 \\ Library & Cryptography \\ \hline \hline \end{tabular}
\end{table} 
Table 5: Experimental environments. our proposed protocol provides strong security, this level of computational overhead is deemed acceptable. It represents a trade-off that we are willing to accept to prioritize robust security. #### 6.2.2 Communication Overhead

Communication overhead refers to the total message size that needs to be transferred in the network for a specific purpose. Based on the 3 GPP 33.501 specification, we have analyzed the total size of the messages that are exchanged through the primary authentication phase. Table 6 refers to the size of the messages that consist of the 5G primary authentication phase. The combination of upper messages concludes the total communication overhead of the 5G-AKA. Table 7 gives the total communication overhead of 5G-AKA, improved protocols, and for practical comparison EAP-TLS1.3 and EAP-AKA\({}^{\prime}\)-FS. For one protocol to offer additional security properties and inherit the structure of 5G-AKA, it is most likely to use additional messages to fulfill that purpose. As a result, 5G-AKA-FS leads to a higher communication overhead than 5G-AKA.