Hubert Comon-Lundh, Stéphanie Delaune, and Jonathan K. Millen. Constraint solving techniques and enriching the model with equational theories. In Véronique Cortier and Steve Kremer, editors, Formal Models and Techniques for Analyzing Security Protocols, Cryptology and Information Security Series, pp. 35–61, IOS Press, 2011.
Derivability constraints represent in a symbolic way the infinite set of possible executions of a finite protocol, in presence of an arbitrary active attacker. Solving a derivability constraint consists in computing a simplified representation of such executions, which is amenable to the verification of any (trace) security property. Our goal is to explain this method on a non-trivial combination of primitives.
In this chapter we explain how to model the protocol executions using derivability constraints, and how such constraints are interpreted, depending on the cryptographic primitives and the assumed attacker capabilities. Such capabilities are represented as a deduction system that has some specific properties. We choose as an example the combination of exclusive-or, symmetric encryption\slashdecryption and pairing\slashunpairing. We explain the properties of the deduction system in this case and give a complete and terminating set of rules that solves derivability constraints. A similar set of rules has been already published for the classical Dolev-Yao attacker, but it is a new result for the combination of primitives that we consider. This allows to decide trace security properties for this combination of primitives and arbitrary finite protocols.
@incollection{CDM-fmtasp11,
abstract = {Derivability constraints represent in a symbolic way
the infinite set of possible executions of a finite
protocol, in presence of an arbitrary active
attacker. Solving a derivability constraint consists
in computing a simplified representation of such
executions, which is amenable to the verification of
any (trace) security property. Our goal is to explain
this method on a non-trivial combination of
primitives.\par In this chapter we explain how to
model the protocol executions using derivability
constraints, and how such constraints are
interpreted, depending on the cryptographic
primitives and the assumed attacker capabilities.
Such capabilities are represented as a deduction
system that has some specific properties. We choose
as an example the combination of exclusive-or,
symmetric encryption{\slash}decryption and
pairing{\slash}unpairing. We explain the properties
of the deduction system in this case and give a
complete and terminating set of rules that solves
derivability constraints. A similar set of rules has
been already published for the classical Dolev-Yao
attacker, but it is a new result for the combination
of primitives that we consider. This allows to decide
trace security properties for this combination of
primitives and arbitrary finite protocols.},
author = {Comon{-}Lundh, Hubert and Delaune, St{\'e}phanie and
Millen, Jonathan K.},
booktitle = {Formal Models and Techniques for Analyzing Security
Protocols},
editor = {Cortier, V{\'e}ronique and Kremer, Steve},
pages = {35-61},
publisher = {{IOS} Press},
series = {Cryptology and Information Security Series},
title = {Constraint solving techniques and enriching the model
with equational theories},
volume = {5},
year = {2011},
lsv-category = {chap},
wwwpublic = {public and ccsb},
}