Steve Kremer: Computing knowledge in security protocols under convergent equational theories

Computing knowledge in security protocols under convergent equational theories

Ștefan Ciobâcă, 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, NY, USA, July 2009.

Download

[PDF]

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.

BibTeX

@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, NY, USA},
  author =        {Ciob{\^a}c{\u{a}}, {\c{S}}tefan 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},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-secret09.pdf},
}