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.

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