Benerecetti, Massimo and Cuomo, Nicola and Peron, Adriano (2009) TPMC: A model checker for time–sensitive security protocols. [Pubblicazione in rivista scientifica]

Il contenuto (Full text) non è disponibile all'interno di questo archivio.
Tipologia del documento: Pubblicazione in rivista scientifica
Titolo: TPMC: A model checker for time–sensitive security protocols
Autori:
AutoreEmail
Benerecetti, Massimo[non definito]
Cuomo, Nicola[non definito]
Peron, Adriano[non definito]
Autore/i: M. Benerecetti, N. Cuomo, A. Peron
Data: 2009
Numero di pagine: 12
Dipartimento: Scienze fisiche
Titolo del periodico: JOURNAL OF COMPUTERS
Data: 2009
Volume: 4
Numero: 5
Intervallo di pagine: pp. 366-377
Numero di pagine: 12
Parole chiave: Model checking, protocolli sicurezza, verifica, metodi formali
Depositato il: 21 Ott 2010 06:56
Ultima modifica: 30 Apr 2014 19:43
URI: http://www.fedoa.unina.it/id/eprint/7478

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.

Actions (login required)

Modifica documento Modifica documento