## 2 Materials and Methods
### Proof of Authentication Using BAN Logic  
This section applies the Burrows-Abadi-Needham logic (BAN) to the proposed scheme to conduct a formal analysis. The BAN logic [50; 51] is used widely to ensure the security of the key agreement-based authentication protocol [24; 29; 44]. First, communication parties establish the protocol's accuracy: the user Ui and the sensor node \(\mathsf{Sn}\), which exchange a freshly formed session key after the execution of the protocol. We begin by illustrating the BAN logic with the following specific notations:  
* \(P|\equiv X\): The principal [PERSON] is convinced that the announcement X is valid. * \(P\triangleleft X\): [PERSON] examines X, which indicates that [PERSON] has received a message containing X that can be read by [PERSON]. * \(P|\sim X\): [PERSON] once stated X, which signifies that [PERSON] \(|\) X as [PERSON] once said it sometime. * \(P|\Rightarrow X\): [PERSON] commands X completely, believing X is trustworthy (Jurisdiction over X). Figure 10: Authentication phase (Case 2). Figure 9: Authentication phase (Case 1). * \(\#(X)\): Because the message X is new, no entity has previously sent a message containing X. * \(P|\equiv Q\xleftrightarrow{SK}P\): [PERSON] and [PERSON] communicate via SK (shared key). * \(P\xleftrightarrow{SK}Q:\) [PERSON] and [PERSON] share SK as a secret. * \(<X>_{Y}:\) In conjunction with the formula Y, the formula X is utilized. * \((X)\): X is a hashed value in the formula. * \((X,Y)\): After that, the X and Y formulae are concatenated and hashed. * \((X,Y)_{k}\): Using the key k to hash the formulae X and Y. In the light of forgoing explanation of specific notations, we present the following rules for formalizing the logical postulates of BAN logic:  
**Message meaning rule:** For shared secret keys (Rule 1):  
\[\frac{P|\equiv Q\xleftrightarrow{k}P,P\triangleleft X_{k}}{P|\equiv Q|\sim X}\]  
[PERSON] trusts [PERSON] if it believes k is shared with [PERSON] and sees X is encrypted under k.  
**Nonce verification rule** (Rule 2):  
\[\frac{P|\equiv\#(X),P|\equiv Q|\sim X}{P|\equiv Q|\equiv X}\]  
If [PERSON] believes X was recently expressed (freshness) and [PERSON] once said X, [PERSON] believes that [PERSON] believes X. **Jurisdiction rule** (Rule 3):  
\[\frac{P|\equiv Q)|\equiv X,P|\equiv Q|\Rightarrow X}{P|\equiv X}\]  
If [PERSON] believes that [PERSON] has jurisdiction over X and [PERSON] believes that a file contains X, [PERSON] believes X as well. **Freshness rule** (Rule 4):  
\[\frac{P|\equiv\#(X)}{P|\equiv\#(X,Y)}\]  
If one of the components in the formula is known to be fresh, the complete formula must be fresh. **Belief rule** (Rule 5):  
\[\frac{P|\equiv Q|\equiv(X,Y)}{P|\equiv Q|\equiv(X)}\]  
If [PERSON] believes that [PERSON] believes in the message set (X, Y), then [PERSON] also believes that [PERSON] believes in message X. Session key rule: For shared secret keys (Rule 6):  
\[\frac{P|\equiv\#(X),P|\equiv Q|\equiv X}{P|\equiv P|\xleftrightarrow{k}Q}\]  
If [PERSON] believes the shared session key is fresh, [PERSON] and [PERSON] are said to believe X. The session key k with Q is then believed by [PERSON] Hence, the proposed scheme should meet the following goals, according to the BAN logic's analytic procedures:  
**Goal 1. **\(HGWN|\equiv(U_{i}\xleftrightarrow{SK}HGWN)\);  
**Goal 2. **\(HGWN|\equiv U_{i}|\equiv(U_{i}\xleftrightarrow{SK}HGWN)\);  
**Goal 3. **\(SN_{j}|\equiv(HGWN\xleftrightarrow{SK}SN_{j})\);  
**Goal 4. **\(SN_{j}|\equiv HGWN|\equiv(HGWN\xleftrightarrow{SK}SN_{j})\). **Goal 5. **\(HGWN|\equiv(SN_{j}\xleftrightarrow{SK}HGWN)\);  
**Goal 6. **\(HGWN|\equiv SN_{j}|\equiv(SN_{j}\xleftrightarrow{SK}HGWN)\). **Goal 7. **\(U_{i}|\equiv(HGWN\xleftrightarrow{SK}U_{i})\);  
**Goal 8. **\(U_{i}|\equiv HGWN|\equiv(HGWN\xleftrightarrow{SK}U_{i})\);  
**Goal 9.**\(FGWN|\equiv(HGWN\xleftrightarrow{SK}FGWN)\). **Goal 10. **\(FGWN|\equiv HGWN|\equiv(HGWN\xleftrightarrow{SK}FGWN)\). **Goal 11.**\(HGWN|\equiv(FGWN\xleftrightarrow{SK}HGWN)\). **Goal 12. **\(HGWN|\equiv FGWN|\equiv(FGWN\xleftrightarrow{SK}HGWN)\).