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 metadatas

Cited literature [18 references]  Display  Hide  Download

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

File

KMT-jar10.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

263

Files downloads

114