(* public communication channel *) free c. (* public identity of MS *) free imsi_wtn. (* constant values *) fun Fail/0. fun reject/0. fun page/0. fun pagingReq/0. fun pagingResp/0. fun imsiReq/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. (* New key generation function *) fun f/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 ( out(c, aenc(pbN, r_ms, (Fail, imsi, 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 ID_MS = new r; in(c, req); if req = imsiReq then ( out(c, aenc(pbN, r, imsi))). let ID_SN = out(c, imsiReq); in(c, ximsi). let PAGING_MS = in(c, x); let (msgtype, xrand, xblob) = x in ( if msgtype = pagingReq then ( let (xpage, ximsi, =sqn_p, xchall) = sdec(f(k, xrand), xblob) in ( if xpage = page then ( if imsi = ximsi then ( out(c, (pagingResp, xchall))))))). let PAGING_SN = new rand; new chall; new r_sn1; let UK = f(k, rand) in ( out(c, (pagingReq, rand, senc(UK, r_sn1, (page, imsi, sqn_p, chall)))); in(c, pres)). let MS = (AKA_MS|ID_MS|PAGING_MS). let SN = (AKA_SN|ID_SN|PAGING_SN). process new pvN; let pbN = pub(pvN) in out(c, pbN); ((! (new k; new imsi; new otmsi; (!new osqn; new sqn_p; ((MS) | (SN))))) | (new k; new id; new otmsi; let imsi = choice[id, imsi_wtn] in ( !new osqn; new sqn_p; ((MS) | (SN)))))