@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@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},
}