Proving Correctness of the Basic TESLA Multicast Stream Authentication Protocol with TAME
Myla M. Archer · 2002
... 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