Stéphanie Delaune, Steve Kremer, and Daniel Pasail\ua. Security protocols, constraint systems, and group theories. In Proceedings of the 6th International Joint Conference on Automated Reasoning (IJCAR'12), pp. 164–178, Lecture Notes in Artificial Intelligence 7364, Springer-Verlag, Manchester, UK, June 2012.
When formally analyzing security protocols it is often important to express properties in terms of an adversary's inability to distinguish two protocols. It has been shown that this problem amounts to deciding the equivalence of two constraint systems, i.e., whether they have the same set of solutions. In this paper we study this equivalence problem when cryptographic primitives are modeled using a group equational theory, a special case of monoidal equational theories. The results strongly rely on the isomorphism between group theories and rings. This allows us to reduce the problem under study to the problem of solving systems of equations over rings.
We provide several new decidability and complexity results, notably for equational theories which have applications in security protocols, such as exclusive or and Abelian groups which may additionally admit a unary, homomorphic symbol.
@inproceedings{DKP-ijcar12,
abstract = {When formally analyzing security protocols it is
often important to express properties in terms of an
adversary's inability to distinguish two protocols.
It has been shown that this problem amounts to
deciding the equivalence of two constraint systems,
i.e., whether they have the same set of solutions. In
this paper we study this equivalence problem when
cryptographic primitives are modeled using a group
equational theory, a special case of monoidal
equational theories. The results strongly rely on the
isomorphism between group theories and rings. This
allows us to reduce the problem under study to the
problem of solving systems of equations over
rings.\par We provide several new decidability and
complexity results, notably for equational theories
which have applications in security protocols, such
as exclusive or and Abelian groups which may
additionally admit a unary, homomorphic symbol.},
address = {Manchester, UK},
author = {Delaune, St{\'e}phanie and Kremer, Steve and
Pasail{\u{a}}, Daniel},
booktitle = {{P}roceedings of the 6th {I}nternational {J}oint
{C}onference on {A}utomated {R}easoning ({IJCAR}'12)},
OPTDOI = {10.1007/978-3-642-31365-3_15},
editor = {Gramlich, Bernhard and Miller, Dale and Sattler, Uli},
month = jun,
pages = {164-178},
publisher = {Springer-Verlag},
series = {Lecture Notes in Artificial Intelligence},
title = {Security protocols, constraint systems, and group
theories},
volume = {7364},
year = {2012},
acronym = {{IJCAR}'12},
nmonth = {6},
OPTLONGPDF = {https://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/
rr-lsv-2012-06.pdf},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}