On Asymmetric Unification for the Theory of XOR with a Homomorphism
This work addresses a gap in automated cryptographic protocol analysis by providing new algorithms for asymmetric unification, though it appears incremental as it builds on existing methods and focuses on a specific theory.
The paper tackled the lack of asymmetric unification algorithms by developing a new automata-based decision procedure for the theory of XOR with a homomorphism (ACUNh), adapting a combination procedure to produce a general asymmetric-ACUNh decision procedure, and presenting a new approach for solution-generating unification automata.
Asymmetric unification, or unification with irreducibility constraints, is a newly developed paradigm that arose out of the automated analysis of cryptographic protocols. However, there are still relatively few asymmetric unification algorithms. In this paper we address this lack by exploring the application of automata-based unification methods. We examine the theory of xor with a homomorphism, ACUNh, from the point of view of asymmetric unification, and develop a new automata-based decision procedure. Then, we adapt a recently developed asymmetric combination procedure to produce a general asymmetric- ACUNh decision procedure. Finally, we present a new approach for obtaining a solution-generating asymmetric-ACUNh unification automaton. We also compare our approach to the most commonly used form of asymmetric unification available today, variant unification.