LDYIS: a Framework for Model Checking Security Protocols

• Autorzy: Lomuscio A. , Penczek W.
• 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 the syntax and semantics of a temporal-epistemic security-specialised logic and provide a lazy-intruder model for the protocol rules that we argue to be particularly suitable for verification purposes. We exemplify the technique by finding a (known) bug in the traditional NSPK protocol.

Słowa kluczowe

EN

multi-agent systems

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 85, nr 1-4
• Strony: 359--375
• Opis fizyczny: bibliogr. 21 poz.

Twórcy

autor

Lomuscio A.

autor

Penczek W.

• Institute of Computer Science, Polish Academy of Science, Ordona 21, 01-237 Warsaw, Poland,

Bibliografia

• [1] A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.C. Heám, O. Kouchnarenko, J. Mantovani, S. Mödersheim, 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 Proc of CAV'05, LNCS 3576: 281-285, 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, 1(1):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.
• [7] D. Dolev and A. Yao. On the security of public key protocols. IEEE Trans. Inf. Theory, 29(2):198-208, 1983.
• [8] R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, 1995.
• [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] G. Jakubowska and W. Penczek. Modelling and checking timed authentication of security protocols. In Fundamenta Informaticae, 79(3-4):363-378, 2007.
• [12] M. Kurkowski, W. Penczek, and A. Zbrzezny. Sat-based verification of security protocols via translation to networks of automata. In MoChart IV, volume 4428 of LNAI, pages 146-165. Springer-Verlag, 2007.
• [13] P. Gammie and R. van derMeyden. MCK: Model checking the logic of knowledge. In CAV'04, volume 3114 of LNCS, 479-483. Springer-Verlag, 2004.
• [14] M. Kacprzak, A. Lomuscio, A. Niewiadomski, W. Penczek, F. Raimondi, and M. Szreter. Comparing BDD and SAT based techniques for model checking Chaum's dining cryptographers protocol. Fundamenta Informaticae, Vol 72(1-3), 215-234, 2006.
• [15] A. Lomuscio, F. Raimondi, and B. Wo´zna. Verification of the tesla protocol in mcmas-x. In Proceedings of Concurrency, Specification & Programming (CS&P), Germany, 2006. Humboldt University Press.
• [16] A. Lomuscio and F. Raimondi. MCMAS: A model checker for multi-agent systems. In H. Hermanns and J. Palsberg, editors, Proc. of TACAS 2006, Vienna, volume 3920, 450-454. Springer Verlag, 2006.
• [17] A. Lomuscio and B. Woźna. A complete and decidable security-specialised logic and its application to the TESLA protocol. In Proc. of AAMAS'06, ACM Press, 145-152, 2006.
• [18] W. Penczek and A. Lomuscio. Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2):167-185, 2003.
• [19] 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.
• [20] F. Raimondi and A. Lomuscio. Automatic verification of multi-agent systems bymodel checking via OBDDs. Journal of Applied Logic, 2005. To appear in Special issue on Logic-based agent verification.
• [21] 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.