Verification of the TESLA protocol in MCMAS-X

Issue title: Special Issue on Concurrency Specification and Programming (CS&P)

Article type: Research Article

Authors: Lomuscio, Alessio | Raimondi, Franco | Woźna, Bożena

Affiliations: Department of Computing, Imperial College London, 180 Queen's Gate, London SW7 2AZ, UK. E-mail: A.Lomuscio@imperial.ac.uk | Department of Computer Science, University College London, Gower Street, London WC1E 6BT, UK. E-mail: f.raimondi@cs.ucl.ac.uk | Institute of Mathematics and Computer Science, Jan Długosz University Al. Armii Krajowej 13/15, 42-200 Cz�stochowa, Poland. E-mail: b.wozna@ajd.czest.pl

Abstract: We use MCMAS-X to verify authentication properties in the TESLA secure stream protocol. MCMAS-Xis an extension to explicit and deductive knowledge of the OBDD-based model checker MCMAS a verification tool for multi-agent systems.

Journal: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 473-486, 2007