@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@inproceedings{DLLT-ICALP2006,
abstract = {Security of a cryptographic protocol for a bounded
number of sessions is usually expressed as a symbolic
trace reachability problem. We show that symbolic
trace reachability for well-defined protocols is
decidable in presence of the exclusive or theory in
combination with the homomorphism axiom. These
theories allow us to model basic properties of
important cryptographic operators. This trace
reachability problem can be expressed as a system of
symbolic deducibility constraints for a certain
inference system describing the capabilities of the
attacker. One main step of our proof consists in
reducing deducibility constraints to constraints for
deducibility in one step of the inference system.
This constraint system, in turn, can be expressed as
a system of quadratic equations of a particular form
over \(\mathbb{Z}/2\mathbb{Z}[h]\), the ring of
polynomials in one indeterminate over the finite
field \(\mathbb{Z}/2\mathbb{Z}\). We show that
satisfiability of such systems is decidable.},
address = {Venice, Italy},
author = {Delaune, St{\'e}phanie and Lafourcade, Pascal and
Lugiez, Denis and Treinen, Ralf},
booktitle = {{P}roceedings of the 33rd {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'06)~--- {P}art~{II}},
OPTDOI = {10.1007/11787006_12},
editor = {Buglesi, Michele and Preneel, Bart and
Sassone, Vladimiro and Wegener, Ingo},
month = jul,
pages = {132-143},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Symbolic Protocol Analysis in Presence of a
Homomorphism Operator and {\emph{Exclusive~Or}}},
volume = {4052},
year = {2006},
acceptrate = {24/81},
acronym = {{ICALP}'06},
nmonth = {7},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}