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.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2012, 48 (2), pp.197-217. 〈10.1007/s10817-010-9203-0〉
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

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

Fichier

KMT-jar10.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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〉

Partager

Métriques

Consultations de la notice

232

Téléchargements de fichiers

58