(* Needham Shroeder Lowe public key protocol *)

pred c/1 elimVar, decompData.

fun pk/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));

(* encoding ciphertext concatenation property up to messages of size 5 *)

(* not required for the attacks and commented out

c:encrypt(m1,pk(x)) & c:encrypt(m2,pk(x)) -> c:encrypt((m1,rnd[m1,m2]),pk(x));
c:encrypt((m1,m2),pk(x)) & c:encrypt(m3,pk(x)) ->
        c:encrypt((m1,(m2,rnd[m2,m3])),pk(x));
c:encrypt((m1,(m2,m3)),pk(x)) & c:encrypt(m4,pk(x)) ->
        c:encrypt((m1,(m2,(m3,rnd[m3,m4]))),pk(x));
c:encrypt((m1,(m2,(m3,m4))),pk(x)) & c:encrypt(m5,pk(x)) ->
        c:encrypt((m1,(m2,(m3,(m4,rnd[m4,m5])))),pk(x));
 
c:encrypt(m1,pk(x)) & c:encrypt((m2,m3),pk(x))
        -> c:encrypt((m1,(rnd[m1,m2],m3)),pk(x));
c:encrypt((m1, m2),pk(x)) & c:encrypt((m3,m4),pk(x))
        -> c:encrypt((m1,(m2,(rnd[m2,m3],m4))),pk(x));
c:encrypt((m1, m2, m3),pk(x)) & c:encrypt((m4,m5),pk(x))
        -> c:encrypt((m1,(m2,(m3,(rnd[m3,m4],m5)))),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 *)

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

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



(* B *) 

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

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