% Needham-Schroeder-Lowe Public Key 
%
%  A --> B : {Na,A}pk(B)  
%  B --> A : {Na,Nb,B}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(Step,Fact):-
  f(Step,WM,_,Fact,_,_),
  \+(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-Lowe ****'),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(A,tuple(NA,B)),enc(B,tuple(NA,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(A,tuple(NA,0)),mem(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(B,tuple(NA,A))], 
     [fresh(Y),step2(B,tuple(NA,NB,A)),enc(A,tuple(NA,NB,B))], 
      {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:
% Since Trudy knows all public keys she needs not to store pk(B)

rule([fresh(X),enc(B,tuple(NA,0))], 
     [fresh(Y),step2(B,tuple(NA,NB,0)),mem(NA),mem(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(B,tuple(NA,NB,0)),mem(NA),mem(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(NA)], 
     [fresh(Y),step2(B,tuple(NA,NB,0)),mem(NA),mem(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(NA)], 
     [fresh(Y),step2(B,tuple(NA,NB,A)),enc(A,tuple(NA,NB,B))], 
      {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(A,tuple(NA,B)),    enc(A,tuple(NA,NB,B))], 
     [step3(A,tuple(NA,NB,B)), enc(B,tuple(NB))], 
     {A>0,B>0}, third).

%
% third_with_trudy. 
% Honest agent A receives from, and replies to Trudy, and stops
% The received message is enc(A,tuple(NA,NB,0))
% Trudy can forge it from mem(NA),mem(NB)

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

%
% alice_is_cheated.  Honest  A receives from some honest B, replies to Trudy, and stops
% Note that: in the received message there must be 0    

rule([step1(A,tuple(NA,0)),    enc(A,tuple(NA,NB,0))], 
     [step3(A,tuple(NA,NB,0)), mem(NA),mem(NB)], 
     {A>0}, alice_is_cheated).

%
% impersonate_third. Trudy forges a fake B-message enc(A,tuple{NA,NB,B})
% honest A receives from Trudy, replies to B, and stops
% Although Alice checks for Bob's identity, 
% if Trudy knows NA and NB then she can forge the right message
%

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

rule([step2(B,tuple(NA,NB,A)), enc(B,tuple(NB))], 
     [step4(B,tuple(NA,NB,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(B,tuple(NA,NB,A)), mem(NB)], 
     [step4(B,tuple(NA,NB,A)), mem(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(A,tuple(NA,_,B)),mem(NA)], 
	 {A>0,B>0}),
  unsafe([step3(A,tuple(_,NB,B)),mem(NB)], 
	 {A>0,B>0}),
  unsafe([step4(B,tuple(NA,_,A)),mem(NA)], 
	 {A>0,B>0}),
  unsafe([step4(B,tuple(_,NB,A)),mem(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(A)],  {A>B}),
inv([mem(X)], {X<0}),
inv([enc(F,_)], {F=<0})
]).

% 
% 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(R0,_),fresh(S0)], {R0>S0}),
inv([step2(R1,_),fresh(S1)], {R1>S1}),
inv([step3(R2,_),fresh(S2)], {R2>S2}),
inv([step4(R3,_),fresh(S3)], {R3>S3}),

inv([enc(G,_),fresh(H)], {G>H}),
inv([enc(_,tuple(G1,_,_)),fresh(G4)], {G1>G4}),
inv([enc(_,tuple(_,G2,_)),fresh(H1)], {G2>H1}),
inv([enc(_,tuple(_,_,G3)),fresh(H2)], {G3>H2}),
inv([enc(_,tuple(_,G5)),fresh(H3)], {G5>H3}),
inv([enc(_,tuple(G6,_)),fresh(H4)], {G6>H4}),
inv([enc(_,tuple(G8)),fresh(H5)], {G8>H5}),

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})
]).