Insecurity problem for assertions remains in NP

TL;DR

This paper proves that the insecurity problem for cryptographic protocols involving logical formulas, including equality and existential quantification, remains in NP, extending previous results to more complex protocol models.

Contribution

The paper extends the NP classification of the insecurity problem to protocols with logical statements, using typed equality proofs and techniques from prior work.

Findings

Insecurity problem remains in NP for protocols with logical formulas.

Typed equality proofs help manage unbounded witnesses.

Applicable to protocols with equality and existential quantification.

Abstract

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).