AKE.pv

(*** AKE Scheme ***)
(* Data types *)
type Key.
type Point.
type Random.
type ID.
type Time.

(* Chael Definition *)
free net : chael.

(* Private Terms *)
free SKij : bitstring [private].
free ai : Random [private].
free aj : Random [private].
free ki : Key [private].
free kj : Key [private].
free Kj : Key [private].
free IDi : ID [private].

(* Public Terms *)
free IDj : ID.
free Qi : Point.
free Qj : Point.
free WTi : Point.
free WTj : Point.
const P : Point.
const Ppub : Point.
free pubkey : Key.
const dt : Time.

(* Functions *)
fun HashFunOne(ID, Point) : bitstring.
fun HashFunTwo(ID, Point, Point, Point, Time) : bitstring.
fun HashFunThree(ID, ID, bitstring, Point) : Key.
fun MulFunOne(Random, Key) : Random.
fun MulFunTwo(Random, Point) : Point.
fun MulFunThree(Key, Point) : Point.
fun MulFunFour(bitstring, Point) : Point.
fun Add(Point, Point) : Point.
fun ElapsedTime(Time, Time) : Time.
fun Lessthan(Time, Time) : bool.
fun Encryptid(Key, bitstring, ID): bitstring.
fun ConcatOne(ID, Point) : bitstring.
fun ConcatTwo(Point, Point, bitstring, bitstring) : bitstring.
fun SEncrypt(bitstring, Key): bitstring.
fun Separate_ID(bitstring): ID.
fun Separate_Point(bitstring): Point.

(* Destructors *)
reduc forall pubKey : Key, M : bitstring, id : ID, deckey : Key; Decryptid(Encryptid(pubKey, M, id), deckey) = M.
reduc forall x: bitstring, y: Key; SDecrypt(SEncrypt(x,y), y) = x.

(* queries *)
query attacker (SKij).
query attacker (ai).
query attacker (aj).
query attacker (ki).
query attacker (kj).
query attacker (IDi).
query inj-event ( endSMi ) ==> inj-event (startSMi).
query inj-event ( endSPj ) ==> inj-event (startSPj).

(* Events *)
event startSPj.
event endSPj.
event startSMi.
event endSMi.

(* SMi *)
let pSMi=
let Ai = MulFunTwo(ai, Qi) in
let (TiCi : bitstring) = Encryptid(pubkey, ConcatOne(IDi, WTi), IDj) in
let Bi = MulFunThree(ki,(Add(WTj, MulFunFour(HashFunOne(IDj, WTj), Ppub)))) in
new CTi : Time;
let Vi = HashFunTwo(IDi, Ai, Bi, WTi, CTi) in
event startSPj;
out (net, (TiCi, Ai, Vi, CTi));
in(net, (xAj : Point, xVj : bitstring, xnCTj : Time));
new nCTi : Time;
if (Lessthan(ElapsedTime(nCTi, xnCTj), dt)) then
let xxVj = HashFunTwo(IDj, xAj, Bi, WTj, xnCTj) in
if (xVj = xxVj) then
let aiki = MulFunOne(ai, ki) in
let Kij = MulFunTwo(aiki, xAj) in
let Trans = ConcatTwo(Ai, xAj, Vi, xVj) in
let SKij_SMi = HashFunThree(IDj, IDi, Trans, Kij) in
out(net, SEncrypt(SKij, SKij_SMi));
event endSMi.

(* SPj *)
let pSPj=
in(net, (xTiCi : bitstring, xAi : Point, xVi : bitstring, xCTi : Time));
new CTj : Time;
if (Lessthan(ElapsedTime(CTj, xCTi), dt)) then
let (xIDiWTi : bitstring) = Decryptid(xTiCi, Kj) in
let xIDi = Separate_ID(xIDiWTi) in
let xWTi = Separate_Point(xIDiWTi) in
let Bj = MulFunThree(kj,(Add(xWTi, MulFunFour(HashFunOne(xIDi, xWTi), Ppub)))) in
let xxVi = HashFunTwo(xIDi, xAi, Bj, xWTi, xCTi) in
if (xVi = xxVi) then
let Aj = MulFunTwo(aj, Qj) in
let Vj = HashFunTwo(IDj, Aj, Bj, WTj, CTj) in
event startSMi;
new nCTj : Time;
out (net, (Aj, Vj, nCTj));
let ajkj = MulFunOne(aj, kj) in
let Kji = MulFunTwo(ajkj, xAi) in
let Trans = ConcatTwo(xAi, Aj, xVi, Vj) in
let SKij_SPj = HashFunThree(IDj, xIDi, Trans, Kji) in
out(net, SEncrypt(SKij, SKij_SPj));
event endSPj.

process
( (!pSPj) | (!pSMi) )

Output:

-- Query inj-event(endSPj) ==> inj-event(startSPj)
Completing...
Starting query inj-event(endSPj) ==> inj-event(startSPj)
RESULT inj-event(endSPj) ==> inj-event(startSPj) is true.
-- Query inj-event(endSMi) ==> inj-event(startSMi)
Completing...
Starting query inj-event(endSMi) ==> inj-event(startSMi)
RESULT inj-event(endSMi) ==> inj-event(startSMi) is true.
-- Query not attacker(IDi[])
Completing...
Starting query not attacker(IDi[])
RESULT not attacker(IDi[]) is true.
-- Query not attacker(kj[])
Completing...
Starting query not attacker(kj[])
RESULT not attacker(kj[]) is true.
-- Query not attacker(ki[])
Completing...
Starting query not attacker(ki[])
RESULT not attacker(ki[]) is true.
-- Query not attacker(aj[])
Completing...
Starting query not attacker(aj[])
RESULT not attacker(aj[]) is true.
-- Query not attacker(ai[])
Completing...
Starting query not attacker(ai[])
RESULT not attacker(ai[]) is true.
-- Query not attacker(SKij[])
Completing...
Starting query not attacker(SKij[])
RESULT not attacker(SKij[]) is true.