D. Dolev and A. C. Yao [IEEE Trans. Inf. Theory IT-29, 198- 208 (1983; Zbl 0502.94005)] developed formal models of two-party protocols. Here the sets of cancellation rules underlying their models are shown to be finite homogeneous Thue systems of degree 2 that are Church-Rosser. Now the question of whether or not a given protocol is secure in the sense of Dolev and Yao can be stated as a special case of the following extended word problem: Instance: Two regular sets R and F on \(\Sigma\). Question: Does there exist \(\alpha\in R\) and \(\beta\in F\) such that \(\alpha\) is reducible to \(\beta\) ?
Conceptually simple polynomial-time algorithms are given for the above problem and for the following decision problem: Instance: Two regular sets R and F on \(\Sigma\). Question: Does there exist \(\alpha\in R\) and \(\beta\in F\) such that \(\alpha\) is congruent to \(\beta\) ?
These algorithms are based on a construction that given a nondeterministic finite state acceptor A with m states yields in \(O(m^ 4)\) steps a nondeterministic finite state acceptor with m states, that recognizes the set of descendants of L(A) modulo a given finite homogeneous Thue system of degree 2. All these results can be extended to finite monadic Thue systems, however, the complexity bounds then depend on the maximum length of the left-hand sides of the rules of the Thue system under consideration.