Intruder deduction problem for locally stable theories with normal forms and inverses

We present an algorithm to decide the intruder deduction problem (IDP) for a class of equational theories that include associative and commutative (AC) operators. The algorithm is based on the analysis of reductions in the head of terms built from normal contexts using the initial knowledge of the intruder. It relies on a new and efficient algorithm to solve a restricted case of higher-order AC-matching. For the subclass of theories for which AC operators have inverses, our algorithm runs in polynomial time on the size of a saturated set built from the initial knowledge of the intruder. To illustrate, we apply the results to Pure AC theories, Abelian Groups, Abelian Groups extended with exponentiation, and XOR. Although specific algorithms have already been defined to deal with each of these theories, we provide a modular approach that can deal with all of them in a uniform way.