Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper explores the intruder deduction problem in symbolic security-protocol analysis by reframing it as a right-divisibility issue within semi-Thue systems, specifically when all function symbols are unary. The authors establish new decidability results for convergent prefix-erasing and suffix-erasing systems, while also demonstrating that deduction remains undecidable for more complex systems involving simultaneous variable lifting. This work highlights both the advancements in understanding decidable fragments and the inherent limitations when extending these results to richer equational theories.
Right-divisibility in semi-Thue systems reveals new decidability results while exposing the limits of extending these findings to more complex equational theories.
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.