## 2 Materials and Methods
### Formal Security Verification Using AVISPA Tool
The role starts by receiving the message (IDSNj,IDGWNh,IDSNj,H(xor(H(IDi.K), RNi')). RNi'.RNk'.H(H(xor (H(IDi.K), RNi')). RNi'.RNk'.TS2').TS2'_H(IDSNj).MKSNj)) from the HGWN using the operation Rcv (). However, the role indicates the values IDi, PWi, R are shared securely to the user using the declarations secret (IDi, PWi, R, sp1, Ui). The declarations secret (IDGWNh, sp2, Ui, SA, HGWNh), and secret (IDGWNf, sp4, Ui, SA, FGWN) specify that the identity of the home and foreign gateway is shared secretly among the Ui, and the SA. While the expressions secret (MKGWNh, sp3, SA, HGWN, and secret(MKGWNf, sp5, SA, FGWN) show that the master key of the home and foreign gateways is shared securely to the user Ui. Likewise, the user believes that the sensor freshly generates TS3', and RNj' for user. The user also acknowledges the HGWN's legality by confirming the TS2' timestamp using the declaration request (HGWN, SNj, hgwn sn rf, TS2'), and by validating the RNk's random nonce with the declaration request (HGWN, SNj, hgwn sn tsf, RNk'). The role of system administrator in HLPSL is shown in Figure 14. After the message (H(IDi.K).H(PWi.K)_SKuisa) is received from the user, it shares the values IDi, PWi, K securely using the protocol ID sp1. Later, it sends (IDGWNh.Aih'.IDGWNf.Aif'.TIDi'.Gen.Rep.H.T_SKuisa) and encrypts the message using the SKuisa secret key. Furthermore, it indicates that the identities by the declarations secret (IDGWNh, sp2, Ui, SA, HGWN), and secret (IDGWNf, sp4, Ui, SA, FGWN) are shared among Ui, SA, HGWN, and FGWN. The master keys MKGWNh, and MKGWNf are share secretly by the declarations secret (MKGWNh, sp3, SA, HGWNh), and secret (MKGWNf, sp5, SA, FGWN) to the SA. Figure 12: The home gateway role in HLPSL. role sensornode (Ui, SA, HGMN, SWj: agent, H: hash_func, Snd, Rev: channel(dy))  
Pslowed by SNj  
def=  
Local State: nat, FOMN: agent, ID1, PWN1, K, DID1, PWN1, Aih, Aif, T: text, F: hash_func, TD1, DOMMN, ID0 MMN1, T51, T52, T53, SUiNjn: text, Gen, Rep: hash func, MKGMMN, MKGMMNf, ID5 Hj, MKGNhj, Pj, Ki, Kj, Bi, Ci, Di, Fi, Gi, Hi, RNi, RNk, RNj, BIOi: text const s  
ronment). In addition, the proposed scheme has implemented five secrecy goals and three authentication goals:  
**Secrecy_Goals:**  
secrecy_of sp1: Indicates that the IDi, PWRi, and BIOi are kept secret to the Ui. secrecy_of sp2: States that the IDGWNh is shared securely to the Ui, SA, and HGWN. secrecy_of sp3: This shows that the MKGWNh is kept secret to the SA and HGWN. secrecy_of sp4: Indicates that the IDGWNf is shared among Ui, SA, and FGWN. secrecy_of sp5: Indicates that the MKGWNf is kept secret to the SA and FGWN. **Authentication Goals:**  
authentication_on ui_hgwn_ru, ui_hgwn_tsu: It indicates that the user Ui generates TS1' and RNi; which are freshly generated and perform a strong authentication with HGWN-based validity of these values. authentication_on hgwn_sn_rf, hgwn_sn_tsf: It indicates that HGWN generates TS2' and RNK' freshly for the sensor and performs a strong authentication of the parameter's freshness. authentication_on sn_ui_rk, sn_ui_tsk: It shows that the sensor generates a fresh TS3' and RNj' for the user and performs a strong authentication based on the validity of the values.