Solving the Insecurity Problem for Assertions

Ramanujam, R. and Sundararajan, Vaishnavi and Suresh, S P (2024) Solving the Insecurity Problem for Assertions. In: 2024 IEEE 37th Computer Security Foundations Symposium (CSF), 08-12 July 2024, Enschede, Netherlands.

Text Restricted to Registered users only Download (746kB)

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. In [1], it is shown 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 equality on terms and 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 [1] to show that this problem is also in NP.

Item Type:	Conference or Workshop Item (Paper)
Authors:	Ramanujam, R. and Sundararajan, Vaishnavi and Suresh, S P
Document Language:	Language English
Subjects:	Computer science, information & general works Azim Premji Foundation Structure > Azim Premji University - Bengaluru > Computer science, information & general works Natural Sciences > Mathematics Technology
Divisions:	Azim Premji University - Bengaluru > School of Arts and Sciences
Full Text Status:	Restricted
URI:	http://publications.azimpremjiuniversity.edu.in/id/eprint/6965
Publisher URL:	https://doi.org/10.1109/CSF61375.2024.00008

Actions (login required)

View Item