# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 5 Discussion  
### Security of the 5G-AKA' Protocol  
According to the above security analysis of the latest version of the 5G AKA protocol, twenty-one attack scenarios can be obtained, where thirteen attack scenarios are related to \(MACf\). In our proposed 5G-AKA' protocol, \(MACf\) is replaced with a timeout mechanism on the HN, so the thirteen attack scenarios are eliminated. As a result, those attacks in the thirteen attack scenarios are eliminated, including MAC failure attacks. Without considering \(MACf\), the comparative analysis of authentication properties [28; 29; 30] between the latest version of the 5G AKA protocol and our proposed 5G-AKA' protocol is shown in Table 1.  
From Table 1, in the latest version of the 5G AKA protocol, only the weaker agreement can be established, and even weak agreement cannot be established in the cases of \"UE to SN\" and \"SN to UE\", because the UE cannot authenticate the SN, and the SN cannot authenticate the UE. However, in our proposed 5G-AKA' protocol, mutual authentication and injection agreement among the UE, the SN and the HN can be established in all cases according to the security analysis of the 5G-AKA' protocol. According to the above security analysis of the latest version of the 5G AKA protocol, based on those missing agreements, the penetrator can perform MitM attacks and cross attacks. Additionally, based on replayed messages, replay attacks and masquerading attacks can be performed, the location privacy of the UE can be compromised and DoS attacks on the SN can be formed. However, according to the above security analysis of the 5G-AKA' protocol, our proposed 5G-AKA' protocol has overcome these attacks. In terms of secrecy properties, the keys established in the latest version of the 5G AKA protocol are secret. However, if \(K\) is leaked, then the attacker can calculate \(K_{AUSF}\) and \(K_{SEAF}\) based on those messages transmitted in the past run of the protocol. As a result, the attacker can decrypt those encrypted messages transmitted in the past run of the protocol. Therefore, the latest version of the 5G AKA protocol does not provide perfect forward secrecy. However, in our proposed 5G-AKA' protocol, \(K\) is replaced with \(BK=KDF(K,x\cdot y\cdot G||SNN)\), providing perfect forward secrecy based on Diffie-Hellman exchange. Therefore, our proposed 5G-AKA' protocol is secure and can overcome those security problems of the latest version of the 5G AKA protocol. The comparative analysis of security properties between the 5G-AKA' protocol and some recently improved 5G AKA protocols [22; 23; 24] is shown in Table 2.  
From Table 2, only some security properties can be guaranteed in the 5G AKA protocol and these recently improved 5G AKA protocols, but all security properties can be guaranteed in our proposed 5G-AKA' protocol. In [22], \(AUTN\) contains the challenge of the UE (i.e., \(r_{UE}\)), so the first received message of the UE cannot be a replayed message, preventing the location privacy of the UE from being compromised. However, \(AUTN\) does not contains \(SNN\), so the UE cannot authenticate \begin{table}
\begin{tabular}{c c c c c c c c} \hline \hline
**Protocols** & **Authentication Properties** & **UE to SN** & **UE to HN** & **SN to UE** & **SN to HN** & **HN to UE** & **HN to SN** \\ \hline \multirow{5}{*}{5G AKA} & Injection agreement & No & No & No & No & No & No \\  & Non-injection agreement & No & No & No & No & No & No \\  & Weaker agreement & No & Yes & No & Yes & Yes & Yes \\ \hline \multirow{5}{*}{5G-AKA’} & Injection agreement & Yes & Yes & Yes & Yes & Yes & Yes \\  & Non-injection agreement & No & No & No & No & No & No \\  & Weaker agreement & No & No & No & No & No & No \\ \hline \hline \end{tabular}
\end{table} 
Table 1: The comparative analysis of authentication properties between the two protocols.