一句话：提出图嵌入项重写系统及收缩收敛子类，证明后者的协议知识问题可判定、前者不可判定，并给出组合结果。
本文研究安全协议符号分析中的两个知识问题：演绎问题与静态等价问题。已有工作表明，子项收敛等受限项重写系统可保证可判定性，但许多“超出子项收敛”的系统虽可由现有过程处理，却需逐个证明适用性。作者受图子式关系启发，提出图嵌入项重写系统，作为同胚嵌入性质的更灵活扩展。关键结果是：在图嵌入收敛系统中识别出收缩收敛子类，并证明该子类的知识问题可判定；相反，一般图嵌入系统的知识问题不可判定。文中还将图嵌入系统与协议分析文献中的已知概念和性质进行比较，并给出组合结果，包括多个收缩收敛系统之间及其与特定置换等式理论的组合。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2401-17226,
title = {Knowledge Problems in Protocol Analysis: Extending the Notion of Subterm Convergent},
author = {Carter Bunch and Saraid Dwyer Satterfield and Serdar Erbatur and Andrew M. Marshall and Christophe Ringeissen},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 2},
year = {2026},
doi = {10.46298/lmcs-22(2:15)2026}
}