Analysing a Stream Authentication Protocol Using Model Checking

Abstract. In this paper, we consider how one can analyse a stream authentication protocol using model checking techniques. In particular, we will be focusing 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.

• Type: Conference
• Year: 2002
• Where: ESORICS
• Authors: Philippa J. Broadfoot, Gavin Lowe
• Keywords: ESORICS 2002, Security Privacy, Stream Authentication Protocol, Stream Loss-tolerant Authentication, Unbounded Stream