(*

WooLam shared-key auth protocol (1992, computer)
Corrections of Gordon, Jeffrey CSFW'01

A -> B : A
B -> A : N (fresh)
A -> B : { m3, B, N }_kAS
B -> S : A,B,{ m3, B, N }_kAS
S -> B : { m5, A, N }_kBS
B: verify { m5, A, N }_kBS = the message from S

Correct.
*)

param NA, NB, NS, NK.

type nonce [large,fixed].
type host [bounded].
type key [fixed].
type tag [bounded].
type plaintext [bounded].
type ciphertext [bounded].

table keytbl (key, host).

fun concat1(tag, host, nonce):plaintext [data].

(* Shared-key encryption (IND-CPA + INT-CTXT) *)

proba Penc.
proba Pencctxt.

expand IND_CPA_INT_CTXT_sym_enc(key, plaintext, ciphertext, enc, dec, injbot, Z, Penc, Pencctxt).

(* The function Z returns for each bitstring, a bitstring
   of the same length, consisting only of zeroes. *)
const Zconcat1:plaintext.
equation forall y:tag, h:host, z:nonce; 
	Z(concat1(y,h,z)) = Zconcat1.

(* Queries *)

channel c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13,
	start, finish.

const A, B: host.
const tag3, tag5: tag.

event beginAfull(host, host, nonce).
event endB(host, host, nonce).

query x:host, y:host, z:nonce;
	inj-event(endB(x,y,z)) ==> inj-event(beginAfull(x,y,z)).

let processA(kAS: key) =
	in(c1, hostB2:host); (* Choose the B host *)
	out(c2, A);
	in(c3, n:nonce);
	event beginAfull(hostB2, A, n);
	out(c4, enc(concat1(tag3, hostB2, n), kAS)).

let processB(kBS: key) =
	in(c5, hostA2:host);
	new N:nonce;
	out(c6, N);
	in(c7, m:ciphertext);
	out(c8, (hostA2, B, m));
	in(c9, (m2:ciphertext));
	if injbot(concat1(tag5, hostA2, N)) = dec(m2, kBS) then
	(* OK *)
	if hostA2 = A then
	event endB(B, hostA2, N).

let processK =
	in(c10, (Khost: host, Kkey: key));
        if (Khost <> A) && (Khost <> B) then
           insert keytbl (Kkey, Khost).

let processS =
	in(c11, (hostA1:host, hostB0:host, m:ciphertext));
        get keytbl (kbs, =hostB0) in
        get keytbl (kas, =hostA1) in
	let injbot(concat1(=tag3, =hostB0, n)) = dec(m, kas) in
	out(c12, enc(concat1(tag5, hostA1, n), kbs)).

process 
	in(start, ());
	new kAS: key;
	new kBS: key;
        insert keytbl (kAS, A);
        insert keytbl (kBS, B);
	out(c13, ());
	((! NA processA(kAS)) |
	 (! NB processB(kBS)) | 
	 (! NS processS) |
	 (! NK processK))