# 5G-IPAKA: An Improved Primary Authentication and Key Agreement Protocol for 5G Networks
## 5 Formal Verification of the 5G-IPAKA Protocol
Then, \(\mathcal{C}\) contains a unique server strand \(t\in\text{Serv}_{\text{I}}[UE\), \(SN\), \(HN\), \(SUCI\), \(SNN\), \(RAND_{\text{SN}}\), \(RAND\), \(AUTN\), \(HXRES*\), \(RES*\), Result, \(K_{SEAF}\), \(SUPI]\), and a unique initiator strand \(s\in\text{Init}_{\text{I}}[UE\), \(SN\), \(HN\), \(SUCI\), \(RAND_{\text{SN}}\), \(RAND\), AUTN, \(RES*\)]._  
**Proof of Theorem 5. ** Through Assumptions 2 and 3, \(K_{SN,HN}\
otin\mathcal{K}_{P}\) and \(RAND\) uniquely originates in \(\sum\), so \(\{RAND_{SN}||K_{SEAF}||SUPI||RAND||H_{\text{I}}||H_{\text{2}}\}_{K_{SN,HN}}= term(<r,3>)\) must uniquely originate on a server strand \(t\) according to Definitions 1 to 3. If \(t\) is a server strand of Definition 1, then \(t\in\text{Serv}_{\text{I}}[UE\), \(SN\), \(HN\), \(SUCI^{\prime}\), \(SNN\), \(RAND_{\text{SN}}\), \(RAND\), \(AUTN^{\prime}\), \((HXRES*)^{\prime}\), \((RES*)^{\prime}\), \(Result\), \(K_{SEAF}\), \(SUPI]\), where \(SUPI\subset SUCI^{\prime}\), \(x^{\prime}\subset AUTN^{\prime}\), \(x^{\prime}\subset(HXRES*)^{\prime}\), \(x^{\prime}\subset(RES*)^{\prime}\) and \(K_{SEAF}\) is generated for \(SUPI\). Similarly, \(\{RAND_{SN}||SUCI^{\prime}||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\) and \(x^{\prime}=x\) according to Assumption 1. Hence, \(AUTN^{\prime}=AUTN\), \((HXRES*)^{\prime}=HXRES*\) and \((RES*)^{\prime}=RES*\). 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*=KDF(CK||IK,SNN\)\(||RAND||RES)\subset term(<t,3>)\) must originate on a unique initiator strand \(s\in\text{Init}_{\text{I}}[UE\), \(SN\), \(HN\), \(SUCI\), \(RAND^{\prime}_{\text{SN}}\), \(RAND\), \(AUTN^{\prime\prime}\), \(RES*\)] according to Assumption 3, where \(SQN^{\prime\prime}\subset AUTN^{\prime\prime}\). Similarly, \(MAC^{\prime\prime}\subset AUTN^{\prime\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\prime}=SQN\) and \(AUTN^{\prime\prime}=AUTN\). According to \(t\), \(K_{SEAF}\) is encrypted by \(K_{SN,HN}\). According to Assumption 2, \(K_{SEAF}\
otin\mathcal{K}_{P}\). Because \(MAC_{UE,2}=HMAC(K_{SEAF},RAND_{\text{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}_{\text{SN}}=RAND_{\text{SN}}\). If \(t\) is a server strand of Definition 2, then \(t\in\text{Serv}_{\text{II}}[UE\), \(SN\), \(HN\), \(SUPI\), \(SUCI^{\prime}\), \(SNN\), \(RAND_{\text{SN}}\), \(K_{SEAF}\), \(RAND\), \(AUTN^{\prime}\), \((HXRES*)^{\prime}\), \(S\text{\em v\em c\em v\em c\em v  
**Proof of Theorem 6. ** According to Assumptions 2 and 3, \(K_{SN,HN}\
otin\mathcal{K}_{P}\) and \(RAND\) uniquely originate in \(\sum\), so \(\{RAND_{SN}||K_{SEAF}||SUIPI||RAND||H_{1}||H_{2}\}_{K_{SN,HN}}=term(<r,3>)\) must uniquely originate on a server strand \(t\) according to Definitions 5-7. If \(t\) is a server strand of Definition 1, then \(t\in\text{Serv}_{\text{I}}\{UE,\,SN,\,HN,\,SUICI^{\prime},\,SNN,\,RAND_{SN},\,RAND,\,AUTN^{\prime},\,(HXRES*)^{\prime},\,(RES*)^{\prime},\,Result,\,K_{SEAF},\, SUIPI\}\), where \(SUIPI\subset SUICI^{\prime}\), \(x^{\prime}\subset AUTN^{\prime}\), \(x^{\prime}\subset(HXRES*)^{\prime}\), \(x^{\prime}\subset(RES*)^{\prime}\), and \(K_{SEAF}\) is generated for \(SUIPI\). Similarly, \(\{(RES*)^{\prime}\}_{K_{SN,HN}}=term(<t,3>)\) must originate on a responder strand \(r^{\prime}\in\text{Resp}_{\text{I}}\{UE^{\prime},\,SN,\,HN,\,SUICI^{\prime},\,SNN,\,RAND ^{\prime\prime},\,RN,\,RAND,\,H^{\prime\prime},\,(HXRES*)^{\prime},\,(RES*)^{ \prime}\), \(Result,\,K^{\prime\prime}{}_{SEAF},\,SUPI^{\prime\prime}\).