-
Knowledge Problems in Protocol Analysis: Extending the Notion of Subterm Convergent
Authors:
Carter Bunch,
Saraid Dwyer Satterfield,
Serdar Erbatur,
Andrew M. Marshall,
Christophe Ringeissen
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 k…
▽ More
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.
△ Less
Submitted 30 January, 2024;
originally announced January 2024.
-
Politeness and Stable Infiniteness: Stronger Together
Authors:
Ying Sheng,
Yoni Zohar,
Christophe Ringeissen,
Andrew Reynolds,
Clark Barrett,
Cesare Tinelli
Abstract:
We make two contributions to the study of polite combination in satisfiability modulo theories.
The first contribution is a separation between politeness and strong politeness, by presenting a polite theory that is not strongly polite. This result shows that proving strong politeness
(which is often harder than proving politeness) is sometimes needed in order to use polite combination.
The s…
▽ More
We make two contributions to the study of polite combination in satisfiability modulo theories.
The first contribution is a separation between politeness and strong politeness, by presenting a polite theory that is not strongly polite. This result shows that proving strong politeness
(which is often harder than proving politeness) is sometimes needed in order to use polite combination.
The second contribution is an optimization to the polite combination method, obtained by borrowing from the Nelson-Oppen method. In its non-deterministic form, the Nelson-Oppen method is based on guessing arrangements over shared variables. In contrast, polite combination requires an arrangement over \emph{all} variables of the shared sort (not just the shared variables). We show that when using polite combination, if the other theory is stably infinite with respect to a shared sort, only the shared variables of that sort need be considered in arrangements, as in the Nelson-Oppen method.
Reasoning about arrangements of variables is exponential in the worst case, so reducing the number of variables that are considered has the potential to improve performance significantly.
We show preliminary evidence for this in practice by demonstrating a speed-up on a smart contract verification benchmark.
△ Less
Submitted 27 April, 2021; v1 submitted 23 April, 2021;
originally announced April 2021.
-
Politeness for the Theory of Algebraic Datatypes
Authors:
Ying Sheng,
Yoni Zohar,
Christophe Ringeissen,
Jane Lange,
Pascal Fontaine,
Clark Barrett
Abstract:
Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly…
▽ More
Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing also how it can be combined with other arbitrary disjoint theories using polite combination. Our results cover both inductive and finite datatypes, as well as their union. The combination method uses a new, simple, and natural notion of additivity, that enables deducing strong politeness from (weak) politeness.
△ Less
Submitted 14 April, 2020; v1 submitted 9 April, 2020;
originally announced April 2020.
