A Coq Formalization of Unification Modulo Exclusive-Or

TL;DR

The paper formalizes XOR unification in Coq, addressing unification modulo the XOR theory defined by $\oplus$ and $0$ with associativity, commutativity, identity, and nilpotency. It builds a rewrite-based approach that reduces terms to a canonical list-shaped form and proves soundness, completeness, and termination, with Coq proofs and OCaml extraction. Key contributions include a formal XOR-unification algorithm, machine-checked proofs of MGUnification properties, and a practical pathway to verified implementations for security protocol analysis. The work lays a foundation for extending XOR reasoning to uninterpreted and homomorphic functions and for integrating XOR-unification into logic-programming-based security analyses.

Abstract

Equational Unification is a critical problem in many areas such as automated theorem proving and security protocol analysis. In this paper, we focus on XOR-Unification, that is, unification modulo the theory of exclusive-or. This theory contains an operator with the properties Associativity, Commutativity, Nilpotency, and the presence of an identity. In the proof assistant Coq, we implement an algorithm that solves XOR unification problems, whose design was inspired by Liu and Lynch, and prove it sound, complete, and terminating. Using Coq's code extraction capability we obtain an implementation in the programming language OCaml.

Figures (4)

• Figure 1: Term Definition
• Figure 2: Equivalence Definition
• Figure 3: Solution found imply solution, solves, most general and idempotent
• Figure 4: Not solvable implies no solution found

Theorems & Definitions (3)

• Lemma 1
• Lemma 2
• Theorem 1