Publications

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

Authors:
BASIN David; CALEIRO Carlos; RAMOS Jaime; VIGANO' Luca
Title:
Distributed Temporal Logic for the Analysis of Security Protocol Models
Year:
2011
Type of item:
Articolo in Rivista
Tipologia ANVUR:
Articolo su rivista
Nations of authors:
STATI UNITI D'AMERICA; ITALIA; PORTOGALLO
Language:
Inglese
Format:
A Stampa
Referee:
Name of journal:
Theoretical Computer Science
ISSN of journal:
0304-3975
N° Volume:
412
Number or Folder:
1
:
Elsevier
Page numbers:
4007-4043
Keyword:
Security protocols, formal methods, temporal logic
Short description of contents:
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.
Product ID:
60915
Handle IRIS:
11562/353870
Deposited On:
November 17, 2012
Last Modified:
November 2, 2016
Bibliographic citation:
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

Related projects
Title Department Managers
SPaCIoS: Secure Provision and Consumption in the Internet of Services Department Informatica Luca Vigano'
<<back

Activities

Research facilities