# Blockchain-Enabled Secure and Interoperable Authentication Scheme for Metaverse Environments
## 6 Security Analysis
### Formal Security Analysis  
After an informal security analysis, it is essential to formally analyze the proposed scheme. Out of the all of the security issues addressed, mutual authentication among the avatars and devices can be ensured using BAN logic. BAN logic is an analysis method commonly used to verify mutual authentication protocols. Before we start with actual BAN logic analysis, we introduce logical postulates, rules, and goals. Then we prove the mutual authentication protocol using BAN logic. The Table 3 introduces the BAN logic notations used in our analysis.  
\begin{table}
\begin{tabular}{c c} \hline
**Notation** & **Description** \\ \hline P\({}_{1}\),P\({}_{2}\) & Two principals \\ \hline S\({}_{1}\),S\({}_{2}\) & Two statements \\ \hline K & The session key \\ \hline P\({}_{1}\) \(|\equiv\) S\({}_{1}\) & P\({}_{1}\) believes S\({}_{1}\) \\ \hline P\({}_{1}\) \(|\sim\) S\({}_{1}\) & P\({}_{1}\)once said S\({}_{1}\) \\ \hline P\({}_{1}\) \(\Rightarrow\) [PERSON]\({}_{1}\) & P\({}_{1}\)controls S\({}_{1}\) \\ \hline P\({}_{1}\) \(<\)S\({}_{1}\) & P\({}_{1}\)receives S\({}_{1}\) \\ \hline \(\Rightarrow\)S\({}_{1}\) & S\({}_{1}\) is fresh \\ \hline \(\{\$\}_{\text{J}}\)\({}_{\text{K}}\) & S\({}_{1}\) is encrypted with K \\ \hline P\({}_{1}\) \(\leq\)P\({}_{2}\) & P\({}_{1}\) and P\({}_{2}\) have shared key K \\ \hline \end{tabular}
\end{table}
Table 3: Notations for BAN logic analysis.  
\(\text{E5}:\text{MPS}\mid\equiv\text{Ui}\mid\equiv(\text{Ai}\;,\text{PIDi}\;,\text{MPS1})\)  
\(\bullet\) To obtain E6 from Message 2.  
\(\text{E6}:\text{Ui}\triangleleft\text{Ai}\;,\text{PIDi}\;,\text{MPS3},\text{t2}\text{MPS4}\)  
\(\bullet\) Applying MMR using E6 and A3 to obtain E7.  
\(\text{E7}:\text{Ui}\mid\equiv\text{St}\mid\sim(\text{Ai}\;,\text{PIDi}\;, \text{MPS3},\text{t3})\)  
\(\bullet\) Applying FR using E7 and A4 to obtain E8.  
\(\text{E8}:\text{Ui}\mid\equiv\#(\text{Ai}\;,\text{PIDi}\;,\text{MPS3},\text{t2})\)  
\(\bullet\) Applying NVR using E7 and E8 to obtain E9.  
\(\text{E9}:\text{Ui}\mid\equiv\text{MPS1}\equiv(\text{Ai}\;,\text{PIDi}\;, \text{MPS3},\text{t2})\)  
\(\bullet\) Applying BR using E9 to obtain E10.  
\(\text{E10}:\text{Ui}\mid\equiv\text{MPS1}\equiv(\text{Ai}\;,\text{PIDi}\;, \text{MPS3},\text{t2})\)  
\(\bullet\) To obtain E11 using E5. MPS can calculate v2 = h(Ai\mid\text{PIDi}\mid\text{|k|}\mid\text{t2})\),  
\(\text{MPS2}=\text{k}\cdot\text{MPS1}\), and \(\text{MPS4}=\text{v2}\cdot\text{MPS1}\). Then, MPS can successfully generate the session key \(\text{SKi}-\text{MPS}=\text{h(Ai}\;|\;\text{MPS2}\mid\text{MPS4})\).  
\(\text{E11}:\text{MPS1}\equiv\text{Ui}\mid\equiv(\text{Ui}\;\text{SKi}-\text{MPS }\longleftrightarrow\text{MPS})\) (Goal 2)  
\(\bullet\) Applying JR using E11 and A5 to obtain E12.  
\(\text{E12}:\text{MPS1}\equiv(\text{Ui}\;\text{SKi}-\text{MPS}\longleftrightarrow \text{MPS})\) (Goal 1)  
\(\bullet\) To obtain E13 using E10. Ui can calculate v1 = h(Ai\(\;|\;\text{PIDi}\;|\;\text{Xi}\;\text{|t1})\), S2 = v1 \(\cdot\) PK, and \(\text{MPS4}=\text{v1}\cdot\text{MPS3}\). Then, Ui can successfully generate the session key \(\text{SKi}-\text{MPS}=\text{h(Ai}\;|\;\text{\text{MPS2}}|\;\text{MPS4})\).  
\(\text{E13}:\text{Ui}\mid\equiv\text{MPS1}\equiv(\text{Ui}\;\text{SKi}-\text{MPS }\longleftrightarrow\text{MPS})\) (Goal 4)  
\(\bullet\) Applying JR using E10 and A6 to obtain E14.  
\(\text{E14}:\text{Ui}\mid\equiv(\text{Ui}\;\text{SKi}-\text{MPS}\longleftrightarrow \text{MPS})\) (Goal 3)  
Thus, we proved that our scheme guarantees secure mutual authentication between Ui and MPS.