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 and Turuani (2003) show that, when considering finitely many sessions and a protocol model where only terms are communicated, 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 formulas, the analysis of the insecurity problem becomes tricky. In this paper we consider the insecurity problem for protocols with logical statements that include equality on terms and existential quantification. Witnesses for existential quantifiers may be of unbounded size, and obtaining small witnesses while maintaining equality proofs complicates the analysis. We use a notion of "typed" equality proofs, and extend techniques from [RT03] to show that this problem is also in NP. We also show that these techniques can be used to analyze the insecurity problem for systems such as the one proposed in Ramanujam, Sundararajan and Suresh (2017).

翻译：在密码协议符号验证中，核心问题之一是判断协议是否存在一次执行，使恶意入侵者获取指定秘密。Rusinowitch与Turuani（2003）的研究表明，在考虑有限会话次数且协议模型仅涉及项通信时，该"非安全性问题"是NP完备的。其证明策略的关键在于观察到：任何协议执行均可通过入侵者仅通信有界长度项的模拟来复现。然而，当考虑可同时通信逻辑公式与项的模型时，非安全性问题的分析变得复杂。本文针对包含项等词及存在量词的逻辑语句的协议，研究非安全性问题。存在量词见证元可能具有无界大小，而在保持等式证明的前提下获取小规模见证元使分析复杂化。我们采用"类型化"等词证明概念，并扩展[RT03]的技术，证明该问题仍在NP中。同时表明这些技术可用于分析Ramanujam、Sundararajan与Suresh（2017）所提系统等模型中的非安全性问题。