Solving the insecurity problem for assertions
R Ramanujam, Vaishnavi Sundararajan, S P Suresh
TL;DR
This work tackles the insecurity problem for protocols that use assertions, including equality and existential quantification, in finitely many sessions. It extends the RT03 approach to handle two sources of unboundedness—intruder substitutions and existential witnesses—and their interaction, to obtain a polynomial-bounded analysis. The authors prove that the insecurity problem for assertions with finitely many sessions remains in NP, enabling a feasible decision procedure for verifying confidentiality properties in assertion-enabled protocols. This advances formal verification of cryptographic protocols by enabling efficient analysis of certificates and partial-information assertions.
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 & 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.