Timed model checking of security protocols

Abstract

We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol. Timing information allows us to study of different attack scenarios. We illustrate the attacks by model checking the protocol using Uppaal. We also present new challenges and threats that arise when considering time. Copyright 2004 ACM.