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
Contributor : Steve Kremer
<>
Submitted on : Wednesday, October 7, 2015 - 10:33:20 PM
Last modification on : Friday, January 4, 2019 - 5:32:59 PM
Long-term archiving on : Friday, January 8, 2016 - 10:56:27 AM
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⟩
