TPMC: A model checker for time–sensitive security protocols

BENERECETTI, MASSIMO and CUOMO, NICOLA and PERON, ADRIANO (2009) TPMC: A model checker for time–sensitive security protocols. [Pubblicazione su rivista scientifica]

Full text non disponibile da questo archivio.

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.

Tipologia di documento:Pubblicazione su rivista scientifica
Parole chiave:Model checking, protocolli sicurezza, verifica, metodi formali
Settori scientifico-disciplinari MIUR:Non specificato
Stato del full text:Accessibilità ristretta
Data:2009
Altri Autori:M. Benerecetti, N. Cuomo, A. Peron
Numero di pagine:12
Intervallo di pagina:pp. 366-377
Volume:4
Numero:5
Dipartimento o Struttura:Dipartimento di Scienze Fisiche
Titolo rivista/pubblicazione:JOURNAL OF COMPUTERS
Numero di sistema:7478
Depositato il:21 Ottobre 2010 08:56
Ultima modifica:21 Ottobre 2010 08:56

Solo per gli Amministratori dell'archivio: edita il record