Steve Kremer: Reducing Equational Theories for the Decision of Static Equivalence (Preliminary Version)

Reducing Equational Theories for the Decision of Static Equivalence (Preliminary Version)

Steve Kremer, Antoine Mercier, and Ralf Treinen. Reducing Equational Theories for the Decision of Static Equivalence (Preliminary Version). In Preliminary Proceedings of the 4th International Workshop on Security and Rewriting Techniques (SecReT'09), Port Jefferson, NY, USA, July 2009.

Download

[PDF] [PS]

Abstract

Static equivalence is a well established notion of indistinguishability of sequences of terms which is useful in the symbolic analysis of cryptographic protocols. Static equivalence modulo equational theories allows a more accurate representation of cryptographic primitives by modelling properties of operators by equational axioms. We develop a method that allows in some cases to simplify the task of deciding static equivalence in a multi-sorted setting, by removing a symbol from the term signature and reducing the problem to several simpler equational theories. We illustrate our technique at hand of bilinear pairings.

BibTeX

@inproceedings{KMT-secret09,
  abstract =      {Static equivalence is a well established notion of
                   indistinguishability of sequences of terms which is
                   useful in the symbolic analysis of cryptographic
                   protocols. Static equivalence modulo equational
                   theories allows a more accurate representation of
                   cryptographic primitives by modelling properties of
                   operators by equational axioms. We develop a method
                   that allows in some cases to simplify the task of
                   deciding static equivalence in a multi-sorted
                   setting, by removing a symbol from the term signature
                   and reducing the problem to several simpler
                   equational theories. We illustrate our technique at
                   hand of bilinear pairings.},
  address =       {Port Jefferson, NY, USA},
  author =        {Kremer, Steve and Mercier, Antoine and Treinen, Ralf},
  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,
  title =         {Reducing Equational Theories for the Decision of
                   Static Equivalence (Preliminary Version)},
  year =          {2009},
  acronym =       {{SecReT}'09},
  nmonth =        {7},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-secret09.pdf},
}