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


rule([init],[time(T),fresh(K),init(1),resp(2)],{K>=0,T>=0},init).

      
rule([fresh(K1),time(T),init(A),resp(B)], 
     [fresh(K2),resp(B),time(T),init(A,tuple(B,K,T)),enc(sv(A),tuple(B,K,T))],
      {A>0,B>0,T>=0,K2>K,K>K1},
      alice_starts).

rule([time(Now),enc(sv(A),tuple(B,K,T))], 
     [time(Now),enc(sk(B),tuple(A,K,Now))],
      {A>0,B>0,Now>=0,T>=0,Now-1=<T,T=<Now},
      server_forwards).

rule([time(Now),resp(B),enc(sk(B),tuple(A,K,T))], 
     [time(Now),resp(B,tuple(A,K,Now))],
      {A>0,B>0,Now>=0,T>=0,Now-1=<T,T=<Now},
      bob_receives).
      
rule([time(Now)], 
     [time(Next)],
      {Now>=0,Next>Now}, 
      tock).

rule([enc(sk(B),T)], 
     [enc(sv(B),T)],
      {},
      impersonate).  

goal([init(A,tuple(B,K,Sent)),resp(B,tuple(A,K,Rec))],
      {Rec-Sent>2},goal).