(* public communication channel *) free c. (* public identity of MS *) free imsi_wtn. (* constant values *) fun Fail/0. fun reject/0. fun Sqn/0. (* UMTS AKA protocol specific mac and key generation functions *) fun f0/2. 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. (* public key generation function *) fun pub/1. (* public key encryption function *) fun aenc/3. reduc adec(k, aenc(pub(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, xsqn) = (mac, 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 ( new rand; new r; out(c, aenc(pbN, r_ms, (Fail, imsi, rand, senc(f0(k, rand), r, (Sqn, osqn))))))))))). 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 pvN; let pbN = pub(pvN) in out(c, pbN); ((! (new k; new imsi; new otmsi; (!new osqn; ((MS) | (SN))))) | (new k; new id; new otmsi; let imsi = choice[id, imsi_wtn] in ( !new osqn; ((MS) | (SN)))))