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
2 LSV - Laboratoire Spécification et Vérification [Cachan]
3 PPS - Preuves, Programmes et Systèmes

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.

Domaines: Cryptographie et sécurité [cs.CR]

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⟩