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