% Needham-Schroeder 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(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 ****').
 
%
% Intruder Theory 

rule([fresh(Y)], 
     [fresh(X),mem(nonce(N))], 
     {X>N,N>Y}, intrudernewnonce).

rule([enc(pk(0),tuple(M))], 
     [mem(M)], 
     {}, intruderreceiveamsg_1).

rule([enc(pk(0),tuple(M,N))], 
     [mem(M),mem(N)], 
     {}, intruderreceivemsg2).

rule([enc(pk(0),tuple(M,N,P))], 
     [mem(M),mem(N),mem(P)], 
     {}, intruderreceivemsg_3).

rule([enc(A,T)], 
     [enc(A,T),enc(A,T)], 
     {}, duplicatemsg_3).
     
rule([enc(A,T)], 
     [], 
     {}, removemsg_3).

rule([mem(N)], 
     [mem(N),
      enc(pk(B),tuple(N))], 
     {B>0}, intrudercreatemsg_1).

rule([mem(M),mem(N)], 
     [mem(M),mem(N),
      enc(pk(B),tuple(M,N))], 
     {B>0}, intrudercreatemsg_2).
     
rule([mem(M),mem(N),mem(Z)], 
     [mem(M),mem(N),mem(Z),
      enc(pk(B),tuple(M,N,Z))], 
     {B>0}, intrudercreatemsg_3).

rule([mem(M)], 
     [mem(M),mem(M)], 
     {}, intruderduplicateknowledge).
   

% 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).

%
% 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),pk(B)))
     ], 
      {A>=0,B>0,Y>NB,NB>X}, second).


%
% 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),pk(B)))
     ], 
     [step3(pk(A),tuple(nonce(NA),nonce(NB),pk(B))), 
      enc(pk(B),tuple(nonce(NB)))
     ], 
     {A>0,B>=0}, 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).


% 
% 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:
% 

secunsafe([ 
  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(_)], {}),
inv([fresh(B),mem(nonce(A))],  {A>=B}),
inv([fresh(X)],                {X=<0}),
inv([fresh(B1),enc(pk(_),tuple(_,nonce(A1),_))],  {A1>=B1}),
inv([fresh(B2),enc(pk(_),tuple(nonce(A2),_,_))],  {A2>=B2}),
inv([fresh(B5),enc(pk(_),tuple(_,_,nonce(A5)))],  {A5>=B5}),
inv([fresh(B3),enc(pk(_),tuple(nonce(A3),_))],    {A3>=B3}),
inv([fresh(B6),enc(pk(_),tuple(_,nonce(A6)))],    {A6>=B6}),
inv([fresh(B4),enc(pk(_),tuple(nonce(A4)))],      {A4>=B4}),
inv([fresh(B7),step2(pk(_),tuple(nonce(_),nonce(A7),pk(_)))],  {A7>=B7})
]).