Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis

We present a new paradigm for unification arising out of a technique commonly used in cryptographic protocol analysis tools that employ unification modulo equational theories. This paradigm relies on: (i) a decomposition of an equational theory into (R, E) where R is confluent, terminating, and coherent modulo E, and (ii) on reducing unifi- cation problems to a set of problems s =^? t under the constraint that t remains R/E-irreducible. We call this method asymmetric unification . We first present a general-purpose generic asymmetric unification algorithm.and then outline an approach for converting special-purpose conventional unification algorithms to asymmetric ones, demonstrating it for exclusive-or with uninterpreted function symbols. We demonstrate how asymmetric unification can improve performanceby running the algorithm on a set of benchmark problems. We also give results on the complexity and decidability of asymmetric unification.