平坦子句和单变量子句：单盲随机数密码协议的复杂性
Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying
摘要：
Comon和Cortier使用一阶子句的新类$\mathcal C$定义并建模了具有单盲复制的密码协议。他们在3-DEXPTIME中证明了它的可满足性问题。我们改进了这一结果表明，满足这个类是NEXPTIME完全的，使用新的分辨率技术。我们证明了满足是DEXPTIME完整的，如果条款是霍恩，这是所需的建模加密协议。虽然翻译霍恩条款只给出了一个DEXPTIME上界的保密问题，这些协议，我们进一步表明，这个保密问题实际上是DEXPTIME完全的。
英文摘要：
Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class $\mathcal C$ of first order clauses. They showed its satisfiability problem to be in 3-DEXPTIME. We improve this result by showing that satisfiability for this class is NEXPTIME-complete, using new resolution techniques. We show satisfiability to be DEXPTIME-complete if clauses are Horn, which is what is required for modeling cryptographic protocols. While translation to Horn clauses only gives a DEXPTIME upper bound for the secrecy problem for these protocols, we further show that this secrecy problem is actually DEXPTIME-complete.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
