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 Proceedings of the 22nd International Conference on Automated Deduction (CADE'09), pp. 355–370, Lecture Notes in Artificial Intelligence, Springer, Montreal, Canada, August 2009.
doi:10.1007/978-3-642-02959-2_27

Download

[PDF] [PDF (long version)] [PS (long version)] [HTML]

Abstract

In the symbolic analysis of security protocols, two classical notions of knowledge, deducibility and indistinguishability, yield corresponding decision problems. We propose a procedure for both problems under arbitrary convergent equational theories. Our procedure terminates on a wide range of equational theories. In particular, we obtain a new decidability result for a theory we encountered when studying electronic voting protocols. We also provide a prototype implementation.

BibTeX

@inproceedings{CDK-cade09,
  abstract =      {In the symbolic analysis of security protocols, two
                   classical notions of knowledge, deducibility and
                   indistinguishability, yield corresponding decision
                   problems. We~propose a procedure for both problems
                   under arbitrary convergent equational theories.
                   Our~procedure terminates on a wide range of
                   equational theories. In~particular, we~obtain a new
                   decidability result for a theory we encountered when
                   studying electronic voting protocols. We~also provide
                   a prototype implementation.},
  address =       {Montreal, Canada},
  author =        {Ciob{\^a}c{\u{a}}, {\c{S}}tefan and
                   Delaune, St{\'e}phanie and Kremer, Steve},
  booktitle =     {{P}roceedings of the 22nd {I}nternational
                   {C}onference on {A}utomated {D}eduction ({CADE}'09)},
  DOI =           {10.1007/978-3-642-02959-2_27},
  editor =        {Schmidt, Renate},
  month =         aug,
  pages =         {355-370},
  publisher =     {Springer},
  series =        {Lecture Notes in Artificial Intelligence},
  title =         {Computing knowledge in security protocols under
                   convergent equational theories},
  year =          {2009},
  acronym =       {{CADE}'09},
  nmonth =        {8},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CDK-cade09.pdf},
}