Verifying Security Protocols Modelled by Networks of Automata

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

Article type: Research Article

Authors: Kurkowski, Mirosław | Penczek, Wojciech

Affiliations: Institute of Mathematics and Computer Science, Jan Długosz University Armii Krajowej 13/15, 42-200 Cz�stochowa, Poland. E-mail: m.kurkowski@ajd.czest.pl | Institute of Computer Science, Polish Academy of Sciences Ordona 21, 01-237 Warsaw, Poland and Institute of Informatics, Podlasie Academy, Sienkiewicza 51, 08-110 Siedlce, Poland. E-mail: penczek@ipipan.waw.pl

Abstract: In this paper we show a novel method for modelling behaviours of security protocols using networks of communicating automata in order to verify them with SAT-based bounded model checking. These automata correspond to executions of the participants as well as to their knowledge about letters. Given a bounded number of sessions, we can verify both correctness or incorrectness of a security protocol proving either reachability or unreachability of an undesired state. We exemplify all our notions on the Needham Schroeder Public Key Authentication Protocol (NSPK) and show experimental results for checking authentication using the verification tool VerICS.

Keywords: security protocols, model checking, authentication

Journal: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 453-471, 2007