Sciweavers

FUIN
2007

Verifying Security Protocols Modelled by Networks of Automata

13 years 3 months ago
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.
Miroslaw Kurkowski, Wojciech Penczek
Added 14 Dec 2010
Updated 14 Dec 2010
Type Journal
Year 2007
Where FUIN
Authors Miroslaw Kurkowski, Wojciech Penczek
Comments (0)