Stefan Ciobaca, Stéphanie Delaune, and Steve Kremer. Computing knowledge in security protocols under convergent equational theories. In Preliminary Proceedings of the 4th International Workshop on Security and Rewriting Techniques (SecReT'09), pp. 47–58, Port Jefferson, New York, USA, July 2009.
We propose a procedure for the intruder deduction problem and for the static equivalence problem, in the case where cryptographic primitives are modeled by a convergent equational theory. Our procedure terminates on a wide range of equational theories. In particular, we obtain a new decidability result for a theory of trapdoor commitment that we encountered in the study of e-voting protocols. We also provide a prototype implementation.
@inproceedings{CDK-secret09,
abstract = {We propose a procedure for the intruder deduction
problem and for the static equivalence problem, in
the case where cryptographic primitives are modeled
by a convergent equational theory. Our~procedure
terminates on a wide range of equational theories.
In~particular, we~obtain a new decidability result
for a theory of trapdoor commitment that we
encountered in the study of e-voting protocols.
We~also provide a prototype implementation.},
address = {Port Jefferson, New~York, USA},
author = {Ciobaca, Stefan and
Delaune, St{\'e}phanie and Kremer, Steve},
booktitle = {{P}reliminary {P}roceedings of the 4th
{I}nternational {W}orkshop on {S}ecurity and
{R}ewriting {T}echniques ({SecReT}'09)},
editor = {Comon{-}Lundh, Hubert and Meadows, Catherine},
month = jul,
pages = {47-58},
title = {Computing knowledge in security protocols under
convergent equational theories},
year = {2009},
acronym = {{SecReT}'09},
nmonth = {7},
}