## 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. In * Proceedings of the 13th Asian Computing Science Conference (ASIAN'09)*, pp. 94–108, Lecture Notes in Computer Science 5913, Springer, Seoul, Korea, December 2009.

doi:10.1007/978-3-642-10622-4_8

### Download

[PDF] [PDF (long version)] [PS] [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 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-asian09, 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 = {Seoul, Korea}, author = {Kremer, Steve and Mercier, Antoine and Treinen, Ralf}, booktitle = {{P}roceedings of the 13th {A}sian {C}omputing {S}cience {C}onference ({ASIAN}'09)}, DOI = {10.1007/978-3-642-10622-4_8}, editor = {Datta, Anupam}, month = dec, pages = {94-108}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, title = {Reducing Equational Theories for the Decision of Static Equivalence}, volume = {5913}, year = {2009}, acronym = {{ASIAN}'09}, nmonth = {12}, url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KMT-asian09.pdf}, }