(* Needham Shroeder Lowe public key protocol, with explicit integrity *)

pred c/1 elimVar, decompData.

fun pk/1.
fun hash/1.
fun encrypt/2.
fun decrypt/2.


query c:Na[pk(sB[])].
(* Secrecy of Na *)

(* query c:Nb[Na[pk(sB[])],pk(sA[])].*)
(* Secrecy of Nb *)

(* query c: (encrypt(challengePlainText[],pk(sA[])),challengePlainText[]).*)
(* chosen ciphertext attack against pkA *)

(* query c: (encrypt(challengePlainText[],pk(sB[])),challengePlainText[]).*)
(* chosen ciphertext attack against pkB *)

not c:sA[].
not c:sB[].

reduc
(* Initialization *)

c:encrypt(challengePlainText[],pk(sA[]));
c:encrypt(challengePlainText[],pk(sB[]));

c:c[];
c:pk(sA[]);
c:pk(sB[]);

(* The attacker *)

c:x & c:encrypt(m,pk(x)) -> c:m;
c:x -> c:pk(x);
c:x & c:y -> c:encrypt(x,y);

(* CBC additional attacker capabilities *)

c:encrypt((m,n),pk(x)) -> c:(encrypt(m,pk(x)),encrypt(n,pk(x)));
c:encrypt(m,pk(x)) & c:n & c:pk(x) -> c:encrypt((m,n),pk(x));

(* ECB adds the following additional capability *)

c:encrypt(m,pk(x)) & c:n & c:pk(x) -> c:encrypt((n,m),pk(x));



(* The protocol *)


(* A *)

c:pk(x) -> c:encrypt((Na[pk(x)],(pk(sA[]),hash((Na[pk(x)],pk(sA[]))))), pk(x));

c:pk(x) &
c:encrypt((Na[pk(x)], (y, (pk(x),hash((Na[pk(x)], (y, pk(x))))))), pk(sA[]))
	-> c:encrypt((y,hash(y)), pk(x));

(* B *) 

c:encrypt((x,(y,hash((x,y)))), pk(sB[])) ->
   c:encrypt((x, (Nb[x,y], (pk(sB[]),hash((x, (Nb[x,y], pk(sB[]))))))), y).