/* 
Modelling of the Needham/Schröder key exchange protocol
with an attacker.

Termination of saturation is made possible
by clausal rewriting and proves the absense
of attacks. More specifically facts
c(secretA) and c(secretB) cannot be derived
hence the attacker cannot get hold of those
keys.

*/



c(B),c(C) -> c(tuple_2(B,C)).
c(tuple_2(B,C)) -> c(B).
c(tuple_2(B,C)) -> c(C).
c(B),c(C), c(D) -> c(tuple_3(B,C,D)).
c(tuple_3(B,C,D)) -> c(B).
c(tuple_3(B,C,D)) -> c(C).
c(tuple_3(B,C,D)) -> c(D).
c(B),c(C),c(D),c(E) -> c(tuple_4(B,C,D,E)).
c(tuple_4(B,C,D,E)) -> c(B).
c(tuple_4(B,C,D,E)) -> c(C).
c(tuple_4(B,C,D,E)) -> c(D).
c(tuple_4(B,C,D,E)) -> c(E).
c(B),c(encrypt(C,B)) -> c(C).
c(host(kas)).
c(host(kbs)).
c(B) -> c(host(B)).
c(kcs).
c(B),c(C) -> c(encrypt(B,C)).
c(B) -> c(decr(B)).
c(decr(B)) -> c(B).
c(B) -> c(tuple_3(host(kas),B,na(B))).
c(encrypt(tuple_4(na(B),B,C,D),kas)) -> c(D).
c(encrypt(tuple_4(na(B),B,C,D),kas)),c(encrypt(E,C)) -> c(encrypt(decr(E),C)).
c(encrypt(tuple_4(na(host(kbs)),host(kbs),B,C),kas)) -> c(encrypt(secretA,B)).
c(encrypt(tuple_2(B,C),kbs)) -> c(encrypt(nb(B,C),B)).
c(encrypt(tuple_2(B,host(kas)),kbs)),c(encrypt(decr(nb(B,host(kas))),B)) -> c(encrypt(secretB,B)).
c(tuple_3(host(B),host(C),D)) -> c(encrypt(tuple_4(D,host(C),k(B,C,D),encrypt(tuple_2(k(B,C,D),host(B)),C)),B)).
c(secretB) -> [].
c(secretA) -> [].

precedence([k,encrypt,tuple_4,tuple_3,'na','nb',decr]).
option([cnf(full),memo_constraints(on),crw_depth(1)]).

:-sama([]).             % We want saturation by ordered resolution w/o sel.
:-sarp([1-7,10-15]).    % the usual + clausal rewriting  
:-sams([3,19]).      



/*

Saturation terminated.

Persisting Clauses:

    1(1) : c(B),c(C) -> c(tuple_2(B,C))
    2(1) : c(tuple_2(B,C)) -> c(B)
    3(1) : c(tuple_2(B,C)) -> c(C)
    4(1) : c(B),c(C),c(D) -> c(tuple_3(B,C,D))
    5(1) : c(tuple_3(B,C,D)) -> c(B)
    6(1) : c(tuple_3(B,C,D)) -> c(C)
    7(1) : c(tuple_3(B,C,D)) -> c(D)
    8(1) : c(B),c(C),c(D),c(E) -> c(tuple_4(B,C,D,E))
    9(1) : c(tuple_4(B,C,D,E)) -> c(B)
   10(1) : c(tuple_4(B,C,D,E)) -> c(C)
   11(1) : c(tuple_4(B,C,D,E)) -> c(D)
   12(1) : c(tuple_4(B,C,D,E)) -> c(E)
   13(1) : c(encrypt(B,C)),c(C) -> c(B)
   14(1) : c(host(kas))
   15(1) : c(host(kbs))
   16(1) : c(B) -> c(host(B))
   17(1) : c(kcs)
   18(1) : c(B),c(C) -> c(encrypt(B,C))
   19(1) : c(B) -> c(decr(B))
   20(1) : c(decr(B)) -> c(B)
   21(1) : c(B) -> c(tuple_3(host(kas),B,na(B)))
   22(1) : c(encrypt(tuple_4(na(B),B,C,D),kas)) -> c(D)
   23(1) : c(encrypt(tuple_4(na(B),B,C,D),kas)),c(encrypt(E,C)) -> c(encrypt(decr(E),C))
   24(1) : c(encrypt(tuple_4(na(host(kbs)),host(kbs),B,C),kas)) -> c(encrypt(secretA,B))
   25(1) : c(encrypt(tuple_2(B,C),kbs)) -> c(encrypt(nb(B,C),B))
   26(1) : c(encrypt(decr(nb(B,host(kas))),B)),c(encrypt(tuple_2(B,host(kas)),kbs)) -> c(encrypt(secretB,B))
   27(1) : c(tuple_3(host(B),host(C),D)) -> c(encrypt(tuple_4(D,host(C),k(B,C,D),encrypt(tuple_2(k(B,C,D),host(B)),C)),B))
   28(1) : c(secretB) -> 
   29(1) : c(secretA) -> 
   31(2) : c(B) -> c(na(B))
   32(2) : c(encrypt(tuple_2(B,C),kbs)),c(B) -> c(nb(B,C))
   38(2) : c(B),c(tuple_3(host(B),host(C),D)) -> c(tuple_4(D,host(C),k(B,C,D),encrypt(tuple_2(k(B,C,D),host(B)),C)))
   39(2) : c(tuple_3(host(kas),host(B),na(host(B)))) -> c(encrypt(tuple_2(k(kas,B,na(host(B))),host(kas)),B))
   41(2) : c(tuple_3(host(kas),host(B),na(host(B)))),c(encrypt(C,k(kas,B,na(host(B))))) -> c(encrypt(decr(C),k(kas,B,na(host(B)))))
   43(3) : c(encrypt(tuple_2(B,host(kas)),kbs)),c(B) -> 
   44(3) : c(encrypt(secretA,k(kas,kbs,na(host(kbs)))))
   52(5) : c(k(kas,kbs,na(host(kbs)))) -> 
   54(6) : c(kbs) -> 
   56(6) : c(kas) -> 
   61(4) : c(B) -> c(tuple_2(k(kas,B,na(host(B))),host(kas)))
   62(5) : c(B) -> c(k(kas,B,na(host(B))))
   66(3) : c(B),c(tuple_3(host(B),host(C),D)) -> c(k(B,C,D))
   67(3) : c(B),c(tuple_3(host(B),host(C),D)) -> c(encrypt(tuple_2(k(B,C,D),host(B)),C))
   73(5) : c(B),c(tuple_3(host(B),host(kbs),C)) -> c(nb(k(B,kbs,C),host(B)))
   76(4) : c(encrypt(tuple_2(k(kas,B,na(host(B))),host(kas)),kbs)),c(tuple_3(host(kas),host(B),na(host(B)))) -> c(encrypt(secretB,k(kas,B,na(host(B)))))
   81(7) : c(encrypt(secretB,k(kas,kbs,na(host(kbs)))))



Total time: 532445 milliseconds

Number of forward inferences: 39
Number of tableau inferences: 0
Number of generated clauses: 83
Number of kept clauses: 48
yes

*/