Affiliations: Faculty of Computer Science and Information Systems,
Szczecin University of Technology, Zolnierska 49, 70-215 Szczecin, Poland.
E-mail: gjakubowska@wi.ps.pl | Institute of Computer Science, PAS, J.K. Ordona 21,
01-237 Warszawa, Poland and Institute of Informatics, Podlasie Academy,
Sienkiewicza 51, 08-110 Siedlce, Poland. E-mail: penczek@ipipan.waw.pl
Abstract: In this paper we offer a novel methodology for verifying correctness
of (timed) security protocols. The idea consists in computing the time of a
correct execution of a session and finding out whether the Intruder can change
it to shorter or longer by an active attack. Moreover, we generalize the
correspondence property so that attacks can be also discovered when some time
constraints are not satisfied. An implementation of our method is described. As
case studies we verify generalized (timed) authentication of KERBEROS, TMN,
Neumann Stubblebine Protocol, Andrew Secure Protocol,Wide Mouthed Frog, and
NSPK.
