Timed model checking of security protocols
Ricardo Corin, Sandro Etalle, Pieter Hartel, Angelika Mader · 2004
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.