# 5G-IPAKA: An Improved Primary Authentication and Key Agreement Protocol for 5G Networks
## 5 Formal Verification of the 5G-IPAKA Protocol
(2) Responder strands \(r\in\text{Resp}_{t}[\text{UE},\,\text{SN},\,\text{HN},\,\text{SUCI},\,\text{ SNN},\,\text{RAND}_{\text{SN}},\,\text{RAND},\,\text{H}_{1},\,\text{H}_{2},\,\text{H}_{3},\,\text{ Result},\,\text{K}_{\text{SEAF}},\,\text{SUPI}]\) with trace: \(<-\text{SUCI},\,+\{\text{RAND}_{\text{SN}}||\text{SUCI}||\text{SNN}\}_{ \text{K}_{\text{SN},HN^{\prime}}},\,-\{\text{RAND}_{\text{SN}}||\text{K}_{ \text{SEAF}}||\text{SUPI}|\,|\text{RAND}||\text{H}_{1}||\text{H}_{2}\}_{\text{ K}_{\text{SN},HN^{\prime}}},\,+\,\text{RAND}_{\text{SN}}||\text{RAND}||\text{H}_{1}|| \text{MAC}_{\text{SN}},\,-\,\text{H}_{3}||\text{MAC}_{\text{UE},2},+\{H_{3}\} _{\text{K}_{\text{SN},HN}},-\{\text{Result}\}_{\text{K}_{\text{SN},HN}}>\). The principal associated with this strand is \(\text{SN}\). \(H_{1}\), \(H_{2}\) and \(H_{3}\) are three messages that are not inspected by SN, where \(H_{2}=SHA256(RAND||H_{3})\). (3) Server strands \(t\in\text{Serv}_{t}[\text{UE},\,\text{SN},\,\text{HN},\,\text{SUCI},\,\text{ SNN},\,\text{RAND}_{\text{SN}},\,\text{RAND},\,\text{AUTN},\,\text{H}_{2} *,\,\text{RES}*,\,\text{Result},\,\text{K}_{\text{SEAF}},\,\text{SUPI}]\) with trace: \(<\quad-\{\text{RAND}_{\text{SN}}||\text{SUCI}||\text{SNN}\}_{\text{K}_{ \text{SN},HN^{\prime}}},\,+\{\text{RAND}_{\text{SN}}||\text{K}_{\text{SEAF}}| \text{SUPI}\quad||\text{RAND}||\text{AUTN}||\)\(HXRES*\}_{\text{K}_{\text{SN},HN}},\,-\{\text{RES}*\}_{\text{K}_{\text{SN},HN^{\prime}}},\,+\{\text{Result}\}_{\text{K}_{\text{SN},HN}}>\). The principal associated with this strand is \(\text{HN}\). Definition 2: A regular strand space \(\sum_{t}\) is a space for case II 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{Syncf},\,\text{AUTS}]\) with trace: \(<+\text{SUCI},\,-\text{RAND}_{\text{SN}}||\text{RAND}\)\(||\text{AUTN}||\text{MAC}_{\text{SN}},\,+\text{Syncf}||\text{AUTS}||\text{MAC}_{\text{UE},2}>\). The principal associated with this strand is UE. \(XMAC\) computed locally is equal to \(\text{MAC}\subset\text{AUTN}\), but \(\text{SQN}\subset\text{AUTN}\) is not in the correct range (i.e., \(\text{SQN}_{\text{UE}}\geq\text{SQN}\)). (2) Responder strands \(r\in\text{Resp}_{t}[\text{UE},\,\text{SN},\,\text{HN},\,\text{SUPI},\,\text{ SUCI},\,\text{SNN},\,\text{RAND}_{\text{SN}},\,\text{K}_{\text{SEAF}},\,\text{RAND},\,\text{H}_{1},\,\text{H}_{2},\,\text{Syncf},\,\text{H}_{4}]\) with trace: \(<-\text{SUCI},\,+\{\text{RAND}_{\text{SN}}||\text{SUCI}||\text{SNN}\}_{ \text{K}_{\text{SEAF}}||\text{SUCI}||\text{RAND}||\text{H}_{1}\,\,\text{|H}_{2} \}_{\text{K}_{\text{SN},HN}}  
tion 2, \(K_{SEAF}\
otin\mathcal{K}_{P}\). Because \(MAC_{SN}=HMAC(K_{SEAF},RAND_{SN}||RAND\ ||AUTN),\)\(MAC_{SN}\subset term(<s,2>)\) must originate on a responder strand \(r\). According to Assumption 2, \(\{RAND_{SN}||K_{SEAF}||SUP^{\prime\prime}||RAND||AUTN||H^{\prime\prime}\}_{K_{SN,HN }}=term(<r,3>)\) must originate on a server strand \(t^{\prime}\). Since \(RAND\) uniquely originates in \(\sum\), \(t^{\prime}=t\), so \(RAND^{\prime}{}_{SN}=RAND_{SN}\). According to Assumption 2, \(\{RES*\}_{K_{SN},HN}=term(<t,3>)\) must originate on a responder strand \(r^{\prime}\in\text{Resp}_{1}[UE^{\prime\prime},SN,HN,SUCI^{\prime\prime}, SNN,RAND^{\prime\prime}{}_{SN},\)\(RAND,\)\(H^{\prime\prime}{}_{1},HXRES*,\)\(RES*\), Result, \(K^{\prime\prime}{}_{SEAF},SUP^{\prime\prime}]\), where \(SUP^{\prime\prime}\subset SUCI^{\prime\prime}\). Similarly, \(\{RAND^{\prime\prime}{}_{SN}||K^{\prime\prime}{}_{SEAF}||SUP^{\prime\prime} ||RAND||H^{\prime\prime}{}_{1}||HXRES*\}_{K_{SN,HN}}=term(<r^{\prime},3>)\) must originate on a server strand \(t^{\prime\prime}\). Since \(RAND\) uniquely originates in \(\sum\)\(t^{\prime\prime}=t\), so \(RAND^{\prime\prime}{}_{SN}=RAND_{SN}\), \(K^{\prime\prime}{}_{SEAF}=K_{SEAF}\), \(H^{\prime\prime}{}_{1}=AUTN\), \(SUP^{\prime\prime}{}^{\prime\prime}=SUP\) and \(UE^{\prime\prime}{}=UE\).