# 5G-IPAKA: An Improved Primary Authentication and Key Agreement Protocol for 5G Networks
## 5 Formal Verification of the 5G-IPAKA Protocol
According to Assumption 2, \(\{Syncf||RAND||AUTS\}_{K_{SN,HN}}=term(<t,3>)\) must originate on a responder strand \(r^{\prime}\) in \(\text{Resp}_{\Pi}[UE^{\prime\prime},SN,HN,SUPI^{\prime\prime},SUCI^{\prime\prime}, SNN,RAND^{\prime\prime}{}_{SN},K^{\prime\prime}{}_{SEAF},RAND,\)\(H^{\prime\prime}{}_{1},H^{\prime\prime\prime},\)\(Sprcf,\)\(AUTS]\), where \(SUPI^{\prime\prime}{}^{\prime\prime}\subset SUCI^{\prime\prime}\). Similarly, \(\{RAND^{\prime}{}_{SN}||K^{\prime\prime}{}_{SEAF}||SUPI^{\prime\prime}||RAND ||H^{\prime\prime}{}_{1}||H^{\prime\prime\prime}{}_{2}\}_{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}{}_{SN}=RAND_{SN}\)\(K^{\prime\prime}{}_{SEAF}=K_{SEAF}\), \(H^{\prime\prime}{}_{1}=AUTN\), \(H^{\prime\prime}{}_{2}=HXRES*\), \(SUPI^{\prime\prime}=SUPI\) and \(UE^{\prime\prime}=UE\). Similarly, \(\{RAND_{SN}||SUCI||SNN\}_{K_{SN,HN}}=term(<t,1>)\) must originate on a responder strand \(r^{\prime\prime}\). Since \(RAND_{SN}\) uniquely originates in \(\sum r^{\prime\prime}=r^{\prime}=r\), so \(SUCI^{\prime\prime}=SUCI\). \(\square\)  
According to Theorems 1 and 2, \(UE\) successfully authenticates \(HN\) and \(SN\), and injection agreement [28; 29; 30] can be established. Theorem 3.1: _Suppose (1) \(\sum\) is a space for the 5G-IPAK protocol, and \(\mathcal{C}\) is a bundle containing a server strand \(t\in\text{Serv}_{\text{I}}[UE,\,SN,\,HN,\,SUCI,\,SNN,\,RAND_{SN},\,RAND,\,AUTN,\, HXRES*\), \(RES*\), Result, \(K_{SEAF}\), \(SUPI\)]; (2) \(K\
otin\mathcal{K}_{P}\) and \(K_{SN,HN}\
otin\mathcal{K}_{P}\); (3) \(x\), \(RAND\), \(RAND_{SN}\) uniquely originates in \(\sum\). Then, \(\mathcal{C}\) contains a unique initiator strand \(s\in\text{Init}_{\text{I}}[UE,\,SN,\,HN,\,SUCI,\,RAND_{SN},\,RAND,\,AUTN,\, RES*]\) and a unique responder strand \(r\in\text{Resp}_{\text{I}}[UE,\,SN,\,HN,\,SUCI,\,SNN,\,RAND_{SN},\,RAND,\,AUTN,\, HXRES*\), \(RES*\), Result, \(K_{SEAF}\), \(SUPI\)]._  
Proof of Theorem 3.1.: Since \(BK=KDF(K,x\cdot y\cdot G||SNN)\), \(BK\
otin\mathcal{K}_{P}\) according to Assumption 2. Because \(CK=f_{3}(BK,RAND)\) and \(IK=f_{4}(BK,RAND)\), \(CK\
otin\mathcal{K}_{P}\), and \(IK\
otin\mathcal{K}_{P}\), so \(CK||IK\
otin\mathcal{K}_{P}\). Hence, \(RES*\gets KDF(CK||IK,SNN||RAND||RES)\subset term(<t,3>)\) must originate on an unique initiator strand \(s\in\text{Init}_{\text{I}}[UE,\,SN,\,HN,\,SUCI,\,RAND^{\prime}{}_{SN},\,RAND,\,AUTN^{ \prime},\,RES*]\) according to Assumption 3, where \(SQN^{\prime}\subset AUTN^{\prime}\). Similarly, \(MAC^{\prime}\subset AUTN^{\prime}\subset term(<s,2>)\) must originate on a server strand \(t^{\prime}\). Since \(RAND\) uniquely originates in \(\sum\), \(t^{\prime}=t\), so \(SQN^{\prime}=SQN\) and \(AUTN^{\prime}=AUTN\). According to Assumption 2, \(\{RES*\}_{K_{SN,HN}}=term(<t,3>)\) must originate on a responder strand \(r\in\text{Resp}_{\text{I}}[UE^{\prime},\,SN,\,HN,\,SUCI^{\prime},\, SNN,\,RAND^{\prime}{}_{SN},\,RAND,\,H^{\prime\prime}{}_{1},\,HXRES*\), \(RES*\), Result, \(K^{\prime}{}_{SEAF},\,SUPI^{\prime\prime}]\), where \(SUPI^{\prime\prime}\subset SUCI^{\prime}\). Similarly, \(\{RAND^{\prime}{}_{SN}||K^{\prime\prime}{}_{SEAF}||SUPI^{\prime\prime}||RAND ||H^{\prime\prime}{}_{1}||HXRES*\}_{K_{SN,HN}}=term(<r,3>)\) must originate on a server strand \(t^{\prime\prime}\). Since \(RAND\) uniquely originates in \(\sum\)\(t^{\prime\prime}=t\), so \(RAND^{\prime}{}_{SN}=RAND_{SN}\), \(K^{\prime}{}_{SEAF}=K_{SEAF}\), \(H^{\prime\prime}{}_{1}=AUTN\), \(SUPI^{\prime\prime}=SUPI\) and \(UE^{\prime\prime}=UE\). Similarly, \(\{RAND_{SN}||SUCI||SNN\}_{K_{SN,HN}}=term(<t,1>)\) must originate on a responder strand \(r^{\prime}\). Since \(RAND_{SN}\) uniquely originates in \(\sum\), \(r^{\prime}=r\), so \(SUCI^{\prime}=SUCI\). According to \(t\), \(K_{SEAF}\) is encrypted by \(K_{SN,HN}\). According to Assumption 2, \(K_{SEAF}\
otin\mathcal{K}_{P}\).