% Wide Mouth Frog  
%: Too many arguments.
%
%  A --> S : {Ts1,B,Kab}sk(AS)
%  S --> B : {Ts2,A,Kab}sk(BS)
%
%  Property: A and B exchange a "secret" key Kab.

% 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):-false.
% This forces the checker to always look for a fixpoint

chkinit(K,L):-
  f(K,WM,CM,L,_,_),
  \+(member(init(_,_),WM)),
  \+(member(initS1(_,_),WM)), 
  \+(member(resp(_,_),WM)),
  \+(member(mem(_),WM)),
  \+(member(from(_,_,_),WM)),
  nl.

%
% Predicate for searching attack traces (in backtracking).
%

trace(K,L):-
 unsafe(U),
 write('**** Protocol: Wide Mouth Frog ****'),nl,
 write('**** Unsafe States ****'),nl,
 portray_clause(U),nl,
 write('**** Potential Attacks ****'),nl,
 init(K,L),
 tracer(K,L),
 write('**** End Potential Attack ****').
 
% Initialization 
 

% Time 
   
rule([clock(ts(Now))], 
     [clock(ts(Next))],
      {Now>=0,Next>Now}, 
      tock).

% Core protocol 
    
rule([fresh(sk(K1)),clock(ts(T)),
     initS(id(A),tuple(id(B)))],      
     [fresh(sk(K2)),clock(ts(T)),
      initS1(id(A),tuple(id(B),sk(K),ts(T)))
     ],      
     {A>0,B>0,K1<K,K<K2},
      alice_create_key).      
  
rule([clock(ts(T)),server(id(S)),
     initS1(id(A),tuple(id(B),sk(K),ts(T)))],      
     [clock(ts(T)),server(id(S)),
     init(id(A),  tuple(id(B),sk(K),ts(T))),
      from(id(A),id(S),enc(sk(A,S),tuple(r,id(B),sk(K),ts(T),ts(T))))],      
      {S>A,A>B,B>0,T>=0},
      alice_starts).
            

rule([clock(ts(Now)),
      server(id(S)),
      from(id(A),id(S),enc(sk(A,S),tuple(r,id(B),sk(K),ts(T),ts(T1)))),
      delay(ts(D1),ts(D2))], 
      
     [clock(ts(Now)),
      server(id(S)),
      from(id(S),id(B),enc(sk(B,S),tuple(s,id(A),sk(K),ts(Now),ts(T1)))),
      delay(ts(D1),ts(D2))],
      {S>A,A>B,B>0,Now>=0,T>=0,Now-D1=<T,T=<Now,D1>=0},
      server_forwards).


rule([clock(ts(Now)),server(id(S)),respS(id(B),tuple(id(S))),
      from(id(S),id(B),enc(sk(B,S),tuple(s,id(A),sk(K),ts(T),ts(T1)))),
      delay(ts(D1),ts(D2))], 
      
     [clock(ts(Now)),
      server(id(S)),
      resp(id(B),tuple(id(A),sk(K),ts(Now),ts(T1))),
      delay(ts(D1),ts(D2))],
      
      {A>B,B>0,Now>=0,T>=0,Now-D2=<T,T=<Now,D2>=0},
      bob_receives).

%
% Intruder Theory 

rule([from(X,Y,M)], 
     [from(Y,X,M)],
      {},
      impersonate).  

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

rule([], 
     [mem(ts(T))], 
     {T>=0}, intrudernewts).

rule([mem(enc(sk(0,_),tuple(M,id(N),sk(P),ts(Q),ts(R))))], 
     [mem(tuple(M,id(N),sk(P),ts(Q),ts(R)))], 
     {}, intruderreceiveamsg_1).

rule([mem(tuple(M,id(N),sk(P),ts(Q),ts(R)))],
     [mem(enc(sk(0,_),tuple(M,id(N),sk(P),ts(Q),ts(R))))],  
     {}, intruderreceiveamsg_1).

rest_rule([mem(enc(sk(0,_),M))], 
     [mem(M)], 
     {}, intruderreceiveamsg_1).

rest:rule([mem(M)],
     [mem(enc(sk(0,_),M))],  
     {}, intruderreceiveamsg_1).
     
rule([mem(id(N)),mem(sk(P)),mem(ts(Q)),mem(ts(R))], 
     [mem(tuple(M,id(N),sk(P),ts(Q),ts(R)))], 
     {}, intruderreceiveamsg_1).

rule([mem(tuple(M,id(N),sk(Z),ts(Q),ts(R)))],
     [mem(id(N)),mem(sk(Z)),mem(ts(Q)),mem(ts(R))],  
     {}, intrudercreatemsg_3).

rule([from(X,Y,M)],
     [from(X,Y,M),mem(M)], 
     {}, intercept).
     
rule([mem(M)],
     [from(X,Y,M)], 
     {}, forge).
       
     
rule([from(_,_,enc(_,_))], 
     [], 
     {}, removemsg_3).


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

invariants([ 
inv([delay(_,_),delay(_,_)], {}),
inv([par(_,_,_),par(_,_,_)], {}),
inv([is(_),is(_)], {}),
inv([clock(_),clock(_)], {}),
inv([fresh(_),fresh(_)], {}),
inv([fresh(sk(X))],                {X=<0}),
inv([clock(ts(X1))],                {X1<0}),
inv([mem(sup(sk(X2))),fresh(sk(K2))],     {K2=<X2}),
inv([from(_,_,sup(sk(X3))),fresh(sk(K3))],     {K3=<X3}),
inv([init(_,sup(sk(X4))),fresh(sk(K4))],     {K4=<X4}),
inv([resp(_,sup(sk(X5))),fresh(sk(K5))],     {K5=<X5})
]).

%
% Properties: you have to turn the selected seed into a 
% unsafe predicate before loading this module
% The reason is that the checker searches for seeds stored in the list 
%
% unsafe([ unsafe(M1,C1),....,unsafe(Mn,Cn) ]).
%
% E.g. to search for traces leading to a responder state
% wioth no time constraints
% Replace g_unsafe(...) - see some lines below- with unsafe(...)
% 
% The current selected seed is the following one: 
%

% auth_unsafe 
%
% Terminates in 7 steps, 80.2s
% 1 initial state (22), all paths from 22 go through 11: 
% 22(4): [fresh(sk(A)),clock(ts(B)),initS(id(C),tuple(id(D))),
% 	  server(id(E)),delay(ts(F),ts(G)),respS(id(D),tuple(id(E))),
% 	  par(id(D),id(C),sk(H))], {C>0.0,D>0.0,H-A>0.0,B>=0.0,F>=0.0,G>=0.0},
%
% 11(3): [clock(ts(A)),server(id(B)),initS1(id(C),tuple(id(D),sk(E),ts(A))),
% 	  delay(ts(F),ts(G)),respS(id(D),tuple(id(B))),par(id(D),id(C),sk(E))], 
%       {C>0.0,D>0.0,A>=0.0,F>=0.0,G>=0.0}, 11, 4, alice_starts).
%
% 11 contains: initS1(id(C),tuple(id(D),sk(E),ts(A))),par(id(D),id(C),sk(E))
%

unsafe([
  unsafe([ resp(id(Id1),tuple(id(Id2),sk(K),ts(Now),ts(Start))),
           delay(ts(D1),ts(D2)),par(id(Id1),id(Id2),sk(K))],
           {Start=<Now,Now=<Start+D1+D2,D1>=0,D2>=0,Start>=0})
]).

%generic_auth_unsafe 
%
% Terminates in 6 steps, 24.2s
% 1 initial state (18), all paths from 18 go through 11: 
% 11 contains: initS1(id(C),tuple(id(D),sk(E),ts(A))),par(id(D),id(C),sk(E))
%
% 
g_unsafe([ 
  unsafe([resp(id(Id1),tuple(id(Id2),sk(K),ts(Now),ts(Start))),
  delay(ts(D1),ts(D2)),par(id(Id1),id(Id2),sk(K))],
  {D1>=0,D2>=0,Start>=0,Now>=0})
]).

%timed_auth_unsafe 
%generic_auth_unsafe 
%
% Terminates in 7 steps, 41.2s
% no initial states
%

t_unsafe([
  unsafe([resp(id(B),tuple(id(A),sk(K),ts(Now),ts(Start))),
 	  delay(ts(D1),ts(D2)),
 	  par(sk(A),sk(B),sk(K))],
  	  {Now>Start+D1+D2,D1>=0,D2>=0,Start>=0})
]).

% Terminates in 11 steps, 3093.7s
% Detect 1 initial state: 335(7)
% Error trace: 
% alice_create_key, alice_starts, server_forwards, intercept, 
% bob_receives, forge, bob_receives
%


%uniqueness 
ru_unsafe([ 
  unsafe([resp(_,sup(sk(K))),
          resp(_,sup(sk(K)))],
          {K>=0})
]).

%uniqueness 
un_unsafe([ 
  unsafe([initS1(_,sup(sk(K))),
          initS1(_,sup(sk(K)))
         ],
          {K>=0})
]).

%uniqueness 
dru_unsafe([ 
  unsafe([resp(id(A),sup(sk(K))),
          resp(id(B),sup(sk(K)))],
          {A>B,K>=0})
]).