eng
episciences.org
Logical Methods in Computer Science
1860-5974
2015-06-19
Volume 11, Issue 2
10.2168/LMCS-11(2:11)2015
1571
journal article
On Unification Modulo One-Sided Distributivity: Algorithms, Variants and Asymmetry
Andrew M Marshall
Catherine Meadows
Paliath Narendran
An algorithm for unification modulo one-sided distributivity is an early
result by Tid\'en and Arnborg. More recently this theory has been of interest
in cryptographic protocol analysis due to the fact that many cryptographic
operators satisfy this property. Unfortunately the algorithm presented in the
paper, although correct, has recently been shown not to be polynomial time
bounded as claimed. In addition, for some instances, there exist most general
unifiers that are exponentially large with respect to the input size. In this
paper we first present a new polynomial time algorithm that solves the decision
problem for a non-trivial subcase, based on a typed theory, of unification
modulo one-sided distributivity. Next we present a new polynomial algorithm
that solves the decision problem for unification modulo one-sided
distributivity. A construction, employing string compression, is used to
achieve the polynomial bound. Lastly, we examine the one-sided distributivity
problem in the new asymmetric unification paradigm. We give the first
asymmetric unification algorithm for one-sided distributivity.
https://lmcs.episciences.org/1571/pdf
Computer Science - Logic in Computer Science