Modelling and Checking Timed Authentication of Security Protocols

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

Article type: Research Article

Authors: Jakubowska, Gizela | Penczek, Wojciech

Affiliations: Faculty of Computer Science and Information Systems, Szczecin University of Technology, Zolnierska 49, 70-215 Szczecin, Poland. E-mail: [email protected] | 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: [email protected]

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.

Journal: Fundamenta Informaticae, vol. 79, no. 3-4, pp. 363-378, 2007