AI 中文总结
本文从最小结构视角，将一元函数符号下的入侵者推导转化为半图厄系统的右可除性问题，证明了收敛前缀、后缀擦除系统的可判定性，同时发现收敛同步变量提升系统的推导不可判定，揭示了相关结果的推广潜力与局限。
AI 中文摘要
入侵者推导问题是符号安全协议分析的核心：它询问攻击者能否利用自身可用的（密码学）算子，从观测到的消息中推导出目标消息。尽管收敛重写系统提供了范式归约形式，但在收敛理论下的推导通常仍是不可判定的，且现有可判定片段往往由实际密码学实例塑造。本文从最小结构视角研究推导：当所有函数符号为一元时，项坍缩为字，推导成为半图厄系统的右可除性问题：给定字u和v，判断是否存在w使得wu ≡_S v。我们针对几类半图厄系统研究该问题，据我们所知，首次证明了收敛前缀擦除系统与收敛后缀擦除系统的新可判定性结果。随后将该视角扩展至规则在提升选定子项或变量时擦除上下文的项重写系统。尽管这些类暗示了超出一元设置的可判定推广可能，但我们证明，对于收敛的同步变量提升系统，推导已是不可判定的。这揭示了将右可除性结果推广至更丰富等式理论的潜力与局限。
英文摘要
The intruder deduction problem is central to symbolic security-protocol analysis: it asks whether an attacker can derive a target message from observed messages using (cryptographic) operators available to the attacker. Although convergent rewrite systems provide canonical normal forms, deduction modulo convergent theories remains undecidable in general, and existing decidable fragments are often shaped by practical cryptographic examples. In this paper, we study deduction from a minimal structural perspective. When all function symbols are unary, terms collapse to words and deduction becomes a right-divisibility problem for semi-Thue systems: given words $u$ and $v$ decide whether there exists $w$ such that $wu \equiv_S v$. We investigate this problem for several classes of semi-Thue systems and prove, to the best of our knowledge, new decidability results for convergent prefix-erasing and convergent suffix-erasing systems. We then extend this perspective to term rewriting systems whose rules erase contexts while lifting selected subterms or variables. Although these classes suggest possible decidable generalisations beyond the unary setting, we show that deduction is already undecidable for a convergent simultaneous variable-lifting system. This exposes both the potential and the limits of extending the right-divisibility results to richer equational theories.
Comments26 pages, 1 figure (Tikz generated), submitted to CSL 2027. Corrected author name; no changes to the content
