% Needham-Schroeder Secret Key 
%
%  A --> B : {sk(Kab),A}sk(B)  
%  B --> A : {secret}sk(Kab)
%
%  Property: A and B exchange a "secret" key.

% 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(enc(_,_),WM)),
  nl.

%
% Predicate 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. 
% Honest A sends a fresh Key to B encrypted with B's key.
%

rule([fresh(X)], 
     [fresh(Y),step1(A,tuple(B,Kab)),enc(B,tuple(A,Kab))],
     {A>0,B>0,Y>Kab,Kab>X}, 
     first).
%
% Honest A sends a compromised Key to B encrypted with B's key.
%

rule([mem(Kab)], 
     [step1(A,tuple(B,Kab)),enc(B,tuple(A,Kab))],
     {A>0,B>0}, 
     compromised_key).

%
% Honest A starts a session with Trudy 
% A sends a fresh Key to Trudy.
%

rule([fresh(X)], 
     [fresh(Y),step1(A,tuple(0,Kab)),mem(Kab)],
     {A>0,Y>Kab,Kab>X},
     alice_starts_a_session_with_trudy).


%
% Second protocol rule. 
% Bob receives from Alice and sends back a secret 
% The Secret is modeled as a fresh name 
% 

rule([fresh(X),enc(B,tuple(A,Kab))], 
     [fresh(Y),step2(B,tuple(A,Kab,Secret)),enc(Kab,tuple(Secret))], 
      {A>0,B>0,Y>Secret,Secret>X}, 
     second).

%
% If Trudy knows Bob's key 
% Trudy starts a session with Bob
% She can either impersonate Alice or use her identity: A>=0 
% Trudy sends a fresh key

rule([fresh(X),mem(B)], 
     [fresh(Y),step2(B,tuple(A,Kab,Secret)),mem(B),mem(Kab),mem(Secret)], 
      {A>=0,B>0,Y>Kab,Kab>Secret,Secret>X},
      trudy_starts_a_session_with_Bob).

% If Trudy knows Bob's key
% Trudy starts a session with Bob
% She can either impersonate Alice or use her identity: A>=0 
% She sends a compromised key
      
rule([fresh(X),mem(B),mem(Kab)], 
     [fresh(Y),step2(B,tuple(A,Kab,Secret)),mem(B),mem(Kab),mem(Secret)], 
      {A>=0,B>0,Y>Secret,Secret>X},
      trudy_starts_a_session_using_a_compromised_key).

%
% Bob replies to Alice
% The secret key is compromised
% Trudy fowards the message to Alice

rule([fresh(X),enc(B,tuple(A,Kab)),mem(Kab)], 
     [fresh(Y),step2(B,tuple(A,Kab,Secret)),enc(Kab,tuple(Secret)),mem(Kab),mem(Secret)], 
      {A>0,B>0,Y>Secret,Secret>X}, 
     trudy_knows_the_secret).

%
% Bob replies to Alice
% The secret key is compromised
% Trudy eavedropes the message

rule([fresh(X),enc(B,tuple(A,Kab)),mem(Kab)], 
     [fresh(Y),step2(B,tuple(A,Kab,Secret)),mem(Kab),mem(Secret)], 
      {A>0,B>0,Y>Secret,Secret>X}, 
     trudy_knows_the_secret_and_impersonates_Alice).

%
% Alice receives the secret
%

rule([step1(A,tuple(B,Kab)),enc(Kab,tuple(Secret))], 
     [step3(A,tuple(B,Kab,Secret))], 
     {A>0,B>=0}, 
     alice_receives_the_secret).

%
% Alice receives the secret from Trudy
%

rule([step1(A,tuple(B,Kab)),mem(Secret),mem(Kab)], 
     [step3(A,tuple(B,Kab,Secret)),mem(Secret),mem(Kab)], 
     {A>0,B>=0},
     alice_receives_from_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.

%
% Here violations are: B believes she exhanged a "secret" with A
% but Trudy got hold of it

unsafe([ 
  unsafe([step2(B,tuple(A,Kab,Secret)),mem(Secret)],{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([ 
inv([fresh(_),fresh(_)], {}),
inv([fresh(X)],      {X=<0}),
inv([fresh(B),mem(A)],  {A>B}),
inv([enc(F,_)], {F=<0})
]).