(*

WooLam shared-key auth protocol (1992, computer)
Corrections of Gordon, Jeffrey CSFW'01
Simplified model in which A talks only to B and conversely.

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].

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, ());
	out(c2, A);
	in(c3, n:nonce);
	event beginAfull(B, A, n);
	out(c4, enc(concat1(tag3, B, n), kAS)).

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

let processS(kAS: key, kBS: key) =
	in(c11, (=A, =B, m:ciphertext));
	let injbot(concat1(=tag3, =B, n)) = dec(m, kAS) in
	out(c12, enc(concat1(tag5, A, n), kBS)).

process 
	in(start, ());
	new kAS: key;
	new kBS: key;
	out(c13, ());
	((! NA processA(kAS)) |
	 (! NB processB(kBS)) | 
	 (! NS processS(kAS, kBS)))