(* JFKr *) (* Exponential and Diffie-Hellman *) data g/0. fun exp/2. equation exp(exp(g,y),z) = exp(exp(g,z),y). (* Signature *) fun S/2. fun Pk/1. data true/0. fun V/3. fun RecoverKey/1. fun RecoverText/1. equation V(S(k,v), Pk(k),v) = true. equation RecoverKey(S(k,v)) = Pk(k). (* For the attacker *) equation RecoverText(S(k,v)) = v. (* For the attacker *) (* Shared-key encryption *) fun E/2. fun D/2. equation D(k,E(k,v)) = v. (* Keyed hash function *) fun H/2. (* Sets data consset/2. data emptyset/0. pred member/2. clauses member:x,consset(x,y); member:x,y -> member:x,consset(z,y). *) (* Tags *) data tagE/0. data tagA/0. data tagV/0. (* Constructors for JFK's formatted messages Selectors are implicit when using "data" *) data cons1/2. data cons2/5. data cons3/7. data cons4/2. (* More constants *) data constI/0. data constR/0. data saR/0. (* Free names *) free c. (* Public channel *) free pub, genprinc, getexponential, grpinfoR, init, getprinc. (* Secrecy assumptions *) not kAminus phase 0. not d. (* Initiator The process processI corresponds to I^A in the figure. *) let processI = ! in(exponent, (dI, xI)); ! in(init, dummy); (* Init message *) new NI; out(c, cons1(NI, xI)); in(c, cons2(=NI, NR, xR, grpinfoR, tR)); let h = exp(xR, dI) in let Ka = H(h, (NI, NR, tagA)) in let Ke = H(h, (NI, NR, tagE)) in let Kv = H(h, (NI, NR, tagV)) in let sI = S(kAminus, (NI, NR, xI, xR, grpinfoR)) in out(getI, (dummy, NI, NR, xI, xR, tR, Ka, Ke, Kv, sI)). (* Responder The process processR corresponds to R^A in the figure. *) let processR = ! in(exponent, (dR, xR)); ! in(c, cons1(NI, xI)); new NR; new tR; out(c, cons2(NI, NR, xR, grpinfoR, tR)); new l; ( ( ! in(c, cons3(=NI,=NR,xI,=xR,=tR,eI,hI)); out(l, (xI,eI,hI)) ) | ( in(l, (xI,eI,hI)); processR4 ) ). let processR4 = let h = exp(xI,dR) in let Ka = H(h, (NI, NR, tagA)) in let Ke = H(h, (NI, NR, tagE)) in let Kv = H(h, (NI, NR, tagV)) in let sR = S(kAminus, (NI, NR, xI, xR)) in out(getR, (NI, NR, xI, xR, tR, eI, hI, Ka, Ke, Kv, sR)). (* Whole JFK system. *) process new ids; new exponent; ( ! new d; let x = exp(g,d) in out(getexponential, x); ! out(exponent, (d,x)) ) | ( ! new kAminus; let IDA = Pk(kAminus) in new init; new getI; new getR; out(getprinc, (IDA, getI, getR, init)); ( processI | processR | !out(ids, (kAminus, IDA))) ) | ( in(pub, NR); in(exponent, (dI,xI)); in(exponent, (dR,xR)); in(ids, (kARminus, IDAR)); in(ids, (kAIminus, IDAI)); in(init, (IDRp, saI)); new NI; new NeI; new NhI; new NeR; new NhR; new NKv; let h = exp(xR,dI) in let Ka = H(h, (NI, NR, tagA)) in let Ke = H(h, (NI, NR, tagE)) in let Kv = H(h, (NI, NR, tagV)) in let sR = S(kARminus, (NI, NR, xI, xR)) in let eR = E(Ke, (IDAR, saR, sR)) in let hR = H(Ka, (constR, eR)) in let sI = S(kAIminus, (NI, NR, xI, xR, grpinfoR)) in let eI = E(Ke, (IDAI, IDRp, saI, sI)) in let hI = H(Ka, (constI, eI)) in out(pub, (NI, choice[eI, NeI], choice[hI, NhI], choice[eR, NeR], choice[hR, NhR], choice[Kv, NKv])) ) (* With in(pub, (NR, xR)), the attacker chooses xR = g, so h = exp(g, dI) = xI hence an attack *) (* Let us name S' the above process. Let us define the context C as follows: C = new getprinc; ( [] | ! in(getprinc, (IDA, getI, getR, init)); new connect; new accept; new channelSIA; out(getprinc2, (IDA, init, accept, connect, channelSIA)); in(channelSIA, SIA); ( processI2 | processR2 ) ) let processI2 = ! in(getI, ((IDRp, saI), NI, NR, xI, xR, tR, Ka, Ke, Kv, sI)); let eI = E(Ke, (IDA, IDRp, saI, sI)) in let hI = H(Ka, (constI, eI)) in out(c, cons3(NI, NR, xI, xR, tR, eI, hI)); in(c, cons4(eR, hR)); if H(Ka, (constR, eR)) = hR then let (IDRl, saR, sR) = D(Ke, eR) in if V(sR, IDRl, (NI, NR, xI, xR)) = true then out(connect, (IDRl, IDRp, saI, saR, Kv)). let processR2 = ! in(getR, (NI, NR, xI, xR, tR, eI, hI, Ka, Ke, Kv, sR)); if H(Ka, (constI, eI)) = hI then let (IDIl, IDRp, saI, sI) = D(Ke,eI) in if member:IDIl,SIA then if V(sI, IDIl, (NI, NR, xI, xR, grpinfoR)) = true then out(accept, (IDIl, IDRp, saI, saR, Kv)); let eR = E(Ke, (IDA, saR, sR)) in let hR = H(Ka, (constR, eR)) in out(c, cons4(eR, hR)). The full JFKr script S (version without cache) is weakly observationally equivalent to C[S'] (more precisely, fst(S) is equivalent to fst(C[S']) and snd(S) is equivalent to snd(C[S'])). This is proved by eliminating communications on the private channel getprinc and on each instance of getI and getR. ProVerif shows that S' satisfies equivalence, then so does C[S'] by the contextual property of equivalence, then fst(S) is weakly observationally equivalent to snd(S). *)