Timed HLPSL for specification and verification of time sensitive protocols

In this paper we face the problem of specifying and verifying security protocols where temporal aspects explicitly appear in the description. For these kinds of protocols we propose an extension of the specification language HLPSL, originally proposed in the context of the Avispa Project and where quantitative temporal aspects were not considered. The semantics of such an extension, called Timed HLPSL, is given in terms of eXtended Timed Automata (XTA). The verification of timed protocols can then exploit standard model checking techniques. In particular, we have developed a protocol verification tool which employs the model checker UPPAAL as the verification engine. To illustrate how our framework applies, we also provide a specification of the Wide Mouthed Frog authentication protocol and show how its temporal features can be specified.