## 2 Materials and Methods
### Proof of Authentication Using BAN Logic
**Goal 13. **\(FGWN|\equiv(U_{i}\xleftrightarrow{SK}FGWN)\);  
**Goal 14. **\(FGWN|\equiv U_{i}|\equiv(U_{i}\xleftrightarrow{SK}FGWN)\). **Goal 15. **\(SN_{j}|\equiv(FGWN\xleftrightarrow{SK}SN_{j})\);  
**Goal 16. **\(SN_{j}|\equiv FGWN|\equiv(FGWN\xleftrightarrow{SK}SN_{j})\);  
**Goal 17. **\(FGWN|\equiv(SN_{j}\xleftrightarrow{SK}FGWN)\);  
**Goal 18. **\(FGWN|\equiv SN_{j}|\equiv(SN_{j}\xleftrightarrow{SK}FGWN)\). **Goal 19. **\(U_{i}|\equiv(FGWN\xleftrightarrow{SK}U_{i})\);  
**Goal 20. **\(U_{i}|\equiv FGWN|\equiv(FGWN\xleftrightarrow{SK}U_{i})\). To simplify the analysis between \(U_{i}\) and \(SN_{j}\), we first idealize the transmitted messages of our proposed scheme, which are as follows:  
**Message 1:**\(U_{i}\to HGWN\): \(HGW_{ID},SN_{ID},W_{i},N_{i},TS_{1}\). **Message 2:**\(HGWN\to SN_{j}\): \(HGW_{ID},SN_{ID},PID_{i},N_{i}^{*},N_{j},P_{i},TS_{2}\). **Message 3:**\(SN_{j}\to HGWN\): \(SN_{ID},B_{i},Z_{i},TS_{3}\). **Message 4:**\(HGWN\to Uli\): \(HGW_{ID},SN_{ID},PID_{i}^{*},N_{j},N_{j}^{*}\). **Message 5:**\(HGWN\to FGWN\): \(SN_{ID},PID_{i},HGW_{ID},A_{fit}\). **Message 6:**\(FGWN\to HGWN\): \(A_{ht},HGW_{ID}:\)\(\in PID_{i},FGW_{ID}>A_{tf},PID_{i}\). **Message 7:**\(HGWN\to U_{i}\): \(A_{ht}:\)\(<\)\(HGW_{ID},SN_{ID},PID_{i}^{*},N_{j},N_{j}^{*}>A_{tf},FGW_{ID}\). **Message 8:**\(U_{i}\to FGWN\): \(FGW_{ID},SN_{ID},PID_{i},N_{i}^{*},N_{j},P_{i},TS_{2}\). **Message 9:**\(FGWN\to SN_{j}\): \(FGW_{ID},SN_{ID},PID_{i},N_{j}^{*},NC_{j}^{*},TS_{6}\). **Message 10:**\(SN_{j}\to FGWN\): \(SN_{ID},F_{i},Q_{i},TS_{5}\). **Message 11:**\(FGWN\to U_{i}\): \(FGW_{ID},SN_{ID},PID_{i},N_{f},Nc_{f}^{*},TS_{6}\). Based on our proposed scheme, we made the following initial state assumptions:  
**A1:**\(U_{i}|\equiv\#(N_{i}^{*},N_{j},N_{f},Nc_{f}^{*})\);  
**A2:**\(HGWN|\equiv\#(N_{i}^{*},N_{j},N_{f})\);  
**A3:**\(SN_{j}|\equiv\#(N_{i}^{*},N_{j},N_{f},Nc_{f}^{*})\);  
**A4:**\(FGWN|\equiv\#(N_{i}^{*},N_{j},N_{f})\);  
**C1:**\(U_{i}|\equiv(U_{i}\xleftrightarrow{SK}HGWN)\);  
**C2:**\(HGWN|\equiv(HGWN\xleftrightarrow{P_{i}}SN_{j})\);  
**C3:**\(SN_{j}|\equiv(SN_{j}\xleftrightarrow{P_{j}}HGWN)\);  
**C4:**\(HGWN|\equiv(HGWN\xleftrightarrow{PID_{i}}U_{i})\);  
**C5:**\(U_{i}|\equiv(U_{i}\xleftrightarrow{SK_{i}\xleftrightarrow{P_{i}}}FGWN)\);  
**C6:**\(FGWN|\equiv(FGWN\xleftrightarrow{SK_{i}\xleftrightarrow{P_{i}}}SA_{j})\);  
**C7:**\(SN_{j}|\equiv(SN_{j}\xleftrightarrow{SK}SN_{j})\);  
**C8:**\(FGWN|\equiv(FGWN\xleftrightarrow{P_{i}}UI)\);  
**C9:**\(HGWN|\equiv(HGWN\xleftrightarrow{Nc_{i}^{*}}FGWN)\)_;_  
**C10:**\(FGWN|\equiv(FGWN\xleftrightarrow{SK_{i}}HGWN)\)_;_  
**B1:**\(HGWN|\equiv(U_{i}\to N_{i}^{*})\)_;_  
**B2:**\(SN_{j}|\equiv(HGWN\to N_{j})\)_;_  
**B3:**\(HGWN|\equiv(SN_{j}\to N_{i}^{*})\)_;_  
**B4:**\(U_{i}|\equiv(HGWN\to N_{j}^{*})\)_;_  
**B5:**\(FGWN|\equiv(U_{i}\to N_{f})\)_;_  
**B6:**\(SN_{j}|\equiv(FGWN\to N_{f})\)_;_  
**B7:**\(FGWN|\equiv(SN_{j}\to Nc_{i}^{*})\)_;_  
**B8:**\(U_{i}|\equiv(FGWN\to N_{f})\)_;_  
**B9:**\(HGWN|\equiv(FGWN\to N_{i}^{*})\)_;_  
**B10:**\(FGWN|\equiv(HGWN\to N_{f})\)_;_  
Additionally, we demonstrate the robustness of the present scheme based on BAN logic rules by showing that Ui and SNj have the same shared SK session key to communicate securely while still accomplishing the required goals under initial assumptions.