用XOR实现协议分析的统一算法
Implementing a Unification Algorithm for Protocol Analysis with XOR
摘要：
在本文中，我们提出了一个统一算法的理论$E$结合统一算法$E\_{\std}$和$E\_{\ACUN}$（ACUN属性，如XOR），但相比更一般的组合方法使用的具体属性的方程理论进一步优化。我们的优化大大减少了非确定性选择的数量，特别是那些变量识别和线性排序。这对于减少统一算法的运行时间和统一器的完整集合中的统一器的数量都是重要的。我们强调，获得一个“小”的统一集是必不可少的约束求解过程中使用的统一算法的效率。该方法已在安全协议分析工具CL-Atse中实现。
英文摘要：
In this paper, we propose a unification algorithm for the theory $E$ which combines unification algorithms for $E\_{\std}$ and $E\_{\ACUN}$ (ACUN properties, like XOR) but compared to the more general combination methods uses specific properties of the equational theories for further optimizations. Our optimizations drastically reduce the number of non-deterministic choices, in particular those for variable identification and linear orderings. This is important for reducing both the runtime of the unification algorithm and the number of unifiers in the complete set of unifiers. We emphasize that obtaining a ``small'' set of unifiers is essential for the efficiency of the constraint solving procedure within which the unification algorithm is used. The method is implemented in the CL-Atse tool for security protocol analysis.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
