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

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

chkis:-
 f(_,[init],_,_,_,_).
%
% 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 ****').


rule([init], 
     [is(T)],
     {T>=0}, 
      is).

rule([is(T)], 
     [is(T),
      initS(id(A),tuple(id(B),id(S)))],
      {A<T,B<T,S<T}, 
      isI).

rule([is(T)], 
     [respS(id(A),tuple(id(S))),
      is(T)],
     {A<T,S<T}, 
      isR).

rule([is(T)], 
     [server(id(A)),
      is(T)],
     {A<T}, 
      isS).

rule([is(T)], 
     [fresh(sk(K)),clock(ts(D)),delay(ts(D1),ts(D2))],
     {K>T,D>=0,D1>=0,D2>=0}, 
      isCFD).

rule([clock(ts(Now))], 
     [clock(ts(Next))],
      {Now>=0,Next>Now}, 
      tock).
      
rule([clock(ts(T)),server(id(S)),fresh(sk(K1)),
     initS(id(A),tuple(id(B),id(S)))], 
     
     [clock(ts(T)),server(id(S)),fresh(sk(K2)),
      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))))],      
      {A>0,B>0,T>=0,K1<K,K<K2},
      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))],
      {A>0,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>0,B>0,Now>=0,T>=0,Now-D2=<T,T=<Now,D2>=0},
      bob_receives).


invariants([ 
inv([delay(_,_),delay(_,_)], {}),
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})
]).




unsafe([ 
  unsafe([from(_,_,sup(enc(sk(K,_),_))),
          init(id(Id),tuple(id(Id2),sk(K),ts(T)))],
          {K>=0,T>=0})
  ,
  unsafe([from(_,_,sup(enc(sk(_,K1),_))),
          init(id(Id1),tuple(id(Id21),sk(K1),ts(T1)))],
          {K1>=0,T1>=0})
]).

ok_unsafe([ 
  unsafe([from(_,_,sup(enc(sk(_,_),sup(enc(sk(_,_),_)))))],
          {})
]).