Paper Info
Title
Intruder deduction problem for locally stable theories with normal forms and inverses.
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.
Year
DOI
Venue
2017
10.1016/j.tcs.2017.01.027
Theoretical Computer Science
Keywords
Field
DocType
Intruder deduction problem,Associativity and commutativity,Locally stable theories,Term rewrite systems,AC-matching
Abelian group,Discrete mathematics,Combinatorics,Associative property,Algebra,Commutative property,Operator (computer programming),Modular design,Time complexity,Saturated set,Exponentiation,Mathematics
Journal
Volume
ISSN
Citations 
672
0304-3975
0
PageRank 
References 
Authors
0.34
15
3
Name
Order
Citations
PageRank
M. Ayala-Rincón1105.38
Maribel Fernández231523.44
Daniele Nantes Sobrinho323.08