Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4952159 | Theoretical Computer Science | 2017 | 37 Pages |
Abstract
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Mauricio Ayala-Rincón, Maribel Fernández, Daniele Nantes-Sobrinho,