Proving Correctness of the Basic TESLA Multicast Stream Authentication Protocol with TAME
Abstract
The TESLA multicast stream authentication protocol is distinguished from other types of cryptographic protocols in both its key management scheme and its use of timing. It takes advantage of the stream being broadcast to periodically commit to and later reveal keys used by a receiver to verify that packets are authentic, and it uses both inductive reasoning and time arithmetic to allow the receiver to determine that an adversary cannot have prior knowledge of a key that has just been revealed. While an informal argument for the correctness of TESLA has been published, no mechanized proof appears to have previously been done for TESLA or any other protocol of the same variety. This paper reports on a mechanized correctness proof of the basic TESLA protocol based on establishing a sequence of invariants for the protocol using the tool TAME, an interface to PVS specialized for proving properties of automata. It discusses the organization and process used in the proof, and the possibilities for reusing these techniques in correctness proofs of similar protocols, starting with more sophisticated versions of TESLA.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 2002
- Accession Number
- ADA464932
Entities
People
- Myla M. Archer
Organizations
- United States Naval Research Laboratory