# 5G-AKA-FS: A 5G Authentication and Key Agreement Protocol for Forward Secrecy
## 5 Formal Verification
### Formal Verification via ProVerif
#### 5.2.3 Assertions
\begin{tabular}{l l} \hline \hline
**Verification Summary** & \\ \hline Query not attacker(skHN[]) is true. & \\ Query not attacker(uk[]) is true. & \\ Query not attacker(SUP[]) is true. & \\ Query event(HNRecReqSN(a)) ===> & event(SNSendReqHN(b)) is true. \\ Query event(SNRecResHN(a)) ===> & event(HNSendResSN(b)) is true. \\ Query event(UERecResSN(a)) ===> & event(SNSendResUE(b)) is true. \\ Query event(SNRecConUE(a)) ===> & event(UESendConSN(b)) is true. \\ Query event(HNRecConSN(a)) ===> & event(SNSendConHN(b)) is true. \\ Query event(SNRecSUPHIN(a)) ===> & event(HNSendSupISN(b)) is true. \\ \hline \hline \end{tabular} 

## 6 Comparative Analysis

In this section, we conduct a comparative assessment aimed at evaluating the effectiveness of the proposed protocol by considering security requirements as well as the computational and communication overheads. For a starter, six protocols are compared against six security requirements to assess the degree of security they each offer. This analysis showcases that the proposed protocol delivers robust security measures in comparison to the others. Next, we proceed to determine the computational overhead linked to each protocol. This involves scrutinizing the amount of cryptographic operations required within each security protocol and quantifying the computational overhead through Python. We also evaluate the communication overhead by closely examining the message dimensions described in the 3 GPP standard document [3]. For that, the transmitted messages are not only inspected, but also their bit sizes are calculated to measure the communication overhead caused by each protocol. ### Security Analysis

The proposed security protocol is compared to the existing protocols based on six security requirements: 5G Network and UE's Mutual Authentication (AUTH), Secure Key Exchange (SKE), Legacy USIM Compatibility Support (LUCS), LinkaBility Attack (LBA), Active attack by Malicious SN (AMS), and Forward Secrecy for \(K_{SEAF}\) (FS). The security requirements that each protocol satisfies are shown in Table 4.

According to the table, all protocols satisfy the requirements for AUTH as well as SKE. However, LUCS is not supported by 5G-IPAKA and 5 GAKA-LCCO. 5G-IPAKA introduces a different structure, which may result in compatibility issues. Similarly, 5 GAKA-LCCO deviates from the standard by utilizing \(T_{SN}\) and follows an unconventional protocol flow, potentially leading to compatibility problems with previous versions, i.e., reverse compatibility problems. LBA is an attack related to compromising a UE's location privacy. 5 GAKA-LCCO eliminates the process of synchronization failure by reducing round-trip, thus preventing LBA. In the case of 5G-AKA\({}^{\prime}\), \(k_{HN}\) is reused instead of \(\mathit{SQN}\), which enables it to confirm the freshness of \(\mathit{MAC}\) and address LBA. On the other hand, 5G-AKA-FS can defend against LBA because it computes \(\mathit{DHK}\) in HN and reflects this key when generating values required for authentication. In 5G-IPAKA and 5G-AKA\({}^{\prime}\), active attacks by malicious SN are possible because the HN delivers \(K_{SEAF}\) to the SN without authentication of the UE. 5G-AKA, SUCI-AKA,and 5G-AKA\({}^{\prime}\) derive the anchor key \(K_{SEAF}\) through the long-term key \(k\), so FS is not supported when \(k\) is leaked. 5G-IPAKA and 5 GAKA-LCCO used not only \(k\) but also HN's private key \(sk_{HN}\) to support FS. However, if \(sk_{HN}\) is compromised, FS for \(K_{SEAF}\) in the past is not achieved. ### Overhead Analysis

To compare the trade-off between security and resource consumption, we have compared the proposed protocol computation and communication overhead. SUCI-AKA, 5G-IPAKA, 5 GAKA-LCCO, and 5G-AKA\({}^{\prime}\) are other protocols improvised based on 5G-AKA. However, they do not provide complete FS. EAP-TLS1.3 and EAP-AKA\({}^{\prime}\)-FS are both representative protocols on the mobile network field and provide complete FS.