PROTOCOL:
TESLA: Timed Efficient Stream Loss-tolerant Authentication

PURPOSE:

Secure source authentication mechanism for multicast or broadcast data streams  

REFERENCE:

 

MODELER:
David von Oheimb, Siemens CT IC 3, August 2004
 

ALICE_BOB:

S chooses N (the number of messages to broadcast) and a random symmetric key K_N.
 0. S -> R: {N.K_0}inv(k_S)         
 i. S -> R: M_i.hash(K_i,M_i).K_i-1 
where
F is a one-way function
K_0 = F^N(K_N) is the N-th power of F on K_N
K_i = F^i(K_N) is the i-th power of F on K_N

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

 

LIMITATIONS:

Issues abstracted from:

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.

 

PROBLEMS:
1
 

CLASSIFICATION:
G5
 

ATTACKS:
None

 

NOTES:

Since function exponentiation F^N(X) (N-times repeated application of F on X), is not directly expressible, we have to model this via loops.

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.  



HLPSL:

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()