Stéphanie Delaune, Pascal Lafourcade, Denis Lugiez, and Ralf Treinen. Symbolic Protocol Analysis in Presence of a Homomorphism Operator and Exclusive Or. In Proceedings of the 33rd International Colloquium on Automata, Languages and Programming (ICALP'06) --- Part II, pp. 132–143, Lecture Notes in Computer Science 4052, Springer, Venice, Italy, July 2006.
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 \(\mathbbZ/2\mathbbZ[h]\), the ring of polynomials in one indeterminate over the finite field \(\mathbbZ/2\mathbbZ\). We show that satisfiability of such systems is decidable.
@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},
}