## 2 Materials and Methods
### Formal Security Verification Using AVISPA Tool
State = 1 / Rcv(IDOHN.HOONH([HDi.B.HXGMMh)).H(H((IDi.R).HXGMMh).H(H((IDi.R).H(PWI.R).TIDi')).IDONNf.xor(H(IDOHNf.H(DIi.R).MKGMMh),H((H(IDi.R).H(PWI.R).TIDi')).TIDi',Gen.Rep.H.T_Skuisa) =|> State' := 2 / secret(IDOHN.H), sp2, {Ui,SA,HOHN}) / secret(([HXGMMh), sp3, {SA,HOHN}] / secret((IDGMMh), sp4,{Ui,SA,FGWN}) / secret(([HXGMMh], sp5, {SA,FGWN}] / login phase % Send message M = CIDNN), Ci> to HGWN via public channel / RNi':= new() / TSI':= new() / Ki':= H(IDiOMN.H(IDi.R).MKGMMh) / Bi':=H(H(IDi.R).TIDi.RNi') / Ci':= {L(IDOHN.H).Bi':RNI':TSI' }_Ki' / Smd(IDNIDN).TIDi':Ci': % Ui has freshly generated the value TSI for HGWN / witness(ui, HGWN, u_hgun_ru, TSI') % Ui has freshly generated the value RNi for HGWN / witness(Ui, HGONN, u_hgun_tsu, RNi') 3. State = 2 / Rcv(IDSHi).xor(H((H(IDi.R).MKI').RNI').TSI') / RNi':= H(IDGMMh.T(ONH(IDi.R).MKI').RNI').TSI') =|> State' := 3 / request(SNj), Ui, sn_ui_rk, TS3') / request(SNj), Ui, sn_ui_tsk,Rmi') end role  
Similarly, Figure 12 shows the role of the home gateway role in HLPSL. The role starts by receiving the message (IDSNj.TIDi'.IDGWNh.IDSNj.H(H(IDi.R).TIDi'.RNI'). RNi'.TS1' _H(IDGWNh.H(IDi.R).MKGWNh)) from the user Ui using the operation Rcv 0. The declaration secret (IDi, PWi, R, sp1, Ui ) indicates that the values IDi, PWi, R sent secularly to the user Ui using the protocol sp1. While the statement secret (IDGWNh, sp2, Ui, SA, HGWN) specifies the identity of the home gateway among the Ui and SA by the HGWN using protocol ID sp2. Furthermore, the indication secret (MKGWNh, sp3, SA, HGWN) shows that the master key is shared between the SA and the HGWN. While the identity of the foreign gateway is shared securely using the declaration secret (IDGWNf, sp4, Ui, SA, FGWN) amongst the Ui, and SA using the protocol ID sp4. The foreign gateway shares its master key with SA using the declaration secret (MKGWNf, sp5, SA, FGWN). Later, the home gateway sends the message (IDSNj.Fi') to the sensor using Snd(). The declaration witness (HGWN, SNj, hgwn_sn_rf, TS2') indicates that the HGWN freshly generates TS2' for the SNj. Furthermore, the HGWN is freshly generating random once RNi' for the sensor using the declaration witness (HGWN, SNj, hgwn_sn_tsf, RNk'). The HGWN accepts the legitimacy of the Ui by checking the freshness of the TSI using the declaration request (Ui, HGWN, u_hgwn_ru, TSI'), and also accepts the legitimacy of the user by checking RNi' through the indication request (Ui, HGWN, u_hgwn_tsu, RNi'). Figure 11: role in HLPSL. role homegateway (Ui, SA, HGWN, SWj : agent, H: hash_func,  Snd, Kvv: channel(dy))  played by HGWN  def=  Local State: nat,  FWM : agent,  PWI, BIO1, S, U1, ID1,TID1, IDGMNh, IDGWNf, TS1, TS2, TS3: text,  F: hashfunc,  R: text,  MKGWNh, MGWNf, IDSNj, MKSNj, Ki, kj, Bi, Ci, Fi, Gi, RNi, RNk, RNj, Gj: text  const spl, sp2, sp3, sp4, sp5, vi_hown_ru, ui_hown_tsu,  hgwn sn rf, hgwn_sn_tsf: protocol_id  init State := 0  transition  % Login and authentication phases  % Reclive message Mgsl from Ui via public channel  1. State = 0 / Rcv(IDSNj).TID1'.(IDGWNh.IDSNj).H(H(IDi.R).TIDi'.RNi'). RNi'.TS1' _H(IDGWNh.H(IDi.R).MGWNh)) =]>  State' := 3 / secret((IDGWNh), sp2, (Ui, SA, HGWNh))  / secret((HGWMh), sp3, (SA, HGWNh))  / secret((IDGMNf), sp4, (Ui,SA, FGWNh))  / secret(MGWNf), sp5, (SA, FGWNh)  % Authentication and key agreement phase % Send message M2 =c10 SMj, Fi>  to sensor SMj via public channel  / TS2' := new()  / Rkk := new()  / k' := H(IDSNj).MKSNj)  / D1' := H((Wxor(H(ID1.R),RNi')).RNi' : RANK'.TS2')  / k' := {DGWNh.IDSNj.H(xor(H(ID1.R),RNi')).RNi'.RNk'.D1'.TS2'}_Kj'  % Send message Mgsl to SMj via public channel  / 5 nd(IDSNj).F1'  % hgwn has freshly generated the values rf and TSf for SMj  / witness(HWMh, Wj, hgwn_sn_tf, TS2')  / witness(HWMh, SNj, hgwn_tsf, RNk')  % hgwn' acceptance of the values ru and Tsu generated for hgwn by Ui  / request(Ui, HGWN, ui hgwn_tsu, RNi') end role  InFigure 12, The home gateway role in HLPSL. In Figure 13, the role of the sensor node in HLPSL is illustrated.