ISM_KA.pv

(*** ISM Key Agreement Scheme ***)

(* Chael Definition *)
free net : chael.

(* Private Terms *)
free SK_esp_r : bitstring [private].
free SK_r_i : bitstring [private].
free IDw : bitstring [private].
free PWw : bitstring [private].
free IDr : bitstring [private].
free IDi : bitstring [private].
free s : bitstring [private].
free rr : bitstring [private].
free ri : bitstring [private].
free X2w : bitstring [private].
free X3w : bitstring [private].
free X4w : bitstring [private].
free X6w : bitstring [private].
free X7w : bitstring [private].
free ai : bitstring [private].
free ar : bitstring [private].
free aesp : bitstring [private].
const Yi : bitstring [private].
const seriali : bitstring [private].

(* Public Terms *)
free Qesp : bitstring.
free IDesp : bitstring.
free Eespi : bitstring.
free Hespi : bitstring.
const x : bitstring.
const p : bitstring.
const dt : bitstring.

(* Functions *)
fun XORFun(bitstring, bitstring) : bitstring.
fun HashFunOne(bitstring) : bitstring.
fun HashFunTwo(bitstring, bitstring) : bitstring.
fun HashFunThree(bitstring, bitstring, bitstring) : bitstring.
fun HashFunFour(bitstring, bitstring, bitstring, bitstring) : bitstring.
fun HashFunSix(bitstring, bitstring, bitstring, bitstring, bitstring, bitstring) : bitstring.
fun Cheb(bitstring, bitstring, bitstring) : bitstring.
fun MulFun(bitstring, bitstring) : bitstring.
fun DivideFun(bitstring, bitstring) : bitstring.
fun ConcatTwo(bitstring, bitstring) : bitstring.
fun ConcatFour(bitstring, bitstring, bitstring, bitstring) : bitstring.
fun Separate_First(bitstring): bitstring.
fun Separate_Second(bitstring): bitstring.
fun Separate_Third(bitstring): bitstring.
fun Separate_Fourth(bitstring): bitstring.
fun SEncrypt(bitstring, bitstring): bitstring.
fun SymEnc(bitstring, bitstring) : bitstring.
fun ElapsedTime(bitstring, bitstring) : bitstring.
fun Lessthan(bitstring, bitstring) : bool.

(* Destructors *)
reduc forall x1 : bitstring, x2 : bitstring; DXORFun(XORFun(x1, x2), x1) = x2.
reduc forall X : bitstring, y : bitstring; SDecrypt(SEncrypt(X,y), y) = X.
reduc forall m : bitstring, key : bitstring; SymDec(SymEnc(m, key), key) = m.

(* queries *)
query attacker (SK_esp_r).
query attacker (SK_r_i).
query attacker (aesp).
query attacker (ar).
query attacker (ai).
query attacker (s).
query attacker (rr).
query attacker (ri).
query attacker (IDw).
query attacker (IDr).
query attacker (IDi).
query inj-event ( endESP ) ==> inj-event (startESP).
query inj-event ( endRr ) ==> inj-event (startRr).
query inj-event ( endISMi ) ==> inj-event (startISMi).

(* Events *)
event startESP.
event endESP.
event startRr.
event endRr.
event startISMi.
event endISMi.

(* Rr *)
let pRr=
let rw = XORFun(XORFun(IDw, PWw), X7w) in
let RPWw = HashFunTwo(PWw, rw) in
let X1w = XORFun(X2w, RPWw) in
let respw = XORFun(HashFunTwo(RPWw, X1w), X4w) in
let xX3w = HashFunTwo(X1w, respw) in
if (X3w = xX3w) then
let Temp = XORFun(HashFunOne(XORFun(IDw, X1w)), X6w) in
let rrar = MulFun(rr, ar) in
let Ar = Cheb(rrar, x, p) in
new T : bitstring;
new Loc : bitstring;
let XIDrw = XORFun(ConcatFour(IDr, IDw, Loc, T), HashFunTwo(Ar, Temp)) in
let Y1w = XORFun(RPWw, HashFunTwo(IDw, X1w)) in
let Y2w = XORFun(XORFun(X4w, HashFunTwo(Ar, X1w)), Temp) in
let X5w = Cheb(respw, x, p) in
let Vresp = HashFunSix(IDr, IDw, Loc, T, RPWw, respw) in
event startESP;
out(net, (XIDrw, X5w, Y1w, Y2w, Ar, Vresp));
in (net, (xXIDespi : bitstring, xCespr : bitstring, xAesp : bitstring, xVesp : bitstring));
let Kespr_R = Cheb(rrar, xAesp, p) in
let SK_esp_r_R = HashFunFour(IDr, IDesp, T, Kespr_R) in
out(net, SEncrypt(SK_esp_r, SK_esp_r_R));
let Temp2 = XORFun(xXIDespi, HashFunOne(SK_esp_r_R)) in
let xIDi = Separate_First(Temp2) in
let xQi = Separate_Second(Temp2) in
let xxVesp = HashFunFour(xIDi, xQi, SK_esp_r_R, xCespr) in
if (xVesp = xxVesp) then
let Temp3 = Cheb(ar, xQi, p) in
let X1r = MulFun(ConcatTwo(T, IDr), Temp3) in
let Vri = HashFunFour(xIDi, xCespr, Ar, X1r) in
event startISMi;
out (net, (X1r, Ar, xCespr, Vri));
in (net, (xAi : bitstring, xVi : bitstring));
let Kri_R = Cheb(rrar, xAi, p) in
let SK_r_i_R = HashFunFour(xIDi, IDr, T, Kri_R) in
out(net, SEncrypt(SK_r_i, SK_r_i_R));
let xxVi = HashFunOne(SK_r_i_R) in
if (xVi = xxVi) then
event endRr.

(* ESP *)
let pESP=
in (net, (xXIDrw : bitstring, xX5w : bitstring, xY1w : bitstring, xY2w : bitstring, xAr : bitstring, xVresp : bitstring));
let Temp4 = XORFun(xXIDrw, HashFunTwo(xAr, HashFunThree(s, Qesp, xX5w))) in
let xIDr = Separate_First(Temp4) in
let xIDw = Separate_Second(Temp4) in
let xLoc = Separate_Third(Temp4) in
let xT = Separate_Fourth(Temp4) in
new CTesp : bitstring;
if (Lessthan(ElapsedTime(CTesp, xT), dt)) then
let xX1w = HashFunTwo(xIDw, s) in
let xRPWw = XORFun(xY1w, HashFunTwo(xIDw, xX1w)) in
let xX4w = XORFun(XORFun(xY2w, HashFunTwo(xAr, xX1w)), HashFunThree(s, Qesp, xX5w)) in
let xrespw = XORFun(HashFunTwo(xRPWw, xX1w), xX4w) in
let xxVresp = HashFunSix(xIDr, xIDw, xLoc, xT, xRPWw, xrespw) in
if (xVresp = xxVresp) then
let saesp = MulFun(s, aesp) in
let Aesp = Cheb(saesp, x, p) in
let Kespr_ESP = Cheb(saesp, xAr, p) in
let SK_esp_r_ESP = HashFunFour(xIDr, IDesp, xT, Kespr_ESP) in
out(net, SEncrypt(SK_esp_r, SK_esp_r_ESP));
let Temp5 = SymDec(Eespi, s) in
let IDi_ESP = Separate_First(Temp5) in
out(net, SEncrypt(IDi, IDi_ESP));
let Qi = Separate_Second(Temp5) in
let xHespi = HashFunThree(xLoc, IDi_ESP, Qi) in
if (Hespi = xHespi) then
let XIDespi = XORFun(ConcatTwo(IDi_ESP, Qi), HashFunOne(SK_esp_r_ESP)) in
let Cespr = HashFunOne(XORFun(HashFunTwo(IDi_ESP, s), HashFunThree(xAr, xT, xIDr))) in
let Vesp = HashFunFour(IDi_ESP, Qi, SK_esp_r_ESP, Cespr) in
event startRr;
out (net, (XIDespi, Cespr, Aesp, Vesp));
event endESP.

(* ISMi *)
let pISMi=
in (net, (xX1r : bitstring, xxAr : bitstring, xxCespr : bitstring, xVri : bitstring));
let xxVri = HashFunFour(IDi, xxCespr, xxAr, xX1r) in
if (xVri = xxVri) then
let Temp6 = DivideFun(xX1r, Cheb(ri, xxAr, p)) in
let xxT = Separate_First(Temp6) in
let xxIDr = Separate_Second(Temp6) in
new CTi : bitstring;
if (Lessthan(ElapsedTime(CTi, xxT), dt)) then
let Temp7 = XORFun(Yi, HashFunTwo(ri, seriali)) in
let xxxCespr = HashFunOne(XORFun(Temp7, HashFunThree(xxAr, xxT, xxIDr))) in
if (xxCespr = xxxCespr) then
let riai = MulFun(ri, ai) in
let Ai = Cheb(riai, x, p) in
let Kri_ISM = Cheb(riai, xxAr, p) in
let SK_r_i_ISM = HashFunFour(IDi, xxIDr, xxT, Kri_ISM) in
out(net, SEncrypt(SK_r_i, SK_r_i_ISM));
let Vi = HashFunOne(SK_r_i_ISM) in
out (net, (Ai, Vi));
event endISMi.

process
( (!pRr) | (!pESP) | (!pISMi) )

Output:
-- Query inj-event(endISMi) ==> inj-event(startISMi)
Completing...
Starting query inj-event(endISMi) ==> inj-event(startISMi)
RESULT inj-event(endISMi) ==> inj-event(startISMi) is true.
-- Query inj-event(endRr) ==> inj-event(startRr)
Completing...
Starting query inj-event(endRr) ==> inj-event(startRr)
RESULT inj-event(endRr) ==> inj-event(startRr) is true.
-- Query inj-event(endESP) ==> inj-event(startESP)
Completing...
Starting query inj-event(endESP) ==> inj-event(startESP)
RESULT inj-event(endESP) ==> inj-event(startESP) is true.
-- Query not attacker(IDi[])
Completing...
Starting query not attacker(IDi[])
RESULT not attacker(IDi[]) is true.
-- Query not attacker(IDr[])
Completing...
Starting query not attacker(IDr[])
RESULT not attacker(IDr[]) is true.
-- Query not attacker(IDw[])
Completing...
Starting query not attacker(IDw[])
RESULT not attacker(IDw[]) is true.
-- Query not attacker(ri[])
Completing...
Starting query not attacker(ri[])
RESULT not attacker(ri[]) is true.
-- Query not attacker(rr[])
Completing...
Starting query not attacker(rr[])
RESULT not attacker(rr[]) is true.
-- Query not attacker(s[])
Completing...
Starting query not attacker(s[])
RESULT not attacker(s[]) is true.
-- Query not attacker(ai[])
Completing...
Starting query not attacker(ai[])
RESULT not attacker(ai[]) is true.
-- Query not attacker(ar[])
Completing...
Starting query not attacker(ar[])
RESULT not attacker(ar[]) is true.
-- Query not attacker(aesp[])
Completing...
Starting query not attacker(aesp[])
RESULT not attacker(aesp[]) is true.
-- Query not attacker(SK_r_i[])
Completing...
Starting query not attacker(SK_r_i[])
RESULT not attacker(SK_r_i[]) is true.
-- Query not attacker(SK_esp_r[])
Completing...
Starting query not attacker(SK_esp_r[])
RESULT not attacker(SK_esp_r[]) is true.