2026/08/04 by Raja Oktovin O. P. Damanik, Alwen Tiu
Computer Science · #cs.LO #cs.CR #cs.FL #msc:68Q42 #msc:68Q60 #msc:68M25 #acm:68Q42 #acm:68Q60 #acm:68M25
26 pages, 1 figure (Tikz generated), submitted to CSL 2027
arxiv created 2026/08/04 · arxiv updated 2026/08/05
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 ≡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.