In this paper we face the problem of verifying security protocols where temporal aspects ex- plicitly appear in the description. In previous work, we proposed Timed HLPSL, an extension of the specification language HLPSL (originally developed in the Avispa Project), where quantitative temporal aspects of security protocols can be specified. In this work we present a model checking tool for the analysis of security protocols which employs THLPSL as a specification language and UPPAAL as the model checking engine. To illustrate how our framework applies, we also provide a specification of the Wide Mouthed Frog protocol and show some experimental results on a number of security protocols.
展开▼
