In the symbolic verification of cryptographic protocols, a central problem is deciding whether a protocol admits an execution which leaks a designated secret to the malicious intruder. Rusinowitch & Turuani (2003) show that, when considering finitely many sessions, this ``insecurity problem'' is NP-complete. Central to their proof strategy is the observation that any execution of a protocol can be simulated by one where the intruder only communicates terms of bounded size. However, when we consider models where, in addition to terms, one can also communicate logical statements about terms, the analysis of the insecurity problem becomes tricky when both these inference systems are considered together. In this paper we consider the insecurity problem for protocols with logical statements that include {\em equality on terms} and {\em existential quantification}. Witnesses for existential quantifiers may be unbounded, and obtaining small witness terms while maintaining equality proofs complicates the analysis considerably. We extend techniques from Rusinowitch & Turuani (2003) to show that this problem is also in NP.

翻译：在密码协议的形式化验证中，一个核心问题在于判断协议是否存在某次执行过程，使得恶意入侵者能够获取指定的机密信息。Rusinowitch与Turuani（2003）的研究表明，在考虑有限会话次数的情形下，这种"不安全性问题"属于NP完全问题。其证明策略的关键在于观察到：任何协议的执行过程都可以被模拟为一种入侵者仅传递有界规模项的执行方式。然而，当模型允许在项之外同时传递关于项的逻辑陈述时，这两个推理系统的共存使得不安全性问题的分析变得棘手。本文研究了包含项等式与存在量化的逻辑陈述的协议不安全性问题。存在量词的见证项可能无界，在维护等式证明的同时获取小型见证项会显著增加分析复杂度。我们扩展了Rusinowitch与Turuani（2003）的技术，证明该问题同样属于NP问题。