Affiliations: Institute of Mathematics and Computer Science, Jan
Długosz University, Armii Krajowej 13/15, 42-200 Cz�stochowa, Poland.
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.
penczek@ipipan.waw.pl
Note: [] Address for correspondence: Institute of Computer Science,
Polish Academy of Sciences, Ordona 21, 01-237 Warsaw, Poland
Abstract: A new approach to verification of timed security protocols is given.
The idea consists in modelling a finite number of users (including an intruder)
of the computer network and their knowledge about secrets by timed automata.
The runs of the product automaton of the above automata correspond to all the
behaviours of the protocol for a fixed number of sessions. Verification is
performed using the module BMC of the tool VerICS.
Keywords: timed security protocols, model checking, authentication
