Verification of the Tesla protocol in Mcmas-x

• Autorzy: Lomuscio A. , Raimondi F. , Woźna B.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

Tesla protokol; model checking; McMAS-X

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 79, nr 3-4
• Strony: 473--486
• Opis fizyczny: bibliogr. 27 poz., tab., wykr.

Twórcy

autor

Lomuscio A.

autor

Raimondi F.

autor

Woźna B.

• Institute of Mathematics and Computer Science, Jan Długosz University, Armii Krajowej 13/15, 42-200 Częstochowa, Poland,

Bibliografia

• [1] R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. Journal of the ACM, 49(5):672-713, 2002.
• [2] M. Archer. Proving correctness of the basic TESLA multicast stream authentication protocol with TAME. In Proceedings of Workshop on Issues in the Theory of Security, 2002.
• [3] A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.-C. Héam, J. Mantovani, S. Moedersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganò, and L. Vigneron. The Avispa tool for the automated validation of internet security protocols and applications. In CAV 2005, 17th Int. Conf. on Computer Aided Verification, Edinburgh, Scotland, UK, July 2005.
• [4] P. J. Broadfoot and G. Lowe. Analysing a stream authentication protocol using model checking. In Proceedings of the 7th European Symposium on Research in Computer Security (ESORICS'02), pages 146-161. Springer-Verlag, 2002.
• [5] R. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transaction on Computers, 35(8):677-691, 1986.
• [6] M. Burrows,M. Abadi, and R. Needham. A logic of authentication. ACMTransactions on Computer Systems, 8(1):18-36, 1990.
• [7] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999.
• [8] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995.
• [9] P. Gammie and R. van der Meyden. MCK: Model checking the logic of knowledge. In Proceedings of 16th International Conference on Computer Aided Verification (CAV'04), volume 3114 of LNCS, pages 479-483. Springer-Verlag, 2004.
• [10] J. Halpern, R. van der Meyden, and M. Y. Vardi. Complete axiomatisations for reasoning about knowledge and time. SIAM Journal on Computing, 33(3):674-703, 2003.
• [11] J. Y. Halpern and R. Pucella. Modeling Adversaries in a Logic for Security ProtocolAnalysis. In Proceedings of the Workshop on Formal Aspects of Security (FASec'02), volume 2629 of LNCS, pages 115-132. Springer-Verlag, 2002.
• [12] M. Kacprzak, A. Lomuscio, A. Niewiadomski, W. Penczek, F. Raimondi, and M. Szreter. Comparing BDD and SAT based techniques for model checking Chaumś dining cryptographers protocol. Fundamenta Informaticae, 63(2,3):221-240, 2006.
• [13] A. Lomuscio and F. Raimondi. MCMAS: A model checker for multi-agent systems. In H. Hermanns and J. Palsberg, editors, Proceedings of TACAS 2006, Vienna, volume 3920, pages 450-454. Springer Verlag, March 2006.
• [14] A. Lomuscio and M. Sergot. Deontic interpreted systems. Studia Logica, 75(1):63-92, 2003.
• [15] A. Lomuscio and B. Woźna. A combination of explicit and deductive knowledge with branching time: completeness and decidability results. In Matteo Baldoni, Ulle Endriss, Andrea Omicini, and Paolo Torroni, editors, Declarative Agent Languages and Technologies III: Third InternationalWorkshop, DALT 2005, Utrecht, The Netherlands, July 25, 2005, Selected and Revised Papers, volume 3904 of LNAI, pages 188 - 204. Springer Berlin/Heidelberg, 2006.
• [16] A. Lomuscio and B. Woźna. A complete and decidable axiomatisation for deontic interpreted systems. In Proceedings of the 8th International Workshop on Deontic Logic in Computer Science (DEON'06), volume 4048, pages 238 - 254. Springer Berlin / Heidelberg, July 2006.
• [17] A. Lomuscio and B. Woźna. A complete and decidable security-specialised logic and its application to the tesla protocol. In Peter Stone and Gerhard Weiss, editors, Proceedings of the fifth international joint conference on Autonomous agents and multiagent systems (AAMAS'06), pages 145-152, Hakodake, Japan, 2006. ACM Press.
• [18] R. van der Meyden. Axioms for knowledge and time in distributed systems with perfect recall. In Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, pages 448-457, Paris, France, 1994. IEEE Computer Society Press.
• [19] R. van der Meyden and K. Wong. Complete axiomatizations for reasoning about knowledge and branching time. Studia Logica, 75(1):93-123, 2003.
• [20] D. Mills. Network time protocol (version 3) specification, implementation and analysis. Technical Report 1305, RFC, March 1992.
• [21] W. Nabialek, A. Niewiadomski, W. Penczek, A. Pólrola, and M. Szreter. VerICS 2004: A model checker for real time and multi-agent systems. In Proceedings of the InternationalWorkshop on Concurrency, Specification and Programming (CS&P'04), volume 170 of Informatik-Berichte, pages 88-99. Humboldt University, 2004.
• [22] A. Perrig, R. Canetti, J. D. Tygar, and Dawn X. Song. Efficient authentication and signing of multicast streams over lossy channels. In IEEE Symposium on Security and Privacy, pages 56-73,May 2000.
• [23] R. Pucella. Deductive Algorithmic Knowledge. In Proceedings of the 8th International Symposium on Artificial Intelligence and Mathematics (SAIM'04), Online Proceedings: AI&M 22-2004, 2004.
• [24] F. Raimondi and A. Lomuscio. MCMAS-X - An extension of MCMAS to Explicit knowledge. http://www.cs.ucl.ac.uk/staff/f.raimondi/mcmas-x.tar.gz.
• [25] F. Raimondi and A. Lomuscio. http://www.cs.ucl.ac.uk/staff/f.raimondi/MCMAS/, 2006.
• [26] F. Raimondi and A. Lomuscio. Automatic verification ofmulti-agent systems by model checking via OBDDs. Journal of Applied Logic, 2007. To appear in Special issue on Logic-based agent verification.
• [27] M. Wooldridge. An introduction to multi-agent systems. JohnWiley, England, 2002.