(* public communication channel *)
free c.
(* constant values *)
fun macFail/0.
fun syncFail/0.
fun reject/0.
(* UMTS AKA protocol specific mac and key generation functions *)
fun f1/2.
fun f2/2.
fun f3/2.
fun f4/2.
fun f5/2.
(* symmetric key encryption function *)
fun senc/3.
fun sdec/2.
equation sdec(k, senc(k, r, m)) = m.
let AKA_MS =
new r_ms;
in(c, x);
let (xrand, xautn) = x in (
let (msg, xmac) = xautn in (
let ak = f5(k, xrand) in (
let xsqn = sdec(ak, msg) in (
let mac = f1(k, (xrand, xsqn)) in (
if xmac = mac then (
if xsqn = osqn then (
let res = f2(k, xrand) in (
let ck = f3(k, xrand) in (
let ik = f4(k, xrand) in (
out(c, res);
in(c, xmsg)))))
else (out(c, syncFail)))
else (out(c, macFail))))))).
let AKA_SN =
new rand;
new r_sn;
new s;
new r;
let mac = f1(k, (rand, osqn)) in (
let res = f2(k, rand) in (
let ck = f3(k, rand) in (
let ik = f4(k, rand) in (
let ak = f5(k, rand) in (
let autn = (senc(ak, r_sn, osqn), mac) in (
let av = (rand, res, ck, ik, ak) in (
out(c, (rand, autn));
in(c, xres);
if xres = res then (
out(c, senc(ck, r, s))
)
else (
out(c, reject))))))))).
let MS = (AKA_MS).
let SN = (AKA_SN).
process (! (new sk1; new imsi1;new otmsi1;
(! (new sk2; new imsi2; new osqn; new otmsi2;
let imsi = choice[imsi1, imsi2] in (
let k = choice[sk1, sk2] in (
let otmsi = choice[otmsi1,otmsi2] in (
(MS) | (SN))))))))