Reducing Equational Theories for the Decision of Static Equivalence

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 a more accurate representation of cryptographic primitives by modelling properties of operators by equational axioms. We develop a method that allows 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: Conference
• Year: 2009
• Where: ASIAN
• Authors: Steve Kremer, Antoine Mercier 0002, Ralf Treinen
• Keywords: Algorithms, ASIAN 2009, Equational Theories, Static Equivalence, Static Equivalence Modulo