(* Needham-Schroeder public key *) free c. (* Public key cryptography *) fun pk/1. fun encrypt/2. reduc decrypt(encrypt(x,pk(y)),y) = x. (* Signatures *) fun sign/2. reduc getmess(sign(m,k)) = m. reduc checksign(sign(m,k), pk(k)) = m. (* Host name / key The server has a table (host name, public key), which we represent by the function getkey. *) fun host/1. private reduc getkey(host(x)) = x. (* Shared-key cryptography *) fun sencrypt/2. reduc sdecrypt(sencrypt(x,y),y) = x. private free secretA_Na, secretA_Nb, secretB_Na, secretB_Nb. query attacker:secretA_Na; attacker:secretA_Nb; attacker:secretB_Na; attacker:secretB_Nb. query ev:endB(x,y) ==> ev:beginA(x,y). query ev:endA(x,y,z) ==> ev:beginB(x,y,z). let processA = in(c, xpkB); new Na; event beginA(xpkB, Na); out(c, encrypt((pkA, Na), xpkB)); in(c, m2); let (=Na, xNb) = decrypt(m2, skA) in out(c, encrypt(xNb, xpkB)); (* Test for secrecy *) if xpkB = pkB then event endA(pkA, Na, xNb); out(c, sencrypt(secretA_Na, Na)); out(c, sencrypt(secretA_Nb, xNb)). let processB = in(c, m1); let (xpkA, xNa) = decrypt(m1, skB) in new Nb; event beginB(xpkA, xNa, Nb); out(c, encrypt((xNa, Nb), xpkA)); in(c, m3); if Nb = decrypt(m3, skB) then (* Test for secrecy *) if xpkA = pkA then event endB(pkB, xNa); out(c, sencrypt(secretB_Na, xNa)); out(c, sencrypt(secretB_Nb, Nb)). process new skA; let pkA = pk(skA) in out(c, pkA); new skB; let pkB = pk(skB) in out(c, pkB); ((!processA) | (!processB))