free c: channel. type host. type pkey. type skey. (* Public key encryption *) fun pk(skey): pkey. fun aenc(bitstring, pkey): bitstring. reduc forall x: bitstring, y: skey; adec(aenc(x,pk(y)),y) = x. (* 2 honest host names A and B *) free A, B, C: host. free nb: bitstring [private]. event beginA(host,host,bitstring). event beginB(host,host,bitstring). event endA(host,host,bitstring). event endB(host,host,bitstring). event toto(bitstring). (*query z:bitstring; event(endA(A,B,z)) ==> event(beginB(A,B,z)).*) query attacker (nb). (* Si A finit en ayant reçu nb, c'est que ça vient de B. *) query z:bitstring; event(endA(A,B,z)) ==> event(beginB(A,B,z)). (* Si B termine, c'est que A a bien reçu nb. *) query z:bitstring; event(endB(A,B,z)) ==> event(beginA(A,B,z)). let clientA(pkA:pkey,skA:skey,pkB:pkey,IdA:host,IdB:host) = new n:bitstring; out(c,aenc((IdA,n),pkB)); in(c,x:bitstring); let (=IdB,=n,y:bitstring)=adec(x,skA) in event beginA(IdA,IdB,y); out(c,aenc(y,pkB)); event endA(IdA,IdB,y). let clientB(pkB:pkey,skB:skey,pkA:pkey,IdA:host,IdB:host,n:bitstring) = in(c,x:bitstring); let (=IdA,na: bitstring) = adec(x,skB) in event beginB(IdA,IdB,n); out(c,aenc((IdB,na,n),pkA)); in(c,y:bitstring); if adec(y,skB) = n then event endB(IdA,IdB,n) else 0. process new skA:skey; new skB:skey; new skC:skey; let pkA= pk(skA) in out(c,pkA); let pkB = pk(skB) in out(c,pkB); let pkC = pk(skC) in out(c,skC); (!clientA(pkA,skA,pkB,A,B) | !new n:bitstring; clientB(pkB,skB,pkA,A,B,n) | clientB(pkB,skB,pkA,A,B,nb) | !clientA(pkA,skA,pkC,A,C) | !new n:bitstring; clientB(pkB,skB,pkC,C,B,n) | !clientA(pkB,skB,pkA,B,A) | !new n:bitstring;clientB(pkA,skA,pkB,B,A,n) | !clientA(pkB,skB,pkC,B,C) | !new n:bitstring;clientB(pkA,skA,pkC,C,A,n) )