TPMC: A Model Checker For Time–Sensitive Security Protocols

Abstract—In this paper we face the problem of ver-ifying security protocols where temporal aspects ex-plicitly appear in the description. In previous work, we proposed Timed HLPSL, an extension of the speci-fication 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 spec-ification language and UPPAAL as the model check-ing 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. I