# Blockchain-Based Multistage Continuous Authentication for Smart Devices
## 6 Scheme Analysis
### Security Evaluation
#### 6.1.2 Logic Proof by BAN Logic  
Formal analysis is an analysis tool commonly used in the design phase of security authentication protocols. The purpose of the analysis is to authenticate the legal identity of the subjects participating in the protocol. The BAN logic analysis of authentication protocols consists of the following four steps:  
1. Protocol idealization: This involves deriving idealized protocols from real agreements. It means that the messages in the protocol are represented in the corresponding BAN logic language;
2. Initial state assumptions: This step identifies the initial belief assumptions and security objectives of the protocol and represents them in logical notation;
3. Logical Reasoning Process: This involves reasoning about messages based on initial assumptions and logical reasoning rules to arrive at the final beliefs of the individual certified entities;
4. Conclusion: The conclusion of the reasoning is analyzed. If the conclusion achieves the purpose for which the protocol was designed, then the protocol is secure; otherwise, the protocol has security flaws. The BAN logic consists of three basic terms: the proposition \(\{X\}\), subject \(\{P,Q\}\), and encryption key \(K\). The notation used in the analysis of BAN logic is shown in Table 4.  
The logical inference rules of the BAN formalize the inference of the authentication protocol. The inference rules specify that \(Y\) is valid if \(X_{1}\), \(X_{2}\), \(\cdots\), and \(X_{n}\) all stand. The following logical rules are considered in this paper:  
1. Message-Meaning Rule (MMR): This rule deals with the interpretation of messages. This formula indicates that \(P\) believes the key \(K\) shared between it and \(Q\) and receives a message \(X\) encrypted with \(K\). Then, \(P\) believes that it was \(Q\) that sent the belief \(X\). \[\textit{Message-Meaning Rule}\ (\textit{MMR}):\frac{P\mid\equiv P\xleftarrow{K}Q,P \triangleleft\{X\}_{K}}{P\mid\equiv Q\mid\sim X}\] (3)
2. Nonce Verification Rule (NVR): This rule defines how to assert that a message is fresh and that the sender believes the message is fresh. The formula expresses that \(P\) believes that \(X\) was sent by \(Q\), and \(P\) believes that \(X\) is fresh. Then, \(P\) believes that \(Q\) sent \(X\) over the course of the protocol. \[\textit{Nonce Verification Rule}\ (NVR):\frac{P\mid\equiv\#(X),P\mid\equiv Q \mid\sim X}{P\mid\equiv Q\mid\sim X}\] (4)
3. Jurisdiction Rule (JR): This rule states that \(P\) believes \(Q\) has jurisdiction. The formula indicates that \(P\) believes \(X\) if \(P\) believes \(Q\) has jurisdiction over \(X\) and trusts \(Q\) to believe \(X\). \[\textit{Jurisdiction Rule}\ (JR):\frac{P\mid\equiv(Q\mid\Rightarrow X),P\mid\equiv(Q \mid\equiv X)}{P\mid\equiv X}\] (5) \begin{table}
\begin{tabular}{c c} \hline \hline
**Notation** & **Description** \\ \hline \(P\mid=X\) & \(P\) believes in the authenticity of statement \(X\). \\ \(\#(X)\) & Statement \(X\) is fresh and has not been sent before. \\ \(P\mid\Rightarrow X\) & \(P\) has jurisdiction over declaration \(X\). \\ \(P\mid\sim X\) & \(P\) once said \(X\). \\ \(P\triangleleft X\) & \(P\) obtains statement \(X\). \\ \(\{X\}_{K}\) & Encryption of statement \(X\) with key \(K\). \\ \(P\xleftarrow{K}Q\) & Communication between \(P\) and \(Q\) with shared key \(K\). \\ \hline \hline \end{tabular}
\end{table} 
Table 4: The BAN logic notations. * Freshness Propagation Rule (FPR): This rule states that if one element of a formula is fresh, then the whole formula is deemed to be fresh. \[Freshness\;Propagation\;Rule\;(FPR):\frac{P\mid\equiv\#(X)}{P\mid\equiv\#(X,Y)}\] (6)
* Belief Rule (BR): Belief rules refer to consistency in the different operations of the cascading and splitting of messages, as well as to the transferability of the beliefs in such operations. \[Belief\;Rule\;(BR):\frac{P\mid\equiv(X,Y)}{P\mid\equiv(X)}\] (7)  
We use \(S_{i}\) for the server and \(U_{i}\) for the user.