@article{Laf07c,
title = { Intruder Deduction for the Equational Theory of Exclusive-or with Commutative and Distributive Encryption },
author = {Lafourcade, Pascal},
month = {jul},
year = {2007},
booktitle = {{P}roceedings of the 1st {I}nternational {W}orkshop on {S}ecurity and {R}ewriting {T}echniques ({SecReT}'06)},
address = {Venice, Italy},
journal = {Electronic Notes in Theoretical Computer Science},
number = {4},
pages = {37-57},
publisher = {Elsevier Science Publishers},
series = {Electronic Notes in Theoretical Computer Science},
volume = {171},
team = {other},
abstract = {The first step in the verification of cryptographic protocols is to decide the intruder deduction problem, that is the vulnerability to a so-called passive attacker. We~extend the Dolev-Yao model in order to model this problem in presence of the equational theory of a commutative encryption operator which distributes over the \emph{exclusive-or} operator. The~interaction between the commutative distributive law of the encryption and \emph{exclusive-or} offers more possibilities to decrypt an encrypted message than in the non-commutative case, which imply a more careful analysis of the proof system. We~prove decidability of the intruder deduction problem for a commutative encryption which distributes over \emph{exclusive-or} with a DOUBLE-EXPTIME procedure. And~we obtain that this problem is EXPSPACE-hard in the binary case.},
}
