(* Needham Schroeder public key protocol. *)

(* In order to determine the proof, use interactive mode: 
   set interactiveMode = true.
The proof is as follows: *)

proof {
crypto uf_cma(sign) rkS;
(* crypto ind_cca2(enc) rkA;
crypto ind_cca2(enc) rkB;
success; *)
auto
}

param NA, NB, NS, NK.

type nonce [large,fixed].
type host [bounded].
type pkey [bounded].
type skey [bounded].
type keyseed [large,fixed].
type spkey [bounded].
type sskey [bounded].
type skeyseed [large,fixed].
type signature [bounded].
type blocksize [fixed].
type sblocksize [bounded].

fun concat1(nonce, host):blocksize [data].
fun concat2(nonce, nonce, host):blocksize [data].
fun concat3(pkey, host):sblocksize [data].
fun pad(nonce):blocksize [data].

equation forall z:nonce,t:nonce,u:host,y2:nonce,z2:host;
	concat2(z,t,u) <> concat1(y2,z2).
equation forall y:nonce,y2:nonce,z2:host;
	pad(y) <> concat1(y2,z2).
equation forall z:nonce,t:nonce,u:host,y2:nonce;
	concat2(z,t,u) <> pad(y2).

(* Public-key encryption (CCA2) *)

proba Penc.
proba Penccoll.

expand IND_CCA2_public_key_enc(keyseed, pkey, skey, blocksize, bitstring, skgen, pkgen, enc, dec, injbot, Z, Penc, Penccoll).

const Zblocksize: blocksize.
equation forall x: blocksize; Z(x) = Zblocksize.

(* Signatures *)

proba Psign.
proba Psigncoll.

expand UF_CMA_proba_signature(skeyseed, spkey, sskey, sblocksize, signature, sskgen, spkgen, sign, check, Psign, Psigncoll).

table keys(host, pkey).

(* Queries *)

channel c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, 
	c15, c16, c17, start, finish.
const A : host.
const B : host.

event beginA(host, host, nonce, nonce).
event endA(host, host, nonce, nonce).
event beginB(host, host, nonce, nonce).
event endB(host, host, nonce, nonce).

query x:host, y:host, na:nonce, nb:nonce;
	event(endA(x,y,na,nb)) ==> event(beginB(x,y,na,nb)).
query x:host, y:host, na:nonce, nb:nonce;
	event(endB(x,y,na,nb)) ==> event(beginA(x,y,na,nb)).
query x:host, y:host, na:nonce, nb:nonce;
	inj-event(endA(x,y,na,nb)) ==> inj-event(beginB(x,y,na,nb)).
query x:host, y:host, na:nonce, nb:nonce;
	inj-event(endB(x,y,na,nb)) ==> inj-event(beginA(x,y,na,nb)).

let processA(skA:skey, pkS:spkey) =
	in(c1, hostX: host);
	out(c2, (A, hostX));
	in(c3, (pkX: pkey, =hostX, ms: signature));
	if check(concat3(pkX, hostX), pkS, ms) then
	(* Message 3 *)
        new Na: nonce;
        out(c4, enc(concat1(Na, A), pkX));
	(* Message 6 *)
        in(c5, m: bitstring);
	let injbot(concat2(=Na, Nb, =hostX)) = dec(m, skA) in
	event beginA(A, hostX, Na, Nb);
	(* Message 7 *)
	out(c6, enc(pad(Nb), pkX));
	(* OK *)
	in(finish, ());
	if hostX = B then
	event endA(A, hostX, Na, Nb).

let processB(skB:skey, pkS:spkey) =
	(* Message 3 *)
	in(c7, m:bitstring);
	let injbot(concat1(Na, hostY)) = dec(m, skB) in
	out(c8, (B, hostY));
	in(c9, (pkY: pkey, =hostY, ms: signature));
	if check(concat3(pkY, hostY), pkS, ms) then
	(* Message 6 *)
	new Nb: nonce;
	event beginB(hostY, B, Na, Nb);
	out(c10, enc(concat2(Na, Nb, B), pkY));
	(* Message 7 *)
	in(c11, m3: bitstring);
	let injbot(pad(=Nb)) = dec(m3, skB) in
	(* OK *)
	if hostY = A then
	event endB(hostY, B, Na, Nb).

let processK(pkA: pkey, pkB: pkey) =
	in(c12, (Khost: host, Kkey: pkey));
	if Khost = A then insert keys(A, pkA) else
	if Khost = B then insert keys(B, pkB) else
	insert keys(Khost, Kkey).

let processS(skS: sskey) = 
	in(c13, (h1: host, h2: host));
	get keys(=h2, pk2) in
	out(c14, (pk2, h2, sign(concat3(pk2, h2), skS))).

process 
	in(start, ());
	new rkA: keyseed;
	let pkA = pkgen(rkA) in
	let skA = skgen(rkA) in
	new rkB: keyseed;
	let pkB = pkgen(rkB) in
	let skB = skgen(rkB) in
	new rkS: skeyseed;
	let pkS = spkgen(rkS) in
	let skS = sskgen(rkS) in
	out(c15, (pkA, pkB, pkS));
	((! NA processA(skA, pkS)) |
	 (! NB processB(skB, pkS)) | 
	 (! NS processS(skS)) |
	 (! NK processK(pkA, pkB)))


(* EXPECTED
All queries proved.
2.710s (user 2.700s + system 0.010s), max rss 96768K
END *)