Model checking security protocols : a multi-agent system approach

• Autorzy: Lomuscio A. , Penczek W.

Warianty tytułu

PL

Weryfikacja modelowa protokołów kryptograficznych : podejście bazujące na systemach wieloagentowych

• Języki publikacji: EN

Abstrakty

EN

We present a formalism for the automatic verification of security protocols based on multi-agent systems semantics. We give syntax and semantics of a temporal-epistemic security-specialised logie and provide a lazy-intruder model for the protocol rules that is arguably particularly suitable for verification purposes. We exemplify the techniąue by finding a (known) bug in the traditional NSPK protocol

PL

Praca prezentuje nowe podejście do automatycznej weryfikacji protokołów kryptograficznych, bazujące na semantyce systemów wieloagentowych. Podajemy składnię i semantykę temporalno-epistemicznej logiki dla protokołów kryptograficznych oraz model intruza typu "lazy", który jest szczególnie właściwy dla celów weryfikacji. Nasza technika jest przedstawiona na przykladzie protokołu NSPK, dla którego znajdujemy znany atak.

Słowa kluczowe

PL

protokoły kryptograficzne; weryfikacja modelowa; uwierzytelnienie; intruz "lazy"

• Wydawca: Instytut Podstaw Informatyki PAN
• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2007
• Tom: Nr 1000
• Strony: 1--23
• Opis fizyczny: Bibliogr. 18 poz.

Twórcy

autor

Lomuscio A.

autor

Penczek W.

• Department of Computing Imperial College London London SW72BZ, UK,

Bibliografia

• [1] A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.-C. Heam, 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.
• [2] A. Armando and L. Compagna. An optimized intruder model for SAT-based model-checking of security protocols. ENTCS, 125(1):91-108, 2005.
• [3] M. Burrows, M. Abadi, R. Needham. A Logic of Authentication, ACM Trans. Comput. Syst. 8(1): 18-36, 1990.
• [4] D. A. Basin, S. Módersheim, and Luca Viganó. OFMC: A symbolic model checker for security protocols. International Journal of Information Security, 4(3):181-208, 2005.
• [5] D. Chaum. The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of Cryptology, l(l):65-75, 1988.
• [6] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Pólrola, M. Szreter, B. Woźna, and A. Zbrzezny. Verics- A tool for verifying Timed Automata and Estelle specifications. In Proc. of TACAS'03, volume 2619 of LNCS, 278-283. Springer-Verlag, 2003.
• [9] J. Halpern, R. van der Meyden, and R. Pucella. Revisiting the foundations of authentication logics.
• [10] J. Y. Halpern and R. Pucella. Modeling adversaries in a logic for security protocol analysis. In Proc. FASec'02), volume 2629 of LNCS, pages 115-132. Springer-Verlag, 2003.
• [11] P. Gammie and R. van der Meyden. MCK: Model checking the logic of knowledge. In CAV04, volume 3114 of LNCS, 479-483. Springer-Yerlag, 2004.
• [12] M. Kacprzak, A. Lomuscio, A. Niewiadomski, W. Penczek, F. Raimondi, and M. Szreter. Comparing BDD and S AT based techniques for model checking Chaum's dining cryptographers protocol. Fundamenta Informaticae, Vol. 72(1-3), 215-234, 2006.
• [13] A. Lomuscio, F.Raimondi, and B. Woźna. Verification of the tesla protocol in mcmas-x. In Proceedings of Concurrency, Specification & Programming (CS&P), Germany, 2006. Humboldt University Press.
• [14] A. Lomuscio and F. Raimondi. MCMAS: A model checker for multi-agent systems. In H. Hermanns and J. Palsberg, editors, Proc. of TAC AS 2006, Vienna, volume 3920, 450-454. Springer Verlag, 2006.
• [15] W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2):167-185, 2003.
• [16] W. Penczek, B. Woźna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL. Fundamenta Informaticae, 51(1-2):135-156, 2002.
• [17] F. Raimondi and A. Lomuscio. Automatic verification of multi-agent systems by model checking via OBDDs. Journal of Applied Logic, 2005. To appear in Special issue on Logic-based agent verification.
• [18] R. van der Meyden and Kaile Su. Symbolic model checking the knowledge of the dining cryptographers. In Proc. CSFW'04, 280-291, USA, 2004. IEEE Computer Society.