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.

TPMC: A model checker for time–sensitive security protocols

BENERECETTI, MASSIMO;CUOMO, NICOLA;PERON, ADRIANO
2009

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.
File in questo prodotto:
File Dimensione Formato  
TPMC-Jour-Comput-2009.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Accesso privato/ristretto
Dimensione 371.89 kB
Formato Adobe PDF
371.89 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11588/364785
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact