7th European Symposium on Research in Computer Security (ESORICS 2002)
Analysing a Stream Authentication Protocol using Model Checking
Philippa Broadfoot, Gavin Lowe
Keywords :
Abstract : In this paper, we consider how one can analyse a stream authentication protocol using model checking techniques. In particular, we focus on the Timed Efficient Stream Loss-tolerant Authentication Protocol, TESLA. This protocol differs from the standard class of authentication protocols previously analysed using model checking techniques in the following interesting way: an unbounded stream of messages is broadcast by a sender, making use of an unbounded stream of keys; the authentication of the n-th message in the stream is achieved on receipt of the n+1-th message. We show that, despite the infinite nature of the protocol, it is possible to build a finite model that correctly captures its behaviour.
(Pages 146-161)