Is Your Security Protocol on Time ?

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. As case studies we verify generalized authentication of KERBEROS, TMN, Neumann Stubblebine Protocol, Andrew Secure Protocol, WMF, and NSPK.

• Type: Conference
• Year: 2007
• Where: FSEN
• Authors: Gizela Jakubowska, Wojciech Penczek
• Keywords: Correct Execution, FSEN 2007, Neumann Stubblebine Protocol, Security Protocols