JOURNAL OF COMPUTERS (JCP)
ISSN : 1796-203X
Volume : 4    Issue : 5    Date : May 2009

TPMC: A Model Checker For Time–Sensitive Security Protocols
Massimo Benerecetti, Nicola Cuomo, and Adriano Peron
Page(s): 366-377
Full Text:
PDF (372 KB)


Abstract
In this paper we consider the problem of verifying time–sensitive security protocols, where temporal
aspects explicitly 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, a model checking
tool, TPMC, for the analysis of security protocols is presented, which employs THLPSL as a
specification language and UPPAAL as the model checking engine. To illustrate the tool, we provide
a specification of the Wide Mouthed Frog protocol in THLPSL, and report some experimental results
on a number of timed and untimed security protocols.

Index Terms