% Needham-Schroeder Public Key 
%
%  A --> B : {Na,A}pk(B)  
%  B --> A : {Na,Nb}pk(A)
%
%  Property: A and B exchange two "fresh" and "secret" nonces.

% Initial assumptions
%
%  Agents' identifier are integers: Trudy =0, honest A >0
%  All agents (and Trudy) know all public keys
%  Trudy = the network
%  She can store everything in her memory (using the predicate mem) 
%  but the messages encrypted with the public keys of honest agents 
%  Trudy does not know the private keys of honest agents
%  Messages are represented as enc(Key,tuple(.,...,.)) 
%  Nonces are represented as integer values and controlled via the global memory fresh(.)
%  In every state there must be only one copy of fresh(.); it keeps the next unused name
%

% Potential initial states
%
%  All states in which an agent is already in an intermediate step of the protocol
%  or in which there is already a pending message enc(.,.)
%
%

init(K,L):-
  f(K,WM,_,L,_,_),
  \+(member(step1(_,_),WM)),
  \+(member(step2(_,_),WM)),
  \+(member(step3(_,_),WM)),
  \+(member(step4(_,_),WM)),
  \+(member(enc(_,_),WM)),
  nl.

%
% Preducate to use for searching attack traces (in backtracking).
%

trace(K,L):-
 unsafe(U),
 write('**** Protocol: Needham-Schroeder ****'),nl,
 write('**** Unsafe States ****'),nl,
 portray_clause(U),nl,
 write('**** Potential Attacks ****'),nl,
 init(K,L),
 tracer(K,L),
 write('**** End Potential Attack ****').
 
%
% first. First protocol rule: 
% Honest A starts a session with honest B (both chosen non-deterministically):
% a message enc(B,.) is sent on the network (=Trudy)
% Freshness is ensured via the constraints on the nonces and the fresh(.) memory
%

rule([fresh(X)], 
     [fresh(Y),step1(pk(A),tuple(nonce(NA),pk(B))),enc(pk(B),tuple(nonce(NA),pk(A)))],
      {A>0,B>0,Y>NA,NA>X}, first).

%
% intercept_first. First protocol rule : intercepted
% Honest A starts a session with Trudy:
% Trudy immediately learns the nonce sent by A (she already knows A's public key)
% Freshness is ensured via the constraints on the nonces and the fresh(.) memory
%

rule([fresh(X)], 
     [fresh(Y),step1(pk(A),tuple(nonce(NA),pk(0))),mem(nonce(NA))],
      {A>0,Y>NA,NA>X}, intercept_first).

%
% second. Second protocol rule 
% Honest B receives from, and replies to A:
%


rule([fresh(X),enc(pk(B),tuple(nonce(NA),pk(A)))], 
     [fresh(Y),step2(pk(B),tuple(nonce(NA),nonce(NB),pk(A))),enc(pk(A),tuple(nonce(NA),nonce(NB)))], 
      {A>0,B>0,Y>NB,NB>X}, second).

%
% impersonate_second. Second protocol rule: Trudy impersonate A 
% Honest B receives from some honest B, but replies to Trudy:
%

rule([fresh(X),enc(pk(B),tuple(nonce(NA),pk(0)))], 
     [fresh(Y),step2(pk(B),tuple(nonce(NA),nonce(NB),pk(0))),mem(nonce(NA)),mem(nonce(NB))], 
      {B>0,Y>NB,NB>X}, impersonate_second).

%
% trudy_starts.  Trudy starts a session with B
% honest B receives from, and replies to Trudy who has 
% forged the A-message  enc(B,tuple(NA,0)) with a fresh nonce NA
%

rule([fresh(X)], 
     [fresh(Y),step2(pk(B),tuple(nonce(NA),nonce(NB),pk(0))),mem(nonce(NA)),mem(nonce(NB))], 
      {B>0,Y>NB,NB>NA,NA>X}, trudy_starts).

%
% trudy_cheats. Trudy starts a session with B
% honest B receives from, and replies to Trudy who has 
% forged a fake A-message  enc(B,tuple(NA,0)) using an old nonce NA
%

rule([fresh(X),mem(nonce(NA))], 
     [fresh(Y),step2(pk(B),tuple(nonce(NA),nonce(NB),pk(0))),mem(nonce(NA)),mem(nonce(NB))], 
      {B>0,Y>NB,NB>X}, trudy_cheats).

%
% trudy_cheats_and_impersonate. Trudy starts a session with B
% Honest B receives from, and replies to Trudy who has 
% forged a fake A-message  enc(B,tuple(NA,A)) using an old nonce NA
% and honest A's public key
%

rule([fresh(X),mem(nonce(NA))], 
     [fresh(Y),step2(pk(B),tuple(nonce(NA),nonce(NB),pk(A))),enc(pk(A),tuple(nonce(NA),nonce(NB)))], 
      {A>0,B>0,Y>NB,NB>X}, trudy_cheats_and_impersonate).

%
% third. Third protocol rule 
% Honest A receives from, and replies to B
%


rule([step1(pk(A),tuple(nonce(NA),pk(B))),    enc(pk(A),tuple(nonce(NA),nonce(NB)))], 
     [step3(pk(A),tuple(nonce(NA),nonce(NB),pk(B))), enc(pk(B),tuple(nonce(NB)))], 
     {A>0,B>0}, third).

%
% third_with_trudy. 
% Honest agent A receives from, and replies to Trudy, and stops
%

rule([step1(pk(A),tuple(nonce(NA),pk(0))),    mem(nonce(NA)),mem(nonce(NB))], 
     [step3(pk(A),tuple(nonce(NA),nonce(NB),pk(0))), mem(nonce(NA)),mem(nonce(NB))], 
     {A>0}, third_with_trudy).

%
% alice_is_cheated.  Honest  A receives from some honest B, replies to Trudy, and stops
%
     
rule([step1(pk(A),tuple(nonce(NA),pk(0))), enc(pk(A),tuple(nonce(NA),nonce(NB)))], 
     [step3(pk(A),tuple(nonce(NA),nonce(NB),pk(0))), mem(nonce(NA)),mem(nonce(NB))], 
     {A>0}, alice_is_cheated).

%
% impersonate_third. Trudy forges a fake B-message enc(B,tuple{NA,NB})
% honest A receives from Trudy, replies to B, and stops
%

rule([step1(pk(A), tuple(nonce(NA),pk(B))),    mem(nonce(NA)),mem(nonce(NB))], 
     [step3(pk(A), tuple(nonce(NA),nonce(NB),pk(B))), enc(pk(B),tuple(nonce(NB))),mem(nonce(NA)),mem(nonce(NB))], 
     {A>0,B>0}, impersonate_third).
     
%
% fourth. Fourth rule: Honest B receives (from A>=0) and stops
%    

rule([step2(pk(B),tuple(nonce(NA),nonce(NB),pk(A))), enc(pk(B),tuple(nonce(NB)))], 
     [step4(pk(B),tuple(nonce(NA),nonce(NB),pk(A)))], 
     {A>=0,B>0}, fourth).

%
% fourth_rule_with_trudy. Trudy forges a fake B-message enc(B,tuple{NB})
% ingenue  B receives from Trudy and stops
%

rule([step2(pk(B),tuple(nonce(NA),nonce(NB),pk(A))), mem(nonce(NB))], 
     [step4(pk(B),tuple(nonce(NA),nonce(NB),pk(A))), mem(nonce(NB))],
     {B>0}, fourth_rule_with_trudy).

% 
% Seed of backward exploration: 
% The states in the "unsafe([unsafe(M1,C1),....,unsafe(Mk,Ck)])" list represents the "disjunction"
% M1:C1 or ... or Mk:Ck (their denotation is the union of the upward closure of the instances
% of every constrained configuration Mi:Ci
% This formula represents "violations" to a given Safety Property, e.g., Secrecy.
%
% In Needham-Schroeder we want to prove "the secrecy of the nonces Na,Nb"
% It is not possible that honest A stops successfully after talking to honest A', 
% and Trudy got to know one of the nonces
%
% Thus, the possible violations are:
% 

unsafe([ 
  unsafe([step3(pk(A),tuple(nonce(NA),nonce(_),pk(B))),mem(nonce(NA))], 
	 {A>0,B>0}),
  unsafe([step3(pk(A),tuple(nonce(_),nonce(NB),pk(B))),mem(nonce(NB))], 
	 {A>0,B>0}),
  unsafe([step4(pk(B),tuple(nonce(NA),nonce(_),pk(A))),mem(nonce(NA))], 
	 {A>0,B>0}),
  unsafe([step4(pk(B),tuple(nonce(_),nonce(NB),pk(A))),mem(nonce(NB))], 
	 {A>0,B>0})	
]).


%     
%
% Pruning with complement of invariant properties
% 
% All states subsumed by some constrained configuration M:C stored as inv(M,C)
% are removed during the symbolic backward exploration
% 
% Thus inv(M,C) denotes a "violation" of an invariant that must hold in any 
% protocol execution. This is useful, e.g., to anticipate the freshness requirement
% Eg. inv([fresh(B),mem(A)],  {A>B}) means that the intruder only knows "used" names
% (clearly, the nonces generated by Trudy are themselves "used" onces).
% Invariants may dramatically accelerate the search. However, if not used in 
% adequate way, they might render the analysis "incomplete". 
% 
% Here are invariants we can infer automatically from the initial state and the rules
% (adding them propagates information coming from the initial states into 
% the backward search)
%
% Important: 
% To work properly, it is necessary to use distinct variables in each inv(.,.) item,
% this is  due to implementation details that we will correct soon
%

invariants([ 
inv([fresh(_),fresh(_)], {}),
%
% this is a delicate one: we enforce a global sequentialization between different sessions
% it is ok only if the protocol semantics is preserved
%
% inv([enc(_,_),enc(_,_)], {}), 
%
inv([fresh(X)],      {X=<0}),
inv([fresh(B),mem(nonce(A))],  {A>B}),
inv([step1(pk(R0),_),fresh(S0)], {R0>S0}),
inv([step2(pk(R1),_),fresh(S1)], {R1>S1}),
inv([step3(pk(R2),_),fresh(S2)], {R2>S2}),
inv([step4(pk(R3),_),fresh(S3)], {R3>S3}),
inv([mem(nonce(X))], {X<0}),
inv([enc(pk(F),_)], {F=<0}),
inv([enc(pk(G),_),fresh(H)], {G>H}),
inv([enc(_,tuple(nonce(G1),_)),fresh(G4)], {G1>G4}),
inv([enc(_,tuple(_,nonce(G2))),fresh(G6)], {G2>G6}),
inv([enc(_,tuple(nonce(G3),_)),fresh(G5)], {G3>G5}),
inv([enc(_,tuple(_,pk(G4))),fresh(G7)], {G4>G7})
]).

% 
% Here are invariants that restrict the search to "interesting" states by 
% eliminating states that are not valid (e.g. in which values are negative)
% To enable them: copy the inv(.,.) item you would like
% to add to the above "invariant" list (remember to use fresh variables)
% 


other_possible_invariants([ 

inv([step1(B,_)],   {B=<0}),
inv([step2(B1,_)], {B1=<0}),
inv([step3(B2,_)], {B2=<0}),
inv([step4(B3,_)], {B3=<0}),

inv([step1(_,tuple(E,_)),  fresh(E1)], {E>E1}),
inv([step2(_,tuple(H,_,_)),fresh(H1)], {H>H1}),
inv([step3(_,tuple(I,_,_)),fresh(I1)], {I>I1}),
inv([step4(_,tuple(J,_,_)),fresh(J1)], {J>J1}),

inv([step2(_,tuple(_,N,_)),fresh(N1)], {N>N1}),
inv([step3(_,tuple(_,O,_)),fresh(O1)], {O>O1}),
inv([step4(_,tuple(_,P,_)),fresh(P1)], {P>P1})
]).