# Mdpj _sciences_
## Appendix A Verification Result of ProVerif  
_Appendix A.1. Verification Algorithm of ProVerif_  
```
(* Channel specification *)  free ch: channel. free sch: channel [private]. (* Key Encapsulation Mechanism *)  fun Encaps(pubKey, bitstring): bitstring. fun KEMkey(bitstring): bitstring. fun KEMCipher(bitstring): bitstring. fun DecapsKey(secKey, bitstring): bitstring. ```
(* Secrecy verification *) Q0: query attacker (SUPI). Q1: query attacker (kseafUE). Q2: query attacker (kseafSN). Q3: query attacker (kseafHN). (* Security requirements verification *) Q4: query mac: bitstring; Inj-event(HNRecReqSN(mac)) ==> (inj-event(SNSendReqHN(mac)) ==> inj-event(UESendReqSN(mac))). Q5: query mac: bitstring; Inj-event(UERCesSN(mac)) ==> (inj-event(SNRecResHN(mac)) ==> inj-event(HNSendResSN(mac))). Q6: query rstar: bitstring; Inj-event(HNRecConSN(rstar)) ==> (inj-event(SNRecConUE(rstar)) ==> inj-event(UESendConSN(rstar))). Q7: query rstar: bitstring, key: bitstring; inj-event(SNKeyObtn(key)) ==> (inj-event(HNRecConSN(rstar)) ==> inj-event(UESendConSN(rstar))). ```
**Algorithm A1**_Cont_. ``` Played by: UE Input: SUPI, \(id_{H}N\), \(pk_{HN}\), \(k\), SNname
[Step 1.1] new r1 LE; let Ks1 = KEMkey(Encaps(\(pk_{HN}\), rUE)) in let c1 = KEMCipher(Encaps(\(pk_{HN}\), rUE)) in new s1 LE; let p1 LE = p1(\(sk_{LIE}\)) in let USUCI = senc((SUPI, \(pk_{ULE}\), SNname), \(Ks1\))in let MAC1 = f1((USUCI, \(Ks1\))) in event UESendReqSN(MAC1); out(usch,c1, USUCI, MAC1, idHN));
[Step 2.3] in(usch, (c4, CONC, MAC2)); let Ks2 = DecapsKey(\(sk_{LIE}\), c4) in let rSN = xor(CONC, f5((\((k,ks2)\))) in if MAC2 <> f1((\(k,ks2\), rSN)) true then exit; event UERCesSN(MAC2); let RES = f2((\(k,ks2\))) in let CK = f3((\(k,ks2\))) in let IK = f4((\(k,ks2\))) in let RESetar = keyseed((CK, IK, \(ks2\), RES, SNname)) in let XRES = SHA((RESetar, rSN)) in let \(k_{AUSF}\) = keyseed((CK, IK, \(ks2\), CONC, SNname)) in let \(k_{SEAF}\) = keyseed((\(k_{AUSF}\), SNname)) in event UESendConSN(RESetar); out(usch, RESstar); out(usch, senc(kseafUE, \(k_{SEAF}\)));```
Played by: SN Input: SNname [Step 1.2] in(usch,(\(c1\), USUCI, MAC1, idHN)); new rSN; new ssID; event SNsendReqHN(MAC1); out(sch,(ssID, c1, USUCI, MAC1, SNname, tSN));
[Step 2.2] in(sch,(=ssID, c4, HXRES, M, CONC, MAC2)); event SNRecResHN(MAC2); out(usch,(c4, CONC, MAC2));
[Step 2.4] in(usch, RESstar); if sHXRES <> SHA((RESstar, rSN)) true then exit; event SNRecConUE(RESstar); let AK = xor(CONC, rSN) in let \(K3\) = xor(RESstar, sAK) in let (\(k_{SEAF}\), SUPI) = sdec(M, \(K3\)) in event SNKeyObtn((tkSEAF, SUPI)); out(sch,(sID, RESstar)); out(usch, senc(kseafN, \(k_{SEAF}\)));
```

**Algorithm A3** proc_SN

```
Played by: HN Input:\(k\), \(k_{HN}\), idHN
[Step 1.3] in(sch,(sID, c1, USUCI, MAC1, SNname, rSN)); let \(ks1\) = DecapsKey(\(sk_{HN}\), c1) in let (hSUPI, \(hpk_{UE}\), hSNname) = sdec(USUCI, \(ks1\)) in if hSNname <> hSNname' true then exit; if MAC1 <> f1((USUCI, \(ks1\))) true then exit; event HNRecRegSN(MAC1);
[Step 2.1] new rHN; let \(ks2\) = KEMkey(Encaps(\(hpk_{UE}\), rHN)) in let \(c4\) = KEMCipher(Encaps(\(hpk_{UE}\), rHN)) in let MAC2 = f1((\(k\), \(ks2\), rSN)) in let XRES = f2((\(k\), \(ks2\))) in let CONC = xor(rSN, f5((\(k\), \(ks2\)))) in let CK = f3((\(k\), \(ks2\))) in let IK = f4((\(k\), \(ks2\))) in let XRESstar = keyseed((CK, IK, \(ks2\), XRES, SNname)) in let HXRES = SHA((XRESstar, rSN)) in let \(k_{AUSF}\) = keyseed((CK, IK, \(ks2\), CONC, SNname)) in let \(k_{SEAF}\) = keyseed((\(k_{AUSF}\), SNname)) in let \(K3\) = xor(XRESstar, f5((k, \(ks2\))) in let M = senc((\(k_{SEAF}\), hSUPI), \(K3\)) in event HNSendResSN(MAC2); out(sch,(sID, c4, HXRES, M, CONC, MAC2));
```
1[Step 2.5] in(sch, (=sID, RESstar)); if XRESstar <> RESstar true then exit; eventHNRecConSN(RESstar); out(usch, senc(kseafHN, \(k_{SEAF}\)));
```
**Algorithm A5** Main Process without FS--(S1)
```
process new idHN; let \(pk_{HN}=pk(sk_{HN})\) in (!UE(SUPI, idHN, \(pk_{HN}\), \(k\), SNname) \(|\)!SN(SNname) \(|\)!HN(\(k\), \(sk_{HN}\), idHN)!