# 5G-IPAKA: An Improved Primary Authentication and Key Agreement Protocol for 5G Networks
## 5 Formal Verification of the 5G-IPAKA Protocol
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\), then \(SUCI^{\prime\prime}=SUCI\). If \(t\) is a server strand of Definition 2, then \(t\in\text{Serv}_{\Pi}[UE,SN,HN,SUPPI,SUCI,SNN,\)\(RAND^{\prime}{}_{SN},K_{SEAF},RAND\), \(AUTN,HXRES*,\)\(Sprcf,\)\(AUTS^{\prime}]\), where \(SQN^{\prime}{}_{UE}\subset AUTN^{\prime}\). Since \(BK\
otin\mathcal{K}_{P}\), \(MAC-S^{\prime}=f_{1}^{*}(BK,SQN^{\prime}{}_{UE}||RAND||AMF_{0})\subset AUTS^{ \prime}\subset term(<t,3>)\) must originate on an initiator strand \(s^{\prime}\in\text{Init}_{\Pi}[UE,SN,HN,SUCI,RAND^{\prime}{}_{SN},\)\(RAND,\)\(AUTN^{\prime\prime},\)\(Sprcf,\)\(AUTS^{\prime}]\), so \(x\) originates on \(term(<s^{\prime},1>)\). According to Assumption 1, \(x\) originates on \(term(<s,1>)\). Since \(x\) uniquely originates in \(\sum\)\(s^{\prime}=s\). However, \(s^{\prime}\in\text{Init}_{\Pi}\) and \(s\in\text{Init}_{\Pi}\), \(s^{\prime}\
eq s\). Hence, \(t\) is not a server strand of Definition 2. \(\square\)  
Theorem 4.2: _Suppose (1) \(\sum\) is a space for the 5G-IPAKA protocol, and \(\mathcal{C}\) is a bundle containing an initiator strand \(s\in\text{Init}_{\Pi}[UE,SN,HN,SUCI,RAND_{SN},RAND,AUTN,\)\(Sprcf,\)\(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 server strand \(t\in\text{Serv}_{\Pi}[UE,SN,HN,SUPI,SUCI,SNN,RAND_{SN},K_{SEAF},\)\(RAND,\)\(AUTN,HXRES*,\)\(Sprcf,\)\(AUTS]\) and a unique responder strand \(r\in\text{Resp}_{\Pi}[UE,SN,HN,SUPI,SUCI,SNN,RAND_{SN},K_{SEAF},RAND,\)\(AUTN,HXRES*,\)\(Sprcf,\)\(AUTS]\)._  
Proof of Theorem 4.2: Since \(BK=KDF(K,x\cdot y\cdot G||SNN)\), \(BK\
otin\mathcal{K}_{P}\) according to Assumption 2. Because \(MAC=f_{1}(BK,SQN||RAND||AMF)\) and \(RAND\) uniquely originate in \(\sum\)\(MAC\subset AUTN\subset term(<s,2>)\) must uniquely originate on a server strand \(t\) according to Definitions 1-3. If \(t\) is a server strand of Definition 1, then \(t\in\text{Serv}_{\Pi}[UE,SN,HN,SUCI,SNN,RAND^{\prime}{}_{SN},RAND,\)\(AUTN,HXRES*,\)\(RES*\), \(Result,\)\(K_{SEAF},\)\(SUPPI]\). Since \(BK\
otin\mathcal{K}_{P}\), \(CK=f_{3}(BK,RAND)\
otin\mathcal{K}_{P}\) and \(IK=f_{4}(BK,RAND)\
otin\mathcal{K}_{P}\), so \(CK||IK\
otin\mathcal{K}_{P}\). Hence, \(RES*\subset term(<t,3>)\) must originate on an initiator strand \(s^{\prime}\in\text{Init}[UE,SN,HN,SUCI,RAND_{SN},RAND,\)\(AUTN^{\prime\prime},RES*]\), so \(x\) originates on \(term(<s^{\prime},1>)\). According to Assumption 1, \(x\) originates on \(term(<s,1>)\). Since \(x\) uniquely originates in \(\sum\)\(s^{\prime}=s\). However, \(s^{\prime}\in\text{Init}_{\Pi}\) and \(s\in\text{Init}_{\Pi},s^{\prime}\
eq s\). Hence, \(t\) is not a server strand of Definition 1. If \(t\) is a server strand of Definition 2, then \(t\in\text{Serv}_{\Pi}[UE,SN,HN,SUPI,SUCI,SNN,\)\(RAND^{\prime}{}_{SN},RAND,\)\(AUTN,\)\(HXRES*,\)\(Sprcf,\)\(AUTS^{\prime}]\), where \(SQN^{\prime}{}_{UE}\subset AUTS^{\prime}\). Since \(BK\
otin\mathcal{K}_{P}\), \(MAC-S^{\prime}=f_{1}^{*}(BK,SQN^{\prime}{}_{UE}||RAND||AMF_{0})\subset AUTS^{ \prime}\subset term(<t,3>)\) must originate on an initiator strand \(s^{\prime}\). Since \(x\) uniquely originates in \(\sum\)\(s^{\prime}=s\), so \(SQN^{\prime}{}_{UE}=SQN_{UE}\) and \(AUTS^{\prime}=AUTS\). According to \(t\), \(K_{SEAF}\) is encrypted by \(K_{SN,HN}\). According to Assumption 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}||SUPI^{\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}\).