Skip to Main content Skip to Navigation
New interface
Journal articles

Reducing Equational Theories for the Decision of Static Equivalence

Steve Kremer 1 Antoine Mercier 2 Ralf Treinen 3 
1 CASSIS - Combination of approaches to the security of infinite states systems
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.
Document type :
Journal articles
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Steve Kremer Connect in order to contact the contributor
Submitted on : Wednesday, October 7, 2015 - 10:33:20 PM
Last modification on : Saturday, June 25, 2022 - 9:09:45 PM
Long-term archiving on: : Friday, January 8, 2016 - 10:56:27 AM


Files produced by the author(s)



Steve Kremer, Antoine Mercier, Ralf Treinen. Reducing Equational Theories for the Decision of Static Equivalence. Journal of Automated Reasoning, 2012, 48 (2), pp.197-217. ⟨10.1007/s10817-010-9203-0⟩. ⟨inria-00636797⟩



Record views


Files downloads