Steve Kremer: Reducing Equational Theories for the Decision of Static Equivalence

Reducing Equational Theories for the Decision of Static Equivalence

Steve Kremer, Antoine Mercier, and Ralf Treinen. Reducing Equational Theories for the Decision of Static Equivalence. Journal of Automated Reasoning, 48(2):197–217, Springer, 2012.
doi:10.1007/s10817-010-9203-0

Download

[PDF] [HTML]

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 for a more accurate representation of cryptographic primitives by modelling properties of operators by equational axioms. We develop a method that allows us 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

@article{KMT-jar10,
  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 for a more accurate representation of
                   cryptographic primitives by modelling properties of
                   operators by equational axioms. We develop a method
                   that allows us 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.},
  author =        {Kremer, Steve and Mercier, Antoine and Treinen, Ralf},
  DOI =           {10.1007/s10817-010-9203-0},
  journal =       {Journal of Automated Reasoning},
  number =        {2},
  pages =         {197-217},
  publisher =     {Springer},
  title =         {Reducing Equational Theories for the Decision of
                   Static Equivalence},
  volume =        {48},
  year =          {2012},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-jar10.pdf},
}