## 5 Formal Verification of the 5 GAKA-LCCO Protocol
### Security Proof Based on the Strand Space Model
By assumption (2), \(\{RAND_{\text{SN}}||T^{\prime}_{\text{SN}}||SUCI^{\prime}\) \(||SNN\}_{K_{\text{SN},HN}}=term(<t^{\prime},1>)\) must originate on a respondar strand \(r^{\prime}\in\text{Resp}[UE^{\prime\prime}\), \(SN\), \(HN\), \(SUCI^{\prime\prime}\), \(SNN\), \(RAND_{\text{SN}}\), \(T^{\prime}_{\text{SN}}\), \(RAND^{\prime\prime}\), \(H^{\prime=}_{1}\), \(K^{\prime\prime}_{\text{SEAF}}\), \(SUPI^{\prime\prime}]\). \(RAND_{\text{SN}}\) is uniquely originating in \(\sum\) and \(r^{\prime}=r\), so \(SUCI^{\prime}=SUCI\) and \(T^{\prime}_{\text{${}^{\prime}$}}s_{N}=T_{\text{SN}}\). According to \(t^{\prime}\) and Definition 1, \(UE^{\prime\prime}=UE\), \(SUPI^{\prime}=SUPI\) and \(K^{\prime}_{\text{SEAF}}=K_{\text{SEAF}}\), so \(\{RAND_{\text{SN}}||T_{\text{SN}}||SUCI||SNN\}_{K_{\text{SN},HN}}=term(<t^{ \prime},1>)\). By Definition 1, \(RAND^{\prime}=RAND\) and \(AUTN^{\prime}=AUTN\), i.e., \(t^{\prime}=t\). Hence, \(r\in\text{Resp}[UE\), \(SN\), \(HN\), \(SUCI\), \(SNN\), \(RAND_{\text{SN}}\), \(T_{\text{SN}}\), \(RAND\), \(AUTN\), \(K_{\text{SEAF}}\), \(SUPI]\). \(\square\)According to Theorem 1, \(UE\) successfully authenticates \(HN\) and \(SN\), and can establish an injection agreement [29; 30] with them. Theorem 2: _Suppose: (1) \(\sum\) is a space for the 5 GAKA-LCCO protocol, and \(\mathcal{C}\) is a bundle containing a server strand \(t\in\mathrm{Serv}[UE,SN,HN,SUCI,SNN,RAND_{SN},T_{SN},RAND,\)\(AUTN,K_{SEAF},\) SUPI]; (2) \(K\
otin\mathcal{K}_{P}\) and \(K_{SN,HN}\
otin\mathcal{K}_{P}\); (3) \(x\), \(RAND\) and \(RAND_{SN}\) are uniquely originating in \(\sum\). Then, \(\mathcal{C}\) contains a unique initiator strand \(s\in\mathrm{Init}[UE,SN,HN,SUCI,RAND_{SN},\)\(T_{SN},RAND,\)\(AUTN]\) and a unique responder strand \(r\in\mathrm{Resp}[UE,SN,HN,SUCI,SNN,RAND_{SN},T_{SN},RAND,AUTN,K_{SEAF},\) SUPI]._  
Proof of Theorem 2: Since \(EK||ICB||MK||K_{AUSF}=KDF(K,x\cdot y\cdot G||RAND_{SN}||T_{SN}\;||SNN)\), \(MK\
otin\mathcal{K}_{P}\) according to assumption (2). \(MAC_{UE}=HMAC(MK,\{SUPPI\}_{EK})\), and \(x\) is uniquely originating in \(\sum\) so \(MAC_{UE}\subset\)\(SUCI\subset term(<t,1)\) = must uniquely originate on an initiator strand \(s\in\mathrm{Init}[UE,SN,HN,SUCI,RAND_{SN},T_{SN},RAND^{\prime},\)\(AUTN^{\prime}]\). Similarly, \(MAC^{\prime}=f_{1}(MK,RAND^{\prime}||AMF)\subset AUTN^{\prime}\subset term(<s,3>)\) must originate on a server strand \(t^{\prime}\in\mathrm{Serv}[UE,SN,HN,SUCI,SNN,RAND_{SN},T_{SN},RAND^{\prime},AUTN^{ \prime},K_{SEAF},\) SUPI], so \(\{RAND_{SN}||T_{SN}||SUCI||SNN\}_{K_{SN,HN}}=term(<t^{\prime},1>)\). By Definition 1, \(RAND^{\prime}=RAND\) and \(AUTN^{\prime}=AUTN\), i.e., \(t^{\prime}=t\). Hence, \(s\in\mathrm{Init}[UE,SN,HN,SUCI,RAND_{SN},\)\(T_{SN},RAND,AUTN]\). Since \(RAND_{SN}\) is uniquely originating in \(\sum\)\(\{RAND_{SN}||T_{SN}||SUCI\mid\|SNN\}_{K_{SN,HN}}=term(<t,1>)\) must uniquely originate on a responder strand \(r\in\mathrm{Resp}[UE^{\prime},SN,HN,SUCI,SNN,RAND_{SN},T_{SN},RAND^{\prime\prime},\)\(H^{\prime},K^{*}_{SEAF},\) SUPI\({}^{\prime\prime}]\) according to assumption (2). Similarly, \(\{RAND_{SN}||K^{*}_{SEAF}|SUPPI^{\prime}\}||RAND^{\prime\prime}||H^{\prime}_{1} \}\)\(K_{SN,HN}=term(<r,4>)\) must originate on a server strand \(t^{\prime}\in\mathrm{Serv}[UE^{\prime},SN,HN,SUCI^{\prime\prime},SNN,RAND_{SN},\)\(T^{\prime\prime},SN,RAND^{\prime\prime},\)\(AUTN^{\prime},K^{*}_{SEAF},\)\(SUPPI^{\prime}]\), where \(H^{\prime}_{1}=AUTN^{\prime}\). By assumption (2), \(\{RAND_{SN}||T^{\prime\prime}|SN|SUCI^{\prime\prime}\,||SNN\}_{K_{SN,HN}}=term(<t ^{\prime},1>)\) must originate on a responder strand \(t^{\prime}\in\mathrm{Resp}[UE^{\prime\prime},SN,HN,SUCI^{\prime\prime},SNN,RAND _{SN},T^{\prime\prime},H^{\prime\prime},K^{*\prime\prime},K^{*\prime\prime}, SUPI^{\prime\prime}]\). \(RAND_{SN}\) is uniquely originating in \(\sum\) and \(r^{\prime}=r\), so \(SUCI^{\prime\prime}=SUCI\) and \(T^{\prime\prime}=T_{SN}\).