• http://www.ietf.org/rfc/rfc4082.txt [RFC4082]
• http://www.ece.cmu.edu/ adrian/tesla.html

 0. S -> R: {N.K_0}inv(k_S)         
 i. S -> R: M_i.hash(K_i,M_i).K_i-1 

Note that the last message M_N cannot be authenticated because the corresponding key K_N is never revealed.

• Real-time issues including initial synchronisation (may be critical)
• Delay other than 1 (should not make a difference wrt security here)
• Any number of packets per interval (should not be critical)
• Multiple receivers (no problem, since receivers are independent of each other)

The count of rounds, N should be a parameter, but is hard-wired to be 3 here.

The current model assumes that the sender sends messages one per time interval and the receiver receives these messages one per time interval - with the possibility of gaps, i.e. he may miss a message. The current model does not include the possibility of messages being delayed, i.e. being received in a later time interval.

• strong authentication on sender_msgstream

A variant with lazy generation of one-way chains is commented out.

We send artificial time ticks to keep the Sender synchronised with the Receiver.

Since protocol_ids are used in the goals section and the third argument of witness and request must be atomic, we use the single constant sender_msgstream to identify the whole message stream rather than individual messages. Yet the check for authentication is fine since the matching of witness and request also takes the fourth argument of witness and request into account.  

role sender(S: agent,
            SND, RCV: channel(dy), 
            F: hash_func,
            K_S: public_key)
played_by S def=

  local State: nat,
        Time, N: message, % current time and final time, should be: text,
        K_prev, K: message, % should be: symmetric_key,
        M: text

  const k_N: symmetric_key

  init State := 0

  transition

  0. State  = 0 /\ RCV(start) =|>
     State':= 1 /\ Time':= t_0 /\ N':= tick(tick(tick(t_0))) % 3 rounds
                /\ K_prev':= F(F(F(k_N)))                    % 3 rounds
%               /\ K_prev' = K_prev' =|>  % lazy generation of one-way chain!
                /\ SND({tick(N').F(K_prev')}_inv(K_S)) % send tick(N') instead
    % of N' to prevent the intruder from replaying N' before receiver sends N'

  1. State  = 1 /\ RCV(Time) % keeps the sender synchronised with the receiver
%t_0 and tick must not be known to the intruder in order to be used as a signal 
%that can only be generated by the receiver
                /\ K_prev = F(K') /\ Time /= N =|> 
     State':= 1 /\ M' := new() /\ SND(M'.hash_(K',M').F(K')) 
                /\ K_prev' := K'
                /\ Time' := tick(Time)
                /\ witness(S,S,sender_msgstream,M') %msgstream should be: tick(Time)

%this transition is not really necessary; it just closes the lazy one-way chain.
% 2. State  = 1 /\ RCV(Time) /\ Time = N /\ K_prev = k_N =|> 
%    State' = 2 

end role



role receiver(R, S: agent,
              SYNC, RCV: channel(dy),
              F: hash_func,
              K_S: public_key)
played_by R def=

  local State: nat,
        Time, N: message, % should be: text,
        T_prev:  message, % time when M_prev was sent, should be: text,
        K_prev_prev, K_prev, K_prev2: message, % should be: symmetric_key,
        M_prev, M1: message,
        Hash_prev, Hash: message, % should be: text
        Compare: bool,
        Gap,Gap2: message % should be: nat

  const true, false: bool,
        zero: nat,
        succ: nat -> nat,
        buffered, compared_and_buffered: protocol_id % signals just for tracing
           
  init State := 3

  transition

   initialise. 
     State  = 3 /\ RCV({tick(N').K_prev_prev'}_inv(K_S)) =|> 
     State':= 4 /\ Compare':= false /\ Gap':= zero
                /\ Time':= t_0 /\ SYNC(Time')

   arrive.
     State  = 4 /\ Time /= N 
                /\ RCV(M1'.Hash'.K_prev') =|> 
     State':= 5 /\ K_prev2':= K_prev' /\ Gap2':= zero

   adjust_K_prev2. 
                   RCV(start) /\ 
     State  = 5 /\ Gap2 /= Gap =|> 
     State':= 5 /\ K_prev2':= F(K_prev2) /\ Gap2':= succ(Gap2)

   buffer.
                   RCV(start) /\ 
     State  = 5 /\ Compare = false /\ Gap2 = Gap
                /\ K_prev_prev = F(K_prev2) =|> 
     State':= 4 /\ K_prev_prev':= K_prev
                /\ M_prev':= M1 /\ Hash_prev':= Hash
                /\ T_prev':= tick(Time)
                /\ Compare':= true /\ Gap':= zero
                /\ Time':= tick(Time) /\ SYNC(Time'.buffered)

   compare_and_buffer.
                   RCV(start) /\ 
     State  = 5 /\ Compare = true /\ Gap2 = Gap
                /\ Hash_prev = hash_(K_prev2,M_prev) % check previous message
                /\ K_prev_prev = F(K_prev2) =|> 
     State':= 4 /\ K_prev_prev':= K_prev
                /\ M_prev':= M1 /\ Hash_prev':= Hash 
                /\ T_prev':= tick(Time)
                /\ Compare':= true /\ Gap':= zero
                /\ Time':= tick(Time) /\ SYNC(Time'.compared_and_buffered) 
                /\ request(S,S,sender_msgstream,M_prev) %msgstream should: be T_prev

   lose.
     State  = 4 /\ Time /= N 
                /\ RCV(loss) =|> 
     State':= 4 /\ Gap':= succ(Gap)
                /\ Time':= tick(Time) /\ SYNC(Time') 

end role



role session(S,R: agent,
             SR, SYNC: channel (dy), 
             F: hash_func,
             K_S: public_key)
def=
  composition
           sender  (S,    SR, SYNC, F, K_S)
       /\  receiver(R, S, SYNC, SR, F, K_S)
end role



role environment() def=

  const s,r: agent,
        sr,ir,sync: channel (dy),
        hash_: hash_func,
        f: hash_func,
        k_S: public_key,
        tick: text -> text,
        t_0: text,
        loss: text,
        sender_msgstream: protocol_id


  intruder_knowledge = {s,r,hash_,loss,f,k_S}

  composition
        session(s,r,sr,sync,f,k_S) 
%    /\ session(i,r,ir,sync,f,k_S) 

end role



goal

  authentication_on sender_msgstream  % addresses G5

end goal



environment()