Title
Distributed temporal logic for the analysis of security protocol models
Abstract
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.
Year
DOI
Venue
2011
10.1016/j.tcs.2011.04.006
Theor. Comput. Sci.
Keywords
DocType
Volume
Security protocols,Security protocol analysis,Security protocol models,Temporal logic,Distributed temporal logic
Journal
412
Issue
ISSN
Citations 
31
0304-3975
10
PageRank 
References 
Authors
0.66
55
4
Name
Order
Citations
PageRank
David A. Basin14930281.93
Carlos Caleiro213515.77
Jaime Ramos3798.31
Luca Viganò488365.69