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

Full text not available from this repository.
Item Type: Pubblicazione in rivista scientifica
Title: TPMC: A model checker for time–sensitive security protocols
Creators:
Creators
Email
Benerecetti, Massimo
UNSPECIFIED
Cuomo, Nicola
UNSPECIFIED
Peron, Adriano
UNSPECIFIED
Autore/i: M. Benerecetti, N. Cuomo, A. Peron
Date: 2009
Number of Pages: 12
Department: Scienze fisiche
Journal or Publication Title: JOURNAL OF COMPUTERS
Date: 2009
Volume: 4
Number: 5
Page Range: pp. 366-377
Number of Pages: 12
Keywords: Model checking, protocolli sicurezza, verifica, metodi formali
Date Deposited: 21 Oct 2010 06:56
Last Modified: 30 Apr 2014 19:43
URI: http://www.fedoa.unina.it/id/eprint/7478

Collection description

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.

Downloads

Downloads per month over past year

Actions (login required)

View Item View Item