Volume 4 Number 5 (May 2009)
Home > Archive > 2009 > Volume 4 Number 5 (May 2009) >
JCP 2009 Vol.4(5): 366-377 ISSN: 1796-203X
doi: 10.4304/jcp.4.5.366-377

TPMC: A Model Checker For Time–Sensitive Security Protocols

Massimo Benerecetti, Nicola Cuomo, Adriano Peron
Dept. of Physical Sciences, Universit`a di Napoli “Federico II”, Napoli, Italy
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.

[PDF]

Cite: Massimo Benerecetti, Nicola Cuomo, Adriano Peron, "TPMC: A Model Checker For Time–Sensitive Security Protocols," Journal of Computers vol. 4, no. 5, pp. 366-377, 2009.

General Information

ISSN: 1796-203X
Abbreviated Title: J.Comput.
Frequency: Bimonthly
Editor-in-Chief: Prof. Liansheng Tan
Executive Editor: Ms. Nina Lee
Abstracting/ Indexing: DBLP, EBSCO,  ProQuest, INSPEC, ULRICH's Periodicals Directory, WorldCat,etc
E-mail: jcp@iap.org
  • Nov 14, 2019 News!

    Vol 14, No 11 has been published with online version   [Click]

  • Mar 20, 2020 News!

    Vol 15, No 2 has been published with online version   [Click]

  • Dec 16, 2019 News!

    Vol 14, No 12 has been published with online version   [Click]

  • Sep 16, 2019 News!

    Vol 14, No 9 has been published with online version   [Click]

  • Aug 16, 2019 News!

    Vol 14, No 8 has been published with online version   [Click]

  • Read more>>