## 5 Formal Verification of the 5 GAKA-LCCO Protocol
### Security Proof Based on the Strand Space Model  
The strand space model [29; 30] is a well-studied formal analysis method for security protocols. Therefore, we use the strand space model to analyze the security of our proposed 5 GAKA-LCCO protocol as follows. **Definition 1**. : _An infiltrated strand space \(\sum\), \(\mathcal{P}\) is a space for the 5 GAKA-LCCO protocol if it is the union of four kinds of strands: (1) Initiator strands \(s\in\text{Init}[UE\), \(SN\), \(HN\), \(SUCI\), \(RAND_{\text{SN}}\), \(T_{\text{SN}}\), \(RAND\), \(AUTN\)] with trace: \(<-RAND_{\text{SN}}||T_{\text{SN}}\), \(+SUCI\), \(-RAND||AUTN>\). The principal associated with this strand is UE; (2) Responder strands \(r\in\text{Resp}[UE\), \(SN\), \(HN\), \(SUCI\), \(SNN\), \(RAND_{\text{SN}}\), \(T_{\text{SN}}\), \(RAND\), \(H_{1}\), \(K_{\text{SEAF}}\), \(SUPI]\) with trace: \(<+RAND_{\text{SN}}||T_{\text{SN}}\), \(-SUCI\), \(+\{RAND_{\text{SN}}||T_{\text{SN}}||SUCI||SNN\}_{K_{\text{SN},HN}}\), \(-\{RAND_{\text{SN}}||K_{\text{SEAF}}||SUPI||RAND||H_{1}\}_{K_{\text{SN},HN}}\), \(+RAND||H_{1}>\). The principal associated with this strand is \(SN\). \(H_{1}\) is one message that is not inspected by SN; (3) Server strands \(t\in\text{Serv}[UE\), \(SN\), \(HN\), \(SUCI\), \(SNN\), \(RAND_{\text{SN}}\), \(T_{\text{SN}}\), \(RAND\), \(AUTN\), \(K_{\text{SEAF}}\), \(SUPI]\) with trace: \(<-\{RAND_{\text{SN}}||T_{\text{SN}}||SUCI||SNN\}_{K_{\text{SN},HN}}\), \(+\{RAND_{\text{SN}}||K_{\text{SEAF}}||SUPI||RAND||AUTN\}_{K_{\text{SN},HN}}\). The principal associated with this strand is \(HN\); (4) Penetrator strands \(p\in\mathcal{P}\)[29; 30]._  
**Theorem 1**. : _Suppose: (1) \(\sum\) is a space for the 5 GAKA-LCCO protocol, and \(\mathcal{C}\) is a bundle containing an initiator strand \(s\in\text{Init}[UE\), \(SN\), \(HN\), \(SUCI\), \(RAND_{\text{SN}}\), \(T_{\text{SN}}\), \(RAND\), \(AUTN\)]; (2) \(K\
otin\mathcal{K}_{P}\) and \(K_{\text{SN},HN}\
otin\mathcal{K}_{P}\); (3) \(x\), \(RAND\) and \(RAND_{\text{SN}}\) are uniquely originating in \(\sum\). Then, \(\mathcal{C}\) contains a unique server strand \(t\in\text{Serv}[UE\), \(SN\), \(HN\), \(SUCI\), \(SNN\), \(RAND_{\text{SN}}\), \(T_{\text{SN}}\), \(RAND\), \(AUTN\), \(K_{\text{SEAF}}\), \(SUPI]\) and a unique respondar \(r\in\text{Resp}[UE\), \(SN\), \(HN\), \(SUCI\), \(SNN\), \(RAND_{\text{SN}}\), \(T_{\text{SN}}\), \(RAND\), \(AUTN\), \(K_{\text{SEAF}}\), \(SUPI]\)._  
**Proof of Theorem 1**. : Since \(EK||ICB||MK||K_{\text{AUSF}}=KDF(K,x\cdot y\cdot G||RAND_{\text{SN}}||T_{ \text{SN}}||SNN)\), \(MK\
otin\mathcal{K}_{P}\) according to assumption (2). \(MAC=f_{1}(MK,RAND||AMF)\), and \(RAND\) is uniquely originating in \(\sum\) so \(MAC\subset AUTN\subset term(<s,3>)\) must uniquely originate on a server strand \(t\in\text{Serv}[UE\), \(SN\), \(HN\), \(SUCI\), \(SNN\), \(RAND_{\text{SN}}\), \(T_{\text{SN}}\), \(RAND\), \(AUTN\), \(K_{\text{SEAF}}\), \(SUPI]\). Since \(RAND_{\text{SN}}\) is uniquely originating in \(\sum\)\(\{RAND_{\text{SN}}||T_{\text{SN}}||SUCI||SNN\}_{K_{\text{SN},HN}}=term(<t,1>)\) must uniquely originate on a respondar strand \(r\in\text{Resp}[UE^{\prime}\), \(SN\), \(HN\), \(SUCI\), \(SNN\), \(RAND_{\text{SN}}\), \(T_{\text{SN}}\), \(RAND^{\prime}\), \(H^{\prime}_{1}\), \(K^{\prime}_{\text{SEAF}}\), \(SUPI^{\prime}]\) according to assumption (2). Similarly, \(\{RAND_{\text{SN}}||K^{\prime}_{\text{SEAF}}||SUPI^{\prime}||RAND^{\prime}||H^{ \prime}_{1}\}_{K_{\text{SN},HN}}=term(<r,4>)\) must originate on a server strand \(t^{\prime}\in\text{Serv}[UE^{\prime}\), \(SN\), \(HN\), \(SUCI^{\prime}\), \(SNN\), \(RAND_{\text{SN}}\), \(T^{\prime}_{\text{SN}}\), \(RAND^{\prime}\), \(AUTN^{\prime}\), \(K^{\prime}_{\text{SEAF}}\), \(SUPI^{\prime}]\), where \(H^{\prime}_{1}=AUTN^{\prime}\).