(* The Needham-Schroeder symmetric-key protocol *)

pred c/1 elimVar, decompData.


fun encrypt/2.
fun host/1.
fun dec/1.

query c:(x, encrypt(x,k[Kas[],Kbs[],Na[host[Kbs[]]]])).
(* known-pair attack against Kab (fails) *)

(* query c:(x, encrypt(x,Kas[])).*)
(* known-pair attack against Kas *)

(* query c:(x, encrypt(x,Kbs[])).*)
(* known-pair attack against Kbs *)

(* query c:(encrypt(challenge[],Kab[])). *)
(* chosen-plaintext attack against Kab (fails) *)

(* query c:(encrypt(challenge[],Kas[])). *)
(* chosen-plaintext attack against Kas *)

(* query c:(encrypt(challenge[],Kbs[])). *)
(* chosen-plaintext attack against Kbs *)

not c:Kas[].
not c:Kbs[].

reduc

(* Initialisation *)
c:host(Kas[]);
c:host(Kbs[]);
c:challenge[];

(* Attacker *)
c:k & c:encrypt(m,k) -> c:m;
c:x -> c:host(x);
c:x & c:y -> c:encrypt(x,y);

(* Additional properties for CBC *)
c:encrypt((m,n),k) -> c:(encrypt(m,k),encrypt(n,k));

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

(* not required for the attacks and commented out

c:encrypt(m1,k) & c:encrypt(m2,k) -> c:encrypt((m1,rnd[m1,m2]),k);
c:encrypt((m1,m2),k) & c:encrypt(m3,k) ->
        c:encrypt((m1,(m2,rnd[m2,m3])),k);
c:encrypt((m1,(m2,m3)),k) & c:encrypt(m4,k) ->
        c:encrypt((m1,(m2,(m3,rnd[m3,m4]))),k);
c:encrypt((m1,(m2,(m3,m4))),k) & c:encrypt(m5,k) ->
        c:encrypt((m1,(m2,(m3,(m4,rnd[m4,m5])))),k);
 
c:encrypt(m1,k) & c:encrypt((m2,m3),k)
        -> c:encrypt((m1,(rnd[m1,m2],m3)),k);
c:encrypt((m1, m2),k) & c:encrypt((m3,m4),k)
        -> c:encrypt((m1,(m2,(rnd[m2,m3],m4))),k);
c:encrypt((m1, m2, m3),k) & c:encrypt((m4,m5),k)
        -> c:encrypt((m1,(m2,(m3,(rnd[m3,m4],m5)))),k);
*)

(* A *)
c:h -> c:(host(Kas[]), h, Na[h]);
c:encrypt((Na[h], (h, (key, m))), Kas[]) -> c:m;
c:encrypt((Na[h], (h, (key, m))), Kas[]) & c:encrypt((n), key)
-> c:encrypt(dec(n), key);

(* B *)
c:encrypt((key, h), Kbs[]) -> c:encrypt((Nb[key,h]), key);

(* S *)
c:(host(Ks1), host(Ks2), n) ->
c:encrypt((n, (host(Ks2), (k[Ks1, Ks2, n],
                encrypt((k[Ks1, Ks2, n], host(Ks1)), Ks2)))), Ks1).