## 5 Formal Verification of the 5 GAKA-LCCO Protocol
### Security Proof Based on the Strand Space Model
According to \(t^{\prime}\) and Definition 1, \(UE^{\prime\prime}=UE,SUPPI^{\prime\prime}=SUPI\) and \(K^{\prime\prime}{}_{SEAF}=K_{SEAF}\), so \(\{RAND_{SN}||T_{SN}||SUCI||SNN\}_{K_{SN,HN}}=term(<t^{\prime},1>)\). By Definition 1, \(RAND^{\prime}=RAND\) and \(AUTN^{\prime\prime}=AUTN\), i.e., \(t^{\prime}=t\). Hence, \(r\in\mathrm{Resp}[UE,SN,HN,SUCI,SNN,RAND_{SN},T_{SN},RAND_{SN},\)\(T_{SN},RAND_{SN},\)\(AUTN,K_{SEAF},\) SUPI]. \(\Box\)  
According to Theorem 2, \(HN\) successfully authenticates \(UE\) and \(SN\), and can establish an injection agreement [29; 30] with them. Theorem 3: _Suppose: (1) \(\sum\) is a space for the 5 GAKA-LCCO protocol, and \(\mathcal{C}\) is a bundle containing a responder strand \(r\in\mathrm{Resp}[UE,SN,HN,SUCI,SNN,RAND_{SN},T_{SN},RAND,\)\(H_{1},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 server strand \(t\in\mathrm{Serv}[UE,SN,HN,SUCI,SNN,RAND_{SN},T_{SN},RAND,\)\(T_{SN},RAND,AUTN,K_{SEAF},\) SUPI] and a unique initiator strand \(s\in\mathrm{Init}[UE,SN,HN,SUCI,RAND_{SN},T_{SN},RAND,AUTN]\)._  
Proof of Theorem 3: By assumptions (2) and (3), \(K_{SN,HN}\
otin\mathcal{K}_{P}\), and \(RAND\) is uniquely originating in \(\sum\) so \(\{RAND_{SN}||K_{SEAF}|SUPPI||RAND||H_{1}\}_{K_{SEAH}}=term(<r,4>)\) must uniquely originate on a server strand \(t\in\mathrm{Serv}[UE,SN,HN,SUCI^{\prime},SNN,RAND_{SN},T^{\prime}_{SN},RAND,\)\(AUTN^{\prime},K_{SEAF},\)\(SUPPI]\). Similarly, \(\{RAND_{SN}||T^{\prime}_{SN}||SUCI^{\prime}||SNN\}_{K_{SN,HN}}=term(<t,1>)\) must originate on a responder strand \(r^{\prime}\). \(RAND_{SN}\) is uniquely originating in \(\sum\) and \(r^{\prime}=r\), so \(T^{\prime}_{SN}=T_{SN}\) and \(SUCI^{\prime}=SUCI\) according to assumption (1). According to \(t\) and Definition 1, \(AUTN^{\prime}=AUTN\). Hence, \(t\in\mathrm{Serv}[UE,SN,HN,SUCI,SNN,RAND_{SN},\)\(T_{SN},RAND,\)\(AUTN,K_{SEAF},\)\(SUPPI]\). 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\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\text{Serv}[U\!E,\, SN,\, HN,\, SUCI,\, SNN,\, RAND_{SN},\,T_{SN},\,RAND^{\prime},\,AUTN^{\prime}]\), \(K_{SEAF}\), \(SUPI]\), so \(\{RAND_{SN}||T_{SN}||SUICI||SNN\}_{K_{SN,HN}=term(<t^{\prime},1>)\). By Definition 1, \(RAND^{\prime\prime}=RAND\) and \(AUTN^{\prime\prime}=AUTN\), i.e., \(t^{\prime}=t\). Hence, \(s\in\text{Init}[U\!E,\, SN,\, HN,\, SUCI,\, RAND_{SN},\,T_{SN},\,RAND,\,AUTN]\). \(\square\)  
According to Theorem 3, \(SN\) successfully authenticates \(U\!E\) and \(HN\), and can establish an injection agreement [29; 30] with them. From Theorems 1-3, mutual authentication between the UE and SN, mutual authentication between the UE and SN, and mutual authentication between the SN and HN are established. Additionally, an injection agreement among the UE, SN and HN is established, so replay and MitM attacks among the UE, SN, and HN are overcome according to the definition of the injection agreement [29; 30]. Because MitM attacks among the UE, SN, and HN are overcome, \(K_{SEAF}\) can reach an agreement among the UE, SN, and HN. In addition, replay attacks among the UE, SN, and HN are overcome, so all the messages among the UE, SN, and HN cannot be replayed. As a result, \(SUCI\) cannot be replayed, the location privacy of the UE cannot be compromised, and DoS attacks against both the SN and HN cannot be formed.