Modelling and Checking Timed Authentication of Security Protocols

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.

• Type: Journal
• Year: 2007
• Where: FUIN
• Authors: Gizela Jakubowska, Wojciech Penczek
• Keywords: Active Attack, Correct Execution, FUIN 2007, Security Protocols