# 5G-IPAKA: An Improved Primary Authentication and Key Agreement Protocol for 5G Networks
## 5 Formal Verification of the 5G-IPAKA Protocol  
To simplify the formal verification of the 5G-IPAKA protocol, we assume the following:  
**Assumption 1**. : _The parties of the 5G-IPAKA protocol shown in Figure 2 are simplified as the UE, the SN, and the HN;_  
**Assumption 2**. : _There is a session key between the SN and the HN, and it is secure;_  
**Assumption 3**. : _Here, ngKS1 and ABBA do not affect the security of the 5G AKA protocol, so they are ignored._  
According to these assumptions, the 5G-IPAKA protocol shown in Figure 2 can be summarized into two cases as follows:  
Case I: The verification of _AUTN_ succeeds and the authentication is successful. The steps of this case are as follows:  
1. \(\textit{UE}\to\textit{SN}\): \(\textit{SUCI}\);
2. \(\textit{SN}\to\textit{HN}\): \(\{\textit{RAND}_{\textit{SN}}||\textit{SUCI}||\textit{SNN}\}_{\textit{K}_{ \textit{SN},\textit{HN}}}\);
3. \(\textit{HN}\to\textit{SN}\): \(\{\textit{RAND}_{\textit{SN}}||\textit{K}_{\textit{SEAF}}||\textit{SUPI}|| \textit{RAND}||\textit{AUTN}||\textit{HXRES*}\}_{\textit{SN},\textit{HN}}\);
4. \(\textit{SN}\to\textit{UE}\): \(\textit{RAND}_{\textit{SN}}||\textit{RAND}||\textit{AUTN}||\textit{MAC}_{ \textit{SN}}\);
5. \(\textit{UE}\to\textit{SN}\): \(\textit{RES*}||\textit{MAC}_{\textit{UE},2}\);
6. \(\textit{SN}\to\textit{HN}\): \(\{\textit{RES*}\}_{\textit{K}_{\textit{SN},\textit{HN}}}\);
7. \(\textit{HN}\to\textit{SN}\): \(\{\textit{Result}\}_{\textit{K}_{\textit{SN},\textit{HN}}}\). Case II: The verification of _AUTN_ fails and it is a synchronization failure. The steps of this case are as follows:  
1. \(\textit{UE}\to\textit{SN}\): \(\textit{SUCI}\);
2. \(\textit{SN}\to\textit{HN}\): \(\{\textit{RAND}_{\textit{SN}}||\textit{SUCI}||\textit{SNN}\}_{\textit{K}_{ \textit{SN},\textit{HN}}}\);
3. \(\textit{HN}\to\textit{SN}\): \(\{\textit{RAND}_{\textit{SN}}||\textit{K}_{\textit{SEAF}}||\textit{SUPI}|| \textit{RAND}||\textit{AUTN}||\textit{HXRES*}\}_{\textit{K}_{\textit{SN}, \textit{HN}}}\);
4. \(\textit{SN}\to\textit{UE}\): \(\textit{RAND}_{\textit{SN}}||\textit{RAND}||\textit{AUTN}||\textit{MAC}_{ \textit{SN}}\);
5. \(\textit{UE}\to\textit{SN}\): \(\textit{Syrf}||\textit{AUTS}||\textit{MAC}_{\textit{UE},2}\);
6. \(\textit{SN}\to\textit{HN}\): \(\{\textit{Syrc}||\textit{RAND}||\textit{AUTS}\}_{\textit{K}_{\textit{SN}, \textit{HN}}}\). In the above cases, \(K\) on the _UE_ and the _HN_ is replaced with \(\textit{BK}\), where \(\textit{BK}=\textit{KDF}(K,x\cdot y\cdot G||SNN)\). \(\textit{K}_{\textit{SN},\textit{HN}}\) denotes the session key between the _SN_ and the _HN_. The strand space model [28; 29; 30] is a well-studied formal analysis method for security protocols. In [28], the authors studied the case of mixed protocols, where principals use secret material in more than one protocol. In such cases, the two protocols can potentially interact, forming vulnerabilities that are not present in either protocol alone. As mentioned above, there are two cases in the 5G-IPAKA protocol, so there may be interactions between these cases, forming vulnerabilities that do not exist in any single case. Therefore, we use the mixed strand space model [28] to analyze the security of our proposed 5G-IPAKA protocol as follows. Definition 1: A regular strand space \(\sum_{t}\) is a space for case I of the 5G-IPAKA protocol if \(\sum_{t}\) is the union of three kinds of strands: (1) Initiator strands \(s\in\text{Init}_{t}[\text{UE},\,\text{SN},\,\text{HN},\,\text{SUCI},\,\text{ RAND}_{\text{SN}},\,\text{RAND},\,\text{AUTN},\,\text{RES}*]\) with trace: \(<+\text{SUCI},\,-\text{RAND}_{\text{SN}}||\text{RAND}||\text{AUTN}\)\(||\text{MAC}_{\text{SN}},\,+\text{RES}*||\text{MAC}_{\text{UE},2}>\). The principal associated with this strand is UE. \(XMAC\) computed locally is equal to \(\text{MAC}\subset\text{AUTN}\) and \(\text{SQN}\subset\text{AUTN}\) is in the correct range (i.e., \(\text{SQN}_{\text{UE}}<\text{SQN}\)).