% Needham-Schroeder Secret Key 
%
%  A --> B : {sk(Kab)}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(pk(A),tuple(pk(B),key(Kab))),enc(sk(B),tuple(pk(A),key(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(key(Kab))], 
     [step1(pk(A),tuple(pk(B),key(Kab))),enc(sk(B),tuple(pk(A),key(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(pk(A),tuple(pk(0),key(Kab))),mem(key(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(sk(B),tuple(pk(A),key(Kab)))], 
     [fresh(Y),step2(pk(B),tuple(pk(A),key(Kab),nonce(Secret))),enc(key(Kab),tuple(nonce(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(sk(B))], 
     [fresh(Y),step2(pk(B),tuple(pk(A),key(Kab),nonce(Secret))),mem(sk(B)),mem(key(Kab)),mem(nonce(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(key(Kab)),mem(sk(B))], 
     [fresh(Y),step2(pk(B),tuple(pk(A),key(Kab),nonce(Secret))),mem(sk(B)),mem(key(Kab)),mem(nonce(Secret))], 
      {A>=0,B>0,Y>Secret,Secret>X},
      trudy_starts_a_session_using_a_compromise_key).


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


rule([fresh(X),   enc(sk(B),tuple(pk(A),key(Kab))),              mem(key(Kab))], 
     [fresh(Y), step2(pk(B),tuple(pk(A),key(Kab),nonce(Secret))),
                  enc(key(Kab),tuple(nonce(Secret))),            mem(key(Kab)),mem(nonce(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(sk(B),tuple(pk(A),key(Kab))),              mem(key(Kab))], 
     [fresh(Y), step2(pk(B),tuple(pk(A),key(Kab),nonce(Secret))),
                                              mem(key(Kab)),mem(nonce(Secret))], 
      {A>0,B>0,Y>Secret,Secret>X}, 
     trudy_knows_the_secret_and_impersonates_Alice).
%
% Alice receives the secret
%

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

%
% Alice receives the secret from Trudy
%

rule([step1(pk(A),tuple(pk(B),key(Kab))),              mem(nonce(Secret)),mem(key(Kab))], 
     [step3(pk(A),tuple(pk(B),key(Kab),nonce(Secret))),mem(nonce(Secret)),mem(key(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: A and B believes they exhanged a "secret key" or a "secret"
% but Trudy got hold of it

unsafe([ 
  unsafe([step2(pk(B),tuple(pk(A),key(Kab),nonce(Secret))),mem(nonce(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(nonce(A))],  {A>B}),
inv([mem(nonce(X))], {X<0}),
inv([enc(pk(F),_)], {F=<0}),
inv([enc(sk(F1),_)], {F1=<0}),
inv([enc(pk(G),_),fresh(H)], {G>H}),
inv([enc(key(R),_),fresh(S)], {R>S})
])