(* Bellovin, Merritt, Oakland 92, section 2.1 Version in which A and B talk to anybody *) free c. (* Symmetric cryptography One does not know whether decryption succeeds or not For use with weak secrets *) fun enc/2. fun dec/2. equation dec(enc(x,y),y) = x. equation enc(dec(x,y),y) = x. (* Symmetric cryptography One knows whether decryption succeeds or not *) fun senc/2. reduc sdec(senc(x,y),y) = x. (* Public key cryptography *) fun penc/2. fun pk/1. reduc pdec(penc(x,pk(y)),y) = x. (* Host name *) fun host/2. free hostA, hostB. private free P. let processA = new sEA; let EA = pk(sEA) in out(c, (hostA, enc(EA, P))); in(c,m2); let R = pdec(dec(m2,P),EA) in new challengeA; out(c, senc((challengeA), R)); in(c, m4); let (=challengeA, challengeB) = sdec(m4, R) in out(c, senc((challengeB), R)). let processB = in(c, (=hostX, m)); let EA = dec(m, P) in new R; out(c, enc(penc(R, EA), P)); in(c,m3); let (challengeA) = sdec(m3, R) in new challengeB; out(c, senc((challengeA, challengeB), R)); in(c, m5); if sdec(m5, R) = (challengeB) then 0. let processAtalkingX = in(c, (PA,PB)); let hostX = host(PA,PB) in let P = PA in processA. let processBtalkingX = in(c, (PA,PB)); let hostX = host(PA,PB) in let P = PB in processB. process (!let hostX = hostB in processA) | (!let hostX = hostA in processB) | (!processAtalkingX) | (!processBtalkingX) | (phase 1; new w; out(c, choice[w,P]))