关于模单侧分配的统一：算法、变式和不对称性
On Unification Modulo One-Sided Distributivity: Algorithms, Variants and Asymmetry
摘要：
模单侧分配性的统一算法是Tidén和Arnborg的早期结果。最近，由于许多密码运算符满足这一性质，这一理论在密码协议分析中引起了人们的兴趣。不幸的是，该算法的文件，虽然正确的，最近已被证明不是多项式时间有界的声称。此外，对于某些情况，存在相对于输入大小呈指数级大的最一般的统一器。在本文中，我们首先提出了一个新的多项式时间算法，解决了决定问题的一个非平凡的子情况下，基于类型化理论，统一模单侧分配。接下来，我们提出了一个新的多项式算法，解决了统一模单侧分配的决策问题。一个结构，采用字符串压缩，是用来实现的多项式界。最后，我们研究了新的非对称统一范式中的单边分配问题。我们给出了单侧分配性的第一个非对称统一算法。
英文摘要：
An algorithm for unification modulo one-sided distributivity is an early result by Tidén 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
