# Formal Verification and Analysis of 5G AKA Protocol Using Mixed Strand Space Model
## 4 Our Proposed 5G-AKA' Protocol and Its Security Analysis
### Mixed Strand Space for the 5G-AKA' Protocol  
**Definition 5**.: _A regular strand space \(\sum_{l}\) is a space for case I of the 5G-AKA' protocol if \(\sum_{l}\) is the union of three kinds of strands: (1) Initiator strands \(s\in\mathit{Init}_{l}[\mathit{UE}\), SN, HN, SUCI, RAND, AUTN, \(RES^{*}]\) with trace: \(<+\mathit{SUCI}\), \(-RAND||AUTN\), \(+RES^{*}>\). The principal associated with this strand is UE. XMAC computed locally is equal to \(MAC\subset AUTN\) and \(SQN\subset AUTN\) is in the correct range (i.e., \(SQN_{\mathit{UE}}<SQN\)); (2) Respender strands \(r\in\mathit{Resp}_{l}[\mathit{UE}\), SN, HN, SUCI, SNN, \(RAND_{SN}\), RAND, \(H_{1}\), \(H_{2}\), \(H_{3}\), Result, \(K_{\mathit{SEAF}}\), \(\mathit{SUPI}]\) with trace: \(<-\mathit{SUCI}\), \(+\{RAND_{SN}||S\mathit{UCI}||SNN\}_{K_{SN,HN}}\), \(-\{RAND_{SN}||S\mathit{UPI}||RAND||H_{1}|H_{2}\}_{K_{SN,HN}}\), \(+RAND||H_{1}\), \(-H_{3}\), \(+\{RAND_{SN}||H_{3}\}_{K_{SN,HN}}\), \(-\{RAND||Result||K_{SEAF}||S\mathit{UPI}\}_{K_{SN,HN}}>\). The principal associated with this strand is SN. \(H_{1}\), \(H_{2}\) and \(H_{3}\) are three messages that are not inspected by SN, where \(H_{2}=SHA256(RAND||H_{3})\); (3) Server strands \(t\in\mathit{Serv}_{l}[\mathit{UE}\), SN, HN, SUCI, SNN, \(RAND_{SN}\), RAND, AUTN, HXRES^{*}\), \(\mathit{RES^{*}}\), Result, \(K_{\mathit{SEAF}}\), \(\mathit{SUPI}]\) with trace: \(<-\{RAND_{SN}||S\mathit{UCI}||SNN\}_{K_{SN,HN}}\), \(+\{RAND_{SN}||S\mathit{UPI}||RAND||AUTN||HXRES^{*}\}_{K_{SN,HN}}\), \(-\{RAND_{SN}||RES^{*}\}_{K_{SN,HN}}+\{RAND||Result||K_{SEAF}||S\mathit{UPI}\}_{K_ {SN,HN}}>\). The principal associated with this strand is HN._  
**Definition 6**.: _A regular strand space \(\sum_{l}\) is a space for case II of the 5G-AKA' protocol if \(\sum_{l}\) is the union of three kinds of strands: (1) Initiator strands \(s\in\mathit{Init}_{l}[\mathit{UE}\), SN, HN, SUCI, RAND, AUTN, \(S\)\(\mathit{syncf}\), AUTS\(]\) with trace: \(<+\mathit{SUCI}\), \(-RAND||AUTN\), \(+S\)\(\mathit{syncf}||AUTTS>\). The principal associated with this strand is UE. XMAC computed locally is equal to \(MAC\subset AUTN\), but \(SQN\subset AUTN\) is not in the correct range (i.e., \(SQN_{\mathit{UE}}\geq SQN\)); (2) Respender strands \(r\in\mathit{Resp}_{l}[\mathit{UE}\), SN, HN, SUPI, SUCI, SNN, \(RAND_{SN}\), RAND, \(H_{1}\), \(H_{2}\), \(\mathit{Syncf}\), \(H_{4}\)] with trace: \(<-\mathit{SUCI}\), \(+\{RAND_{SN}||S\mathit{UCI}||SNN\}_{K_{SN,HN}}\), \(-\{RAND_{SN}||S\mathit{UPI}||RAND||H_{1}||H_{2}\}_{K_{SN,HN}}\), \(+RAND||H_{1}\), \(-\mathit{Syncf}||H_{4}\), \(+\{RAND_{SN}||S\mathit{yncf}||RAND||H_{4}\}_{K_{SN,HN}}>\). The principal associated with this strand is SN. \(H_{1}\), \(H_{2}\) and \(H_{4}\) are three messages that are not inspected by SN; (3) Server strands \(t\in\mathit{Serv}_{l}[\mathit{UE}\), SN, HN, SUPI, SUCI, SNN, \(RAND_{SN}\), RAND, AUTN, HXRES^{*}\), \(\mathit{Syncf}\), AUTS\(]\) with trace: \(<-\{RAND_{SN}||S\mathit{UCI}||SNN\}_{K_{SN,HN}}\), \(+\{RAND_{SN}||S\mathit{UPI}||RAND||AUTN||HXRES^{*}\}_{K_{SN,HN}}\), \(-\{RAND_{SN}||S\mathit{yncf}||RAND\\ ||AUTS\}_{K_{SN,HN}}>\). The principal associated with this strand is HN._  
**Definition 7**.: _An infiltrated strand space \(\sum\mathcal{P}\) is a space for the 5G-AKA' protocol if \(\sum=\sum_{l}\cup\sum_{l}\cup\mathcal{P}\), where penetrator strands \(p\in\mathcal{P}\)[28; 29; 30]._  
Definition 5 gives a regular strand space for case I of the 5G-AKA' protocol (i.e., \(\sum_{l}\)), including initiator strands, responder strands and server strands for case I of the 5G-AKA' protocol. Definition 6 gives a regular strand space for case II of the 5G-AKA' protocol (i.e., \(\sum_{l}\)), including initiator strands, responder strands and server strands for case II of the 5G AKA protocol. Definition 7 gives an infiltrated mixed strand space for the 5G-AKA' protocol, including \(\sum_{l}\), \(\sum_{l}\) and penetrator strands (i.e., \(\mathcal{P}\)).