Unification modulo a partial theory of exponentiation

TL;DR

This paper investigates the unification problem in a partial theory of modular exponentiation and multiplication, proving its decidability in some cases and undecidability when different group structures are assumed.

Contribution

It introduces a focused subtheory of modular exponentiation and multiplication, establishing new decidability and undecidability results for unification problems.

Findings

Unification is decidable when no additional properties are assumed.

Unification becomes undecidable when multiplication operators are in different abelian groups.

Provides theoretical boundaries for unification in cryptographic algebraic theories.

Abstract

Modular exponentiation is a common mathematical operation in modern cryptography. This, along with modular multiplication at the base and exponent levels (to different moduli) plays an important role in a large number of key agreement protocols. In our earlier work, we gave many decidability as well as undecidability results for multiple equational theories, involving various properties of modular exponentiation. Here, we consider a partial subtheory focussing only on exponentiation and multiplication operators. Two main results are proved. The first result is positive, namely, that the unification problem for the above theory (in which no additional property is assumed of the multiplication operators) is decidable. The second result is negative: if we assume that the two multiplication operators belong to two different abelian groups, then the unification problem becomes undecidable.