一种用于通用符号协议分析的、结合不可约性与 SMT 约束的高效典范窄化实现
An Efficient Canonical Narrowing Implementation with Irreducibility and SMT Constraints for Generic Symbolic Protocol Analysis
AI总结：
本文实现并扩展一种高效典范窄化算法，使其支持带 SMT 条件约束的条件重写理论，从而增强通用符号密码协议分析能力。
摘要：
窄化与合一对于重写理论的符号分析是非常有用的工具，因此也适用于任何可以用这种方式指定的模型。其应用的一个非常明确的例子是形式化密码协议分析领域，这正是 Maude-NPA、Tamarin 和 Akiss 等工具使用窄化与合一的原因。在本工作中，我们提出一种典范窄化算法的实现，该算法改进了标准窄化算法，并经过扩展，能够处理带条件规则的重写理论。规则条件将包含 SMT 约束，这些约束会在算法整个执行过程中被携带，以判定各个解是否关联可满足或不可满足约束；在后一种情况下，则将这些解丢弃。
英文摘要：
Narrowing and unification are very useful tools for symbolic analysis of rewrite theories, and thus for any model that can be specified in that way. A very clear example of their application is the field of formal cryptographic protocol analysis, which is why narrowing and unification are used in tools such as Maude-NPA, Tamarin and Akiss. In this work we present the implementation of a canonical narrowing algorithm, which improves the standard narrowing algorithm, extended to be able to process rewrite theories with conditional rules. The conditions of the rules will contain SMT constraints, which will be carried throughout the execution of the algorithm to determine if the solutions have associated satisfiable or unsatisfiable constraints, and in the latter case, discard them.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
