# Blockchain-Based Decentralised Authentication in Closed Environments
## 4 Results
### GNY Analysis  
GNY logic is used for proving the correctness of the cryptographic protocol messages. This method allows a step-by-step examination of message components according to specified rules or postulates [21; 22]. In the process of logical reasoning, each entity in the protocol maintains belief and possession sets. Information in both sets can change with each phase of the protocol message exchange. When performing GNY analysis on a protocol, we begin by idealising the protocol message and specifying the initial assumptions. The GNY postulates, i.e., the being-told, possession, freshness, recognisability, message interpretation, and jurisdiction postulates, are then applied to each protocol message. Once the analysis is completed, the protocol must terminate with the expected outcome, such as mutual authentication. On the whole, GNY logic focuses on how protocol principals interpret, trust, and track the logic of cryptographic information exchanged during the execution of a protocol. By using specialised operators (Table 1) and postulates, we can assess potential vulnerabilities and information flows within cryptographic and authentication protocols that might not be apparent through conventional analysis methods. We suppose that \(P\) and \(Q\) are protocol principals (or entities engaging in a protocol message exchange); the annotations used for the analysis are defined in Table 1.  
From the notations in Table 1, the proposed authentication protocol can be idealised as follows. \[ \begin{array}{ll}\textit{Message1}:&V_{i}\triangleleft*ID_{A},*\{*ID_{A},*N _{A},*H(PWD)\}_{K},\\ &*MAC_{K}(*ID_{A},*\{*ID_{A},*N_{A},*H(PWD)\}_{K})\\ \textit{Message2}:&A\triangleleft*ID_{V_{i}},*\{*ID_{V_{i}},ID_{A},*N_{A}+1,*N _{V_{i}},*AuthStatus\}_{K},\\ &*MAC_{K}(*ID_{V_{i}},*\{*ID_{V_{i}},ID_{A},*N_{A}+1,*N_{V_{i}},*AuthStatus \}_{K})\end{array} \] \begin{table}
\begin{tabular}{l l} \hline \hline
**Notation** & **Description** \\ \hline \(P\triangleleft X\) & \(P\) receives statement \(X\). \\ \(P\
i X\) & \(P\) possesses statement (a message or a protocol component) \(X\) and \\  & anything computable from \(X\). \\ \(P\mid\sim X\) & \(P\) once conveyed statement \(X\). \\ \(P\mid\equiv\#(X)\) & \(P\) believes that statement \(X\) is fresh. \\ \(P\mid\equiv\phi(X)\) & \(P\) believes that statement \(X\) is recognisable. \\ \(P\mid\equiv P\triangleleft S\) & \(Q\) believes that \(S\) is a suitable secret shared between \(P\) and \(Q\). \\ \(P\triangleleft*X\) & \(P\) receives statement \(X\) that \(P\) has not conveyed previously. \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Notations of GNY logic. where  
\(V_{i}\) is the validator node \(i\);  
\(A\) is the node to be authenticated;  
\(ID_{x}\) is the identity of node \(x\);  
\(N_{x}\) is the nonce (number used once) generated by node \(x\);  
\(H(PWD)\) is the hash value of the password (\(PWD\));  
\(\{M\}_{K}\) means message \(M\) is encrypted with a symmetric key \(K\);  
\(MAC_{K}(M)\) is the hash value of message \(M\) computed by message authentication code such as CBC-MAC or HMAC with a secret key \(K\). Several assumptions were made prior to the analysis. These assumptions have been explained in the previous section. \(A\
i K\)\(A\mid\equiv A\xleftrightarrow{K}V_{i}\)\(A\mid\equiv\#(N_{V_{i}})\)  
\(V_{i}\
i K\)\(V_{i}\mid\equiv A\xleftrightarrow{K}V_{i}\)\(V_{i}\mid\equiv\#(N_{A})\)  
We then conducted a GNY analysis on each of the protocol message. **Message 1:** We applied the being-told postulates T1 and T3 to obtain \(V_{i}\triangleleft ID_{A},N_{A},H(PWD)\), which meant that the validator nodes \(V_{i}\) that held the group key \(K\) could decrypt the message containing the components \(ID_{A},N_{A},H(PWD)\). Nodes \(V_{i}\) could also apply \(K\) to verify the integrity of the received message. Then, we applied the possession postulate P1 to obtain the fact that the validator nodes \(V_{i}\) possessed the identity of node \(A\), nonce value of \(A\), and hash value of \(A\)'s password.