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.

翻译：我们引入了一种新形式的受限项重写系统——图嵌入项重写系统。这类系统（其名称亦源于此）受图子式关系启发，是项重写系统中著名的同胚嵌入性质的更灵活扩展。作为激励性应用领域，我们考虑安全协议的符号分析，更精确地说，是由推导问题和静态等价问题定义的两个知识问题。在该领域中，受限项重写系统（例如子项收敛系统）已被证明是有用的，因为此类系统的知识问题是可判定的。许多相同的决策程序对于"超越子项收敛"的系统实例仍然有效。然而，这些决策程序对这类实例的适用性通常需要逐个证明。这是因为它们不符合现有已知可适用这些程序的语法定义。本文证明，许多此类系统属于图嵌入收敛系统的一个特定子类，称为收缩收敛系统。一方面，我们证明收缩收敛系统子类的知识问题是可判定的。另一方面，我们证明图嵌入系统类的知识问题是不可判定的。进一步地，我们将这些图嵌入系统与协议分析文献中已知的若干概念和性质进行比较和对比。最后，我们提供了多个组合结果，既包括多个收缩收敛系统的组合，也包括收缩收敛系统与特定置换等式理论的组合。