FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
https://hal.inria.fr/inria-00636797
Contributeur : Steve Kremer
<>
Soumis le : mercredi 7 octobre 2015 - 22:33:20
Dernière modification le : jeudi 15 novembre 2018 - 20:27:00
Document(s) archivé(s) le : vendredi 8 janvier 2016 - 10:56:27
Steve Kremer, Antoine Mercier, Ralf Treinen. Reducing Equational Theories for the Decision of Static Equivalence. Journal of Automated Reasoning, Springer Verlag, 2012, 48 (2), pp.197-217. 〈10.1007/s10817-010-9203-0〉. 〈inria-00636797〉
