## 2 Materials and Methods
### Proof of Authentication Using BAN Logic
The following are the descriptions of the inside information:  
We might get the following based on message 1:  
\[S1:HGWN\xleftrightarrow{}HGW_{I}D,SN_{ID},W_{i},N_{i},TS_{1}.\]  
We apply the message meaning rule to S1 and Assumption C1 to get:  
\[S2:HGWN|\equiv U_{i}|\sim N_{i}.\]  
Then, we use the freshness conjunctenation rule and the nonce verification rule to get the final observations based on assumptions A2 and Step 2:  
Figure 9:0  
When B1, S3, and the jurisdiction rule are applied, we get:  
Figure 9:1  
We apply the session key rule to the assumptions A2 and S3 to get:  
Figure 9:2  
The nonce verification rule and jurisdiction rule are applied to S5 and assumption A2 to obtain:  
Figure 9:3  
We could obtain the following from message 2:  
Figure 9:4  
If we apply the message meaning rule to C2, S7, we get:  
Figure 9:5  
The freshness conjunctenation rule and nonce verification rule are applied to assumptions A3 and S8 to obtain:  
Figure 9:6We use the jurisdiction rule to get the following results from Step 9 and B2:  
Figure 9:7  
S9 and A3 are combined with the session key rule to produce:  
Figure 9:8  
S11 and assumption A3 are applied to the nonce verification rule to achieve:  
Figure 9:9  
We may get the following from message 3:  
\[\frac{P|\equiv Q\xleftrightarrow{k}P,P\triangleleft X_{k}}{P|\equiv Q|\sim X}\]0  
We apply the message meaning rule to S13 and assumption C3 to get:  
\[\frac{P|\equiv Q\xleftrightarrow{k}P,P\triangleleft X_{k}}{P|\equiv Q|\sim X}\]1  
The freshness conjunctenation rule and nonce verification rule are applied to assumptions A2 and S14 to obtain:  
\[\frac{P|\equiv Q\xleftrightarrow{k}P,P\triangleleft X_{k}}{P|\equiv Q|\sim X}\]2  
We apply the jurisdiction rule in S15 and B3 to obtain:  
\[\frac{P|\equiv Q\xleftrightarrow{k}P,P\triangleleft X_{k}}{P|\equiv Q|\sim X}\]3  
We apply the session key rule to the assumptions A2 and S15 to obtain:  
\[\frac{P|\equiv Q\xleftrightarrow{k}P,P\triangleleft X_{k}}{P|\equiv Q|\sim X}\]4  
We use the nonce verification rule to derive the following result from S17 and assumption A2:  
\[\frac{P|\equiv Q\xleftrightarrow{k}P,P\triangleleft X_{k}}{P|\equiv Q|\sim X}\]5  
We might get the following based on message 4:  
\[\frac{P|\equiv Q\xleftrightarrow{k}P,P\triangleleft X_{k}}{P|\equiv Q|\sim X}\]6  
We apply the message meaning rule to S19 and assumption C4 to obtain:  
\[\frac{P|\equiv Q\xleftrightarrow{k}P,P\triangleleft X_{k}}{P|\equiv Q|\sim X}\]7  
Applying the freshness concatenation and nonce verification rules to assumptions A1 and S20, we obtain:  
\[\frac{P|\equiv Q\xleftrightarrow{k}P,P\triangleleft X_{k}}{P|\equiv Q|\sim X}\]8  
We obtain jurisdiction by using the jurisdiction rule in line with B4 and S21:  
\[\frac{P|\equiv Q\xleftrightarrow{k}P,P\triangleleft X_{k}}{P|\equiv Q|\sim X}\]9  
We use the session key rule-following A1 and S21 to achieve:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\sim X}{P|\equiv Q|\equiv X}\]0We use the nonce verification rule to derive the following result from S23 and assumption A1:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\sim X}{P|\equiv Q|\equiv X}\]1  
According to message 5, we might be able to obtain:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\sim X}{P|\equiv Q|\equiv X}\]2  
S25 and assumption C9 are subjected to the message meaning rule to obtain:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\sim X}{P|\equiv Q|\equiv X}\]3  
From S26, we apply the nonce verification rule to get:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\sim X}{P|\equiv Q|\equiv X}\]4  
We use the jurisdiction rule to get the following from S27 and B8:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\sim X}{P|\equiv Q|\equiv X}\]5  
According to S27 and S28, the session key rule is applied, and we get:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\sim X}{P|\equiv Q|\equiv X}\]6  
According to S29, we apply the nonce verification rule to get:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\sim X}{P|\equiv Q|\equiv X}\]7  
We might be able to access this based on message 6:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\sim X}{P|\equiv Q|\equiv X}\]8  
Using the message meaning rule with S31 and Assumption C10, and we get at:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\sim X}{P|\equiv Q|\equiv X}\]9  
We use the nonce verification rule to get the following observations from S32:  
\[\frac{P|\equiv Q)|\equiv X,P|\equiv Q|\Rightarrow X}{P|\equiv X}\]0  
We apply the jurisdiction rule to S33 and B9 to obtain:  
\[\frac{P|\equiv Q)|\equiv X,P|\equiv Q|\Rightarrow X}{P|\equiv X}\]1  
According to S33 and S34, the session key rule is applied, we get:  
\[\frac{P|\equiv Q)|\equiv X,P|\equiv Q|\Rightarrow X}{P|\equiv X}\]2  
We apply the nonce verification procedure following S35 to obtain:  
\[\frac{P|\equiv Q)|\equiv X,P|\equiv Q|\Rightarrow X}{P|\equiv X}\]3  
We might be able to obtain this based on message 7:  
\[\frac{P|\equiv Q)|\equiv X,P|\equiv Q|\Rightarrow X}{P|\equiv X}\]4We apply the message meaning rule to S37 and assumption C5 to obtain:  
\[\frac{P|\equiv Q)|\equiv X,P|\equiv Q|\Rightarrow X}{P|\equiv X}\]5  
Applying the freshness conjuncatenation and nonce verification rules to assumptions A4 and S38, we obtain:  
\[\frac{P|\equiv Q)|\equiv X,P|\equiv Q|\Rightarrow X}{P|\equiv X}\]6  
We apply the jurisdiction rule by B9 and S39 to get:  
\[\frac{P|\equiv Q)|\equiv X,P|\equiv Q|\Rightarrow X}{P|\equiv X}\]7  
We apply the session key rule-following A1, A4, and Step 40 to obtain:  
\[\frac{P|\equiv Q)|\equiv X,P|\equiv Q|\Rightarrow X}{P|\equiv X}\]8  
We apply the nonce verification rule to Step 41 and assumption A1 to get:  
\[\frac{P|\equiv Q)|\equiv X,P|\equiv Q|\Rightarrow X}{P|\equiv X}\]9  
We may obtain according to message 8:  
\[\frac{P|\equiv\#(X)}{P|\equiv\#(X,Y)}\]0  
We use the message meaning rule from S43 and assumption C10:  
\[\frac{P|\equiv\#(X)}{P|\equiv\#(X,Y)}\]1  
We apply the freshness conjuncatenation rule and the nonce verification rule from assumptions A4 and S44 to:  
\[\frac{P|\equiv\#(X)}{P|\equiv\#(X,Y)}\]2  
From S45 and B5, we apply the rule of competence to obtain:  
\[\frac{P|\equiv\#(X)}{P|\equiv\#(X,Y)}\]3  
The session key rule is applied according to A4 and S45 and 46; thus, we obtain:  
\[\frac{P|\equiv\#(X)}{P|\equiv\#(X,Y)}\]4  
Under A4 and S47, the nonce verification rule is to be established:  
\[\frac{P|\equiv\#(X)}{P|\equiv\#(X,Y)}\]5  
We may obtain according to message 9:  
\[\frac{P|\equiv\#(X)}{P|\equiv\#(X,Y)}\]6  
We apply the message meaning rule according to C2, B5, and S49:  
\[\frac{P|\equiv\#(X)}{P|\equiv\#(X,Y)}\]7  
We apply the freshness conjuncatenation rules and the nonce verification rule for assumptions A3 and S50:  
\[\frac{P|\equiv\#(X)}{P|\equiv\#(X,Y)}\]8  
We use the rule of jurisdiction to obtain the following S51 and B6 results:  
\[\frac{P|\equiv\#(X)}{P|\equiv\#(X,Y)}\]9From S52 and A3 and to obtain the key session rule:  
\[\frac{P|\equiv Q|\equiv(X,Y)}{P|\equiv Q|\equiv(X)}\]0  
From S52 and A3 and to obtain the key session rule:  
\[\frac{P|\equiv Q|\equiv(X,Y)}{P|\equiv Q|\equiv(X)}\]1  
According to message 10, we could get:  
\[\frac{P|\equiv Q|\equiv(X,Y)}{P|\equiv Q|\equiv(X)}\]2  
From S55 and assumption C7, we use the message meaning rule:  
\[\frac{P|\equiv Q|\equiv(X,Y)}{P|\equiv Q|\equiv(X)}\]3  
We obtain by applying the freshness conjuncatenation and nonce verification rules to assumptions A4 and S56:  
\[\frac{P|\equiv Q|\equiv(X,Y)}{P|\equiv Q|\equiv(X)}\]4  
We apply the jurisdiction rule-following S57 and B7 to obtain:  
\[\frac{P|\equiv Q|\equiv(X,Y)}{P|\equiv Q|\equiv(X)}\]5  
We apply the session key rule to the assumptions A4 and S58 to obtain:  
\[\frac{P|\equiv Q|\equiv(X,Y)}{P|\equiv Q|\equiv(X)}\]6  
We obtain by applying the nonce verification rule to S59 and assumption A4:  
\[\frac{P|\equiv Q|\equiv(X,Y)}{P|\equiv Q|\equiv(X)}\]7  
According to message 11, we might be able to obtain:  
\[\frac{P|\equiv Q|\equiv(X,Y)}{P|\equiv Q|\equiv(X)}\]8  
We apply the message meaning rule to Step 61 and assumption C8 to obtain:  
\[\frac{P|\equiv Q|\equiv(X,Y)}{P|\equiv Q|\equiv(X)}\]9  
We obtain by applying the freshness conjuncatenation and nonce verification rules to the assumptions A1 and S62:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\equiv X}{P|\equiv P|\xleftrightarrow{k}Q}\]0  
We apply the jurisdiction rule by A1 and S63 to get:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\equiv X}{P|\equiv P|\xleftrightarrow{k}Q}\]1  
We apply the session key rule by A1 and S63 and S64 to achieve:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\equiv X}{P|\equiv P|\xleftrightarrow{k}Q}\]2  
Applying the nonce verification rule to S65 and assumption A1, we obtain:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\equiv X}{P|\equiv P|\xleftrightarrow{k}Q}\]3  
From Steps 5-6, 11, 12, 17, 18, 23, 24, 29, 30, 35, 36, 41, 42, 48, 47, 53, 54, 59, 60, 65, and 66, it is obvious that our scheme accomplishes all of the goals (Goals 1-20).