pith. sign in

arxiv: 1907.00227 · v1 · pith:SFXBMP2Pnew · submitted 2019-06-29 · 💻 cs.CC · cs.CR

On Asymmetric Unification for the Theory of XOR with a Homomorphism

Christopher Lynch , Andrew M. Marshall , Catherine Meadows , Paliath Narendran , Veena Ravishankar This is my paper

Pith reviewed 2026-05-25 12:35 UTC · model grok-4.3

classification 💻 cs.CC cs.CR
keywords asymmetric unificationACUNhXORhomomorphismautomata-based decision procedureirreducibility constraintscryptographic protocol analysisvariant unification
0
0 comments X

The pith

The theory ACUNh of XOR with homomorphism has an automata-based decision procedure for asymmetric unification.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops decision procedures for asymmetric unification problems in the equational theory ACUNh, which combines XOR with a homomorphism. It first builds an automata-based procedure specific to this theory, then combines it with an existing asymmetric unification method to handle the general case. Finally it gives a new construction for an automaton that generates solutions rather than merely deciding existence. A sympathetic reader would care because asymmetric unification arises directly in the automated analysis of cryptographic protocols, and few such procedures exist for common algebraic theories. If the procedures are correct, they supply both decidability and a practical way to produce solutions under irreducibility constraints.

Core claim

Asymmetric unification problems in ACUNh are decidable by automata constructions; these constructions can be lifted via an asymmetric combination procedure to a general decision method, and a separate construction yields a solution-generating automaton for the same theory.

What carries the argument

An automata-based decision procedure for asymmetric ACUNh unification that tracks irreducibility constraints during state transitions.

If this is right

  • Asymmetric unification in ACUNh becomes decidable.
  • The decision procedure extends to the combined theory via the adapted asymmetric combination method.
  • A solution-generating automaton can be obtained directly for asymmetric ACUNh problems.
  • The automata approach can be compared directly with variant unification on the same problems.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same automata technique might be tried on other XOR-based theories that appear in protocol analysis.
  • If the solution-generating automaton can be made efficient, it could replace variant unification in tools that already use ACUNh.
  • The decision procedure supplies a concrete benchmark for measuring the overhead of irreducibility constraints versus ordinary unification.

Load-bearing premise

Automata constructions that track irreducibility can be made to terminate and correctly decide all asymmetric unification problems in ACUNh.

What would settle it

A concrete ACUNh unification problem with an irreducibility constraint for which the constructed automaton either fails to halt or produces an incorrect yes/no answer.

Figures

Figures reproduced from arXiv: 1907.00227 by Andrew M. Marshall, Catherine Meadows, Christopher Lynch, Paliath Narendran, Veena Ravishankar.

Figure 1
Figure 1. Figure 1: Automata Construction Fig. 1a: Let Pi ,Qi and Ri denote the i th bits of P,Q and R respectively. Pi has a value 1, when either Qi or Ri has a value 1. We need 3-bit alphabet symbols for this equation. The input for this automaton are column vectors of 3-bits each, i.e., Σ = { 0 0 0  ,··· ,  1 1 1  }.  For example, if R2 = 0, Q2 = 1, then P2 = 1. The corresponding alphabet symbol is P2 Q2 R2  =  1 0 … view at source ↗
Figure 2
Figure 2. Figure 2: Automata construction Fig. 2a: We need 2-bit vectors as alphabet symbols since we have two unknowns X and Y. Remember that h acts like the successor function. q0 is the only accepting state. A state transition occurs with bit vectors 1 0  , [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Automata construction The string 1 0 0 1 0 1 0 0 0 0 1 1 0 0 0 0  is accepted by all the three automata. The correspond￾ing asymmetric unifier is {V 7→ a, W 7→ h(a), Y 7→ h 2 (a), U 7→ (h 2 (a) +a)}. start q0 q1 q2 × 1 0 ×  × 0 0 ×  × 0 1 ×  × 1 1 ×  × 0 0 ×  × 1 0 ×  (a) Automata for Example 3.1, Part 1 start q0 q1 q3 q2  0 × 0 0   1 × 0 1   0 × 1 1   0 × 0 0  ,  0 × 1 1   1… view at source ↗
Figure 4
Figure 4. Figure 4: Automata example Once we have automata constructed for all the formulas, we take the intersection and check if there exists a string accepted by all the automata. If the intersection is not empty, then we have a solution or an asymmetric unifier for the given problem. Problems with more than one constant : This technique can be extended to the case where we have more than one constant. Suppose we have k co… view at source ↗
Figure 5
Figure 5. Figure 5: Automata example Algorithm 1 ACUNh-decision Procedure for a single constant Require: Asymmetric ACUNh-unification problem S. For S construct automata for each equation as outlined in the paragraph “Problems with one constant”. Let these be A1,A2,...,An. “Intersect the automata”: Let A be the automaton that recognizes Tn i=1 L(Ai). if L(A ) = /0 then return ‘no solution.’ else return a solution. end if We e… view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 0 minor

Summary. The paper examines asymmetric unification (unification with irreducibility constraints) for the equational theory ACUNh of XOR with a homomorphism. It develops an automata-based decision procedure for the asymmetric ACUNh problem, adapts a recently developed asymmetric combination procedure to obtain a general decision procedure for asymmetric ACUNh, and presents a new approach for constructing a solution-generating asymmetric-ACUNh unification automaton. The work also compares the approach to variant unification.

Significance. Asymmetric unification remains an important but sparsely populated area for cryptographic protocol analysis. If the automata constructions are correct and the combination adaptation preserves soundness, the paper supplies decision procedures and a solution-generating automaton for a theory (ACUNh) that arises in protocol modeling, extending the small existing toolkit beyond variant unification.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of our manuscript and for recommending minor revision. The referee's description of the paper's contributions to asymmetric unification for ACUNh is accurate.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper constructs automata-based decision procedures and a solution-generating automaton for asymmetric ACUNh unification by adapting prior asymmetric unification methods and a recently developed combination procedure. No derivation step reduces by construction to its own inputs, fitted parameters renamed as predictions, or load-bearing self-citations whose justification collapses into the present work. The claims rest on explicit algorithmic constructions that are independent of the target results and draw on external literature without self-referential definitions or ansatz smuggling.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The paper is a theoretical contribution in equational unification. It relies on standard mathematical properties of the ACUNh theory (associativity, commutativity, unit, nilpotency for XOR, and homomorphism axioms) but introduces no fitted parameters or new postulated entities. No free parameters or invented entities are identifiable from the abstract.

axioms (1)
  • domain assumption The equational theory ACUNh is defined by the standard axioms for XOR (ACUN) together with the homomorphism axioms.
    Invoked when the authors state they examine ACUNh from the asymmetric unification viewpoint.

pith-pipeline@v0.9.0 · 5664 in / 1396 out tokens · 42530 ms · 2026-05-25T12:35:44.465675+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

14 extracted references · 14 canonical work pages

  1. [1]

    Handbook of A utomated Reasoning 1, 445–532 (2001)

    Baader, F., Snyder, W .: Unification theory. Handbook of A utomated Reasoning 1, 445–532 (2001)

    work page 2001

  2. [2]

    Mathematical Logic Quarterly 6(1-6), 66–92 (1960)

    B¨ uchi, J.R.: Weak second-order arithmetic and finite au tomata. Mathematical Logic Quarterly 6(1-6), 66–92 (1960)

    work page 1960

  3. [3]

    In: Proceedings of CR YPTO ’83

    Chaum, D.: Blind signature system. In: Proceedings of CR YPTO ’83. p. 153 (1983)

    work page 1983

  4. [4]

    Comon-Lundth, H., Delaune, S.: The finite variant proper ty: how to get rid of some algebraic properties, in Proc RTA’05, Springer LNCS 3467, 294–307, 2005

    work page 2005

  5. [5]

    Transactions of the American Mathematical Society 98(1), 2 1–51 (1961)

    Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Transactions of the American Mathematical Society 98(1), 2 1–51 (1961)

    work page 1961

  6. [6]

    , Meadows, C., Meseguer, J., Narendran, P ., Santiago, S., Sasse, R.: Asymmetric Unifi cation: A New Unifi- cation Paradigm for Cryptographic Protocol Analysis

    Erbatur, S., Escobar, S., Kapur, D., Liu, Z., Lynch, C.A. , Meadows, C., Meseguer, J., Narendran, P ., Santiago, S., Sasse, R.: Asymmetric Unifi cation: A New Unifi- cation Paradigm for Cryptographic Protocol Analysis. In: A utomated Deduction, (CADE-24), LNCS, vol. 7898, pp. 231–248 (2013)

    work page 2013

  7. [7]

    In: Foundations of Software Science and Computation ( FOSSACS-17), vol- ume 8412 LNCS

    Erbatur, S., Kapur, D., Marshall, A.M., Meadows, C.A., N arendran, P ., Ringeis- sen, C.: On asymmetric unification and the combination probl em in disjoint theo- ries. In: Foundations of Software Science and Computation ( FOSSACS-17), vol- ume 8412 LNCS. pp. 274–288 (2014)

    work page 2014

  8. [8]

    Escobar, S., Meseguer, J., Sasse, R.: V ariant narrowing and equational unification. Electr. Notes in Theoretical Computer Science 238(3), 103– 119 (2009)

    work page 2009

  9. [9]

    Klaedtke, F., Ruess, H.: Parikh automata and monadic sec ond-order logics with linear cardinality constraints (2002) On Asymmetric Unification for the Theory of XOR with a Homomor phism 17

    work page 2002

  10. [10]

    In: Pro- ceedings, 11th Annual IEEE Symposium on Logic in Computer Sc ience, New Brunswick, New Jersey, USA, July 27-30, 1996

    Narendran, P .: Solving linear equations over polynomi al semirings. In: Pro- ceedings, 11th Annual IEEE Symposium on Logic in Computer Sc ience, New Brunswick, New Jersey, USA, July 27-30, 1996. pp. 466–472. I EEE Computer Society (1996)

    work page 1996

  11. [11]

    In: Proceedings of EUROCRYPT ’99

    Paillier, P .: Public-key cryptosystems based on compo site degree residu- osity classes. In: Proceedings of EUROCRYPT ’99. pp. 223–23 8 (1999), https://doi.org/10.1007/3-540-48910-X_16

    work page doi:10.1007/3-540-48910-x_16 1999

  12. [12]

    Rivest, R.L., Shamir, A., Adleman, L.M.: A method for ob taining digital sig- natures and public-key cryptosystems. Commun. ACM 21(2), 1 20–126 (1978), http://doi.acm.org/10.1145/359340.359342

    work page doi:10.1145/359340.359342 1978

  13. [13]

    if” part, let θ be the matching substitution. Then the substitution θ ′, defined as yθ ′= h(yθ ) for all y matches s with h(t). For the “only if

    V ardi, M.Y ., Wilke, T.: Automata: From Logics to Algori thms. Logic and au- tomata 2, 629–736 (2008) A Proof of R2, ACh convergence A.1 R2 is ACh-convergent To begin with let us show that the theory, → R2/ACh, is terminating. Lemma A.1 → R2/ACh is terminating. Proof. We use a polynomial interpretation. The signature of R2 is Σ = {+, h, 0}. We take the p...

    work page 2008

  14. [14]

    identified

    where t′ 1 ≈ AC t|p. If t′ 1 is reducible then so is t′; if not, then t′ is a smaller counterexample. Corollary A.8.1 F or all t, t′, t′′: if t is reducible by − → R2,ACh and t ′′ ≈ AC t + t′ then t′′is also reducible by − → R2,ACh. Lemma A.9 F or all s1, s2, s3: if s 1 − → Rh,AC s2, and s 2 − → R2,ACh s3, then s 1 is also reducible by − → R2,ACh. 20 Lync...

    work page