LDYIS: a Framework for Model Checking Security Protocols

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

Article type: Research Article

Authors: Lomuscio, Alessio | Penczek, Wojciech

Affiliations: Department of Computing, Imperial College London, UK. A.Lomuscio@doc.ic.ac.uk | Institute of Computer Science, PAS, and University of Podlasie, Poland. penczek@ipipan.waw.pl

Note: [] Address for correspondence: Institute of Computer Science, PAS ul. Ordona 21, 01-237 Warsaw, Poland

Abstract: 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 securityspecialised 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.

Journal: Fundamenta Informaticae, vol. 85, no. 1-4, pp. 359-375, 2008