Verifying Security Protocols Modelled by Networks of Automata

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.

• Type: Journal
• Year: 2007
• Where: FUIN
• Authors: Miroslaw Kurkowski, Wojciech Penczek
• Keywords: Automata Correspond, FUIN 2007, SAT-based Bounded Model, Security Protocol