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完全类。