Pubblicazioni

Distributed Temporal Logic for the Analysis of Security Protocol Models  (2011)

Autori:
BASIN David; CALEIRO Carlos; RAMOS Jaime; VIGANO' Luca
Titolo:
Distributed Temporal Logic for the Analysis of Security Protocol Models
Anno:
2011
Tipologia prodotto:
Articolo in Rivista
Tipologia ANVUR:
Articolo su rivista
Nazioni degli autori:
STATI UNITI D'AMERICA; ITALIA; PORTOGALLO
Lingua:
Inglese
Formato:
A Stampa
Referee:
Nome rivista:
Theoretical Computer Science
ISSN Rivista:
0304-3975
N° Volume:
412
Numero o Fascicolo:
1
Editore:
Elsevier
Intervallo pagine:
4007-4043
Parole chiave:
Security protocols, formal methods, temporal logic
Breve descrizione dei contenuti:
The distributed temporal logic DTL is an expressive logic, well suited for formalizing properties of concurrent, communicating agents. We show how DTL can be used as a metalogic to reason about and relate different security protocol models. This includes reasoning about model simplifications, where models are transformed to have fewer agents or behaviors, and verifying model reductions, where to establish the validity of a property it suffices to consider its satisfaction on only a subset of models. We illustrate how DTL can be used to formalize security models, protocols, and properties, and then present three concrete examples of metareasoning. First, we prove a general theorem about sufficient conditions for data to remain secret during communication. Second, we prove the equivalence of two models for guaranteeing message-origin authentication. Finally, we relate channel-based and intruder-centric models, showing that it is sufficient to consider models in which the intruder completely controls the network. While some of these results belong to the folklore or have been shown, mutatis mutandis, using other formalisms, DTL provides a uniform means to prove them within the same formalism. It also allows us to clarify subtle aspects of these model transformations that are often neglected or cannot be specified in the first place.
Id prodotto:
60915
Handle IRIS:
11562/353870
depositato il:
17 novembre 2012
ultima modifica:
2 novembre 2016
Citazione bibliografica:
BASIN David; CALEIRO Carlos; RAMOS Jaime; VIGANO' Luca, Distributed Temporal Logic for the Analysis of Security Protocol Models «Theoretical Computer Science» , vol. 412 , n. 12011pp. 4007-4043

Consulta la scheda completa presente nel repository istituzionale della Ricerca di Ateneo IRIS

Progetti Collegati
Titolo Dipartimento Responsabili
SPaCIoS: Secure Provision and Consumption in the Internet of Services Dipartimento Informatica Luca Vigano'
<<indietro

Attività

Strutture