# 5G-AKA-FS: A 5G Authentication and Key Agreement Protocol for Forward Secrecy
## 5 Formal Verification
### Formal Verification via ProVerif
#### 5.2.3 Assertions
However, as compensation for this sacrifice, i.e., additional overhead, the proposed protocol offers forward secrecy by newly generating the HN's ephemeral ECDH public key and using it as RAND in the initialization phase. Note that in 5G-AKA RAND is a 128-bit random challenge, but in 5G-AKA-FS the RAND challenge is replaced with the HN's ephemeral ECDH public key, which is 256-bit. This results in 5G-AKA-FS having 384-bit higher communication overhead than 5G-AKA. With only 384-bit extra messages traveling through the network, \begin{table}
\begin{tabular}{l c c c c c c} \hline \hline Message & SUCI &
\begin{tabular}{c} SNN(SN- \\ Name) \\ \end{tabular} & 5G HE AV & 5G SE AV & AUTN & SUPI \\ \hline Bits & 536 & 256 & 640 & 384 & 128 & 60 \\ \hline \hline \end{tabular}
\end{table} 
Table 6: 5G-AKA message size. Figure 5: Total Computation Overhead. 5G-AKA-FS achieves resistance against LBA and AMS and provides FS. Among 5G-AKA-related protocols, 5G-AKA-FS is the only improvised protocol that offers all three security properties. Furthermore, despite its increase, the overhead of 5G-AKA-FS remains lower than that of the EAP-TLS-1.3 protocol and EAP-AKA\({}^{\prime}\)-FS. The analysis results indicate that the addition of 384 extra bits for three crucial security properties are reasonably justifiable trade-offs. ## 7 Further Discussions

The proposed protocol has both advantages on security properties and overheads. However, implementing 5G-AKA-FS presents another challenge. While it is USIM compatible and does not require hardware exchange, software updates are required on both the UE and the 5G Core. Given that the 5G network serves as the infrastructure for connecting a massive number of devices, testing, and simulation are essential before the updates. As for security properties, the proposed 5G-AKA-FS protocol has several limitations. For example, our protocol does not provide resistance to key compromise impersonation attacks since an attacker who obtains a permanent key \(k\) from HN can easily impersonate UE. Also, the proposed protocol does not guarantee security against ephemeral key leakage (e.g., due to side-channel attacks) because the exposure of \(r\) breaks UE anonymity. Additionally, the security of the proposed protocol relies on the safety of the cryptographic key exchange function ECDH. However, the emergence of quantum computing poses a threat to the security of legacy cryptographic algorithms including ECDH. Therefore, future research on quantum-resistant AKA using Post-Quantum Cryptography is required. ## 8 Conclusions

In this paper, we proposed an improved 5G-AKA (5G-AKA-FS) protocol that provides UE unlinkability and forward secrecy, and is compatible with the 3 GPP standard. Implementing the proposed protocol will require the update on UE and 5G Core. However, since it is compatible with the original 5G-AKA it only needs minor software updates. Also, we proved that the 5G-AKA-FS protocol is valid by using formal verification tools BAN Logic and ProVerif. Moreover, we compared the security properties and computation/communication overheads of our 5G-AKA-FS to those of the other existing protocols, including 5G-AKA, SUCI-AKA, 5G-AKA/, 5G-IPAKA, 5 GAKA-LCCO, EAP-TLS 1.3, and EAP-AKA\({}^{\prime}\)-FS. This comparative analysis demonstrates that the proposed protocol effectively maintains a balance between security and efficiency. Conceptualization, I.Y. and S.S.; methodology, I.Y., S.S., J.K. and J.B.; software, G.K., H.K. and J.K.; validation, I.Y., G.K. and J.K.; formal analysis, I.Y., G.K., J.K. and J.B.; investigation, I.Y. and S.S.; writing--original draft preparation, I.Y., G.K., S.S., H.K. and J.K.; writing--review and editing, I.Y., G.K., S.S., H.K., J.K. and J.B.; visualization, G.K. and H.K. ; supervision, I.Y. ; funding acquisition, I.Y. All authors have read and agreed to the published version of the manuscript. This work was supported by the Institute of Information & Communications Technology Planning & Evaluation (IITP) grant funded by the Korean government (MSIT) (No.