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},
}