%A A. Lomuscio
%A F. Raimondi
%A B. Wozna
%C Wandlitz, Germany
%T Verification of the TESLA protocol in MCMAS-X
%L discovery5624
%D 2006
%I Humboldt University Press
%P 255-267
%X We present MCMAS-X, an extension of the OBDD-based model
checker MCMAS for multi-agent systems, to explicit and deductive knowledge. We use MCMAS-X to verify authentication properties in the TESLA secure stream protocol.
%E G. Lindemann
%E H. Schlingloff
%B Proceedings of Concurrency, Specification and Programming (CS&P) 2006