Key Establishment Protocol

(********************** Key Establishment Protocol *************************)
(* Data types *)
type Key.
type Point.
type Random.
type ID.

(* Chael Definition *)
free net : chael.

(* Private Terms *)
free SSKnm : Key [private].
const skm : Key [private].
const sn : Key [private].
const rn : Key [private].

(* Public Terms *)
const IDm : ID.
const IDn : ID.
const PKm : Point.
const PKn : Point.

(* Functions *)
fun ScalarMul(Random, Point) : Point.
fun MulTwo(Random, Key) : Random.
fun MulThree(Random, Key, bitstring) : Random.
fun HashFunTwo(ID, Key) : bitstring.
fun HashFunFour(ID, Point, Point, Point) : bitstring.
fun HashFunFive(ID, ID, Point, Point, Point) : Key.
fun S_Encrypt(Key, Key): bitstring.

(* Destructors *)
reduc forall x : Key, y : Key; S_Decrypt(S_Encrypt(x,y), y) = x.

(* queries *)
query attacker (SSKnm).
query attacker (new ra).
query attacker (new rb).
query attacker (skm).
query attacker (sn).
query attacker (rn).
query inj-event (endSMm) ==> inj-event (startSMm).
query inj-event (endAHEn) ==> inj-event (startAHEn).

(* Events *)
event startSMm.
event endSMm.
event startAHEn.
event endAHEn.

(* SMm *)
let pSMm=
new ra : Random;
let A = ScalarMul(ra, PKm) in
event startAHEn;
out(net, (IDm, A));
in(net, (xB : Point, xVn : bitstring));
let C_SM = ScalarMul(MulTwo(ra, skm), xB) in
let xxVn = HashFunFour(IDn, A, xB, C_SM) in
if (xVn = xxVn) then
let SSKnm_SM = HashFunFive(IDn, IDm, A, xB, C_SM) in
out(net, S_Encrypt(SSKnm, SSKnm_SM));
let Vm = HashFunTwo(IDm, SSKnm_SM) in
out(net, (IDm, Vm));
event endSMm.

(* AHEn *)
let pAHEn=
new rb : Random;
let B = ScalarMul(rb, PKn) in
in(net, (xIDm : ID, xA : Point));
let temp1 = HashFunTwo(IDm, sn) in
let C_AHE = ScalarMul(MulThree(rb, rn, temp1), xA) in
let Vn = HashFunFour(IDn, xA, B, C_AHE) in
event startSMm;
out(net, (B, Vn));
in(net, (xxIDm : ID, xVm : bitstring));
let SSKnm_AHE = HashFunFive(IDn, xxIDm, xA, B, C_AHE) in
let xxVm = HashFunTwo(xxIDm, SSKnm_AHE) in
if (xVm = xxVm) then
out(net, S_Encrypt(SSKnm, SSKnm_AHE));
event endAHEn.

process
( (!pSMm) | (!pAHEn) )