## 2 Materials and Methods
### Formal Security Verification Using AVISPA Tool  
This section demonstrates the proposed scheme's security validation using the AVISPA tool, a widely used and well-known security validation tool [52]. The security verification code was written using the AVISPA tool based on High-Level Protocol Specification Language (HLPSL). It is a role-oriented language composed of primary roles that define each participant system and composition roles representing scenarios connected to fundamental roles [53]. The intruder, who is always represented by \"I\" and explained using the Dolev-Yao model, also plays a special role. The intruder plays a critical part in implementing the protocol and interacts with several other functions in the system. Using the HLPSL2 IF translator, the HLPSL protocol specification is transformed into an intermediate format (IF). After that, the intermediate format is examined using one of four different backends: CL-AtSe, OFMC, SATMC, or TA4 SP. Each backend uses a variety of automated analytical tools to detect potential attacks against known models. Specifying Scheme Roles  
This section shows our scheme employing HLPSL in two scenarios. The first scenario, as shown in Figures 11-14, carries out the basic functions of UI's, SA's, HWGN, and SNj sensor nodes during the user registration, log-in and authentication, and key agreement phases (Case 1). In the second scenario, we integrated user roles Ui, SA, HWGN, and sensor node SNj throughout the user registration, log-in and authentication phase, and key agreement phase (Case 2). The details of the role of the initiator, the user Ui, are shown in Figure 11 for Case 1. The start signal is first received by Ui, which changes its state from 0 to 1. The variable status is used to keep track of the current state. Using the SND0 function, Ui securely provides PIDi, PWRi to the SA during the registration phase of the user. The SCi smart card is received in Ui from the SA containing information (IDGWNNh, Aih), (IDGWNf, Aif), TIDi, Gen (. ), Rep(. ), h (.) and t, changing the status from 1 to 2. Ui delivers the log-in request message M1 = IDSNj, TIDi, Ci to the HGWN across an open channel during the log-in phase. The secret declaration (X, id, A) states that the protocol identification of agent A is id. The information X is kept secret from agent A. For example, secret (IDi, PWRi, BIOi, sp1, Ui) implies that IDi, PWi, and secret number R are kept secret from Ui only, as determined by the protocol identifier sp1. Declaration witness (Ui, HGWN, ui hgwn ru, TS1') implies that Ui recently generated the HGWN timestamp TS1. During the authentication and key agreement phases, Ui gets the acknowledgment message M3 = hIDSNj, Gi, Hi, TS3i through a public channel from the sensor node SNj and updates its state from 2 to 3. Finally, Ui checks SNj's authenticity by comparing SNj's timestamp TS3 to the randomly generated nonce RNj generated by the declaration request (SNj, Ui, sn ui rk, RNj'). Notably, the type declaration channel (dy) reflects the communication channel using the Dolev-Yao threat model, implying that an intruder can view, intercept, or change messages sent via an insecure public channel. Sentence A denotes that the function is carried out by the agent identified by variable A.  
role user (Ui, SA, HGWN, SN) : agent, H: hash_func, SKuisa : symmetric_key, Snd, Rcv: chname((dy)) played by Ui def= local State: mat, FGWN : agent, PID1, PWRi, Di, IDi, RTDi, PWi, BIOi, R: text, Aih, AiI, f, RTSi, TIDj,TIDi, IDOMWh, IDONNf, TSL, TS2, TS3: text, Gen, Rep: hash func, RGWNH,HGWNnf,IDSNj, MKSNj,Kl, Kj, Bi, Ci, RNi, RNk, RNj: text, F: hash_func const SP1, sp2, sp3, sp4, sp5, ui_hgun_ru, ui_hgun_tsu, su_ui_rk, su_ui_tsk : protocol_id init State := 0 transition 1. State = 0 / Rcv(start) =|> State' := 1 / PID1':= H(IDi:R) / PWHi':= H(HUI:R) / Smd((PD1 POi:PWRi)_Skuisa) / secret(([ID1,PWRi,BIOi], sp1, {Ui}]) % Receive registration reply from the SA Securely 2.