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

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

init(K,L):-
  f(K,[init],CM,L,_,_).
  
%
% 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)),par(_,_)],
     {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(s,id(B),sk(K),ts(T),ts(T))))],
      {A>B,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(s,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).

%
% 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(X,Y,M)], 
%     [from(X,Y,M),from(X,Y,M)], 
%     {}, duplicatemsg_3).
     
rule([from(_,_,enc(_,_))], 
     [], 
     {}, removemsg_3).


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

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})
]).

a_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})
]).

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

unicity_unsafe([
  unsafe([resp(id(_),tuple(id(_),sk(K),ts(_),ts(_))),
          resp(id(_),tuple(id(_),sk(K),ts(_),ts(_)))],
          {K>=0})
]).

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


distinct_unsafe([
  unsafe([resp(id(A),tuple(id(_),sk(K),ts(_),ts(_))),
          resp(id(B),tuple(id(_),sk(K),ts(_),ts(_)))],
          {A>B,K>=0})
]).


sec_unsafe([ 
  unsafe([resp(id(B),tuple(id(A),sk(K),ts(Now),ts(Start))),
          mem(sk(K))],{A>0,B>0})
  
]).

sec_init_unsafe([ 
  unsafe([init(id(A),tuple(id(B),sk(K),ts(T))),
          mem(sk(K))],{A>0,B>0})
  
]).

secr_unsafe([ 
  unsafe([init(id(A),tuple(id(B),sk(K),ts(T))),
          resp(id(B),tuple(id(A),sk(K),ts(Now),ts(Start))),
          mem(sk(K))],{})
  
])