Knowledge Problems in Protocol Analysis: Extending the Notion of Subterm Convergent
Carter Bunch, Saraid Dwyer Satterfield, Serdar Erbatur, Andrew M. Marshall, Christophe Ringeissen
TL;DR
The paper addresses decidability of knowledge problems in symbolic security protocol analysis when the underlying equational theory extends beyond subterm convergent TRSs. It introduces graph-embedded TRS, with a contracting convergent subclass that yields decidability via a local-stability and finite saturation framework, while the general graph-embedded convergent class remains undecidable. It relates these notions to the cap problem, finite variant property, and layered convergent property, and provides modular combination results for unions of contracting TRSs and permutative theories. The results offer a graph-informed, syntactic framework that broadens the applicability of existing decision procedures for protocol analysis and supports modular reasoning across theories.
Abstract
We introduce a new form of restricted term rewrite system, the graph-embedded term rewrite system. These systems, and thus the name, are inspired by the graph minor relation and are more flexible extensions of the well-known homeomorphic-embedded property of term rewrite systems. As a motivating application area, we consider the symbolic analysis of security protocols, and more precisely the two knowledge problems defined by the deduction problem and the static equivalence problem. In this field restricted term rewrite systems, such as subterm convergent ones, have proven useful since the knowledge problems are decidable for such systems. Many of the same decision procedures still work for examples of systems which are "beyond subterm convergent". However, the applicability of the corresponding decision procedures to these examples must often be proven on an individual basis. This is due to the problem that they don't fit into an existing syntactic definition for which the procedures are known to work. Here we show that many of these systems belong to a particular subclass of graph-embedded convergent systems, called contracting convergent systems. On the one hand, we show that the knowledge problems are decidable for the subclass of contracting convergent systems. On the other hand, we show that the knowledge problems are undecidable for the class of graph-embedded systems. Going further, we compare and contrast these graph embedded systems with several notions and properties already known in the protocol analysis literature. Finally, we provide several combination results, both for the combination of multiple contracting convergent systems, and then for the combination of contracting convergent systems with particular permutative equational theories.