Dolev-Yao Theory with Associative Blindpair Operators

In the context of modeling cryptographic tools like blind signatures and homomorphic encryption, the Dolev-Yao model is typically extended with an operator over which encryption is distributive. The intruder deduction problem has a non-elementary upper bound when the extended operator is an Abelian group operator. Here we show that the intruder deduction problem is DEXPTIME-complete when we restrict the operator to satisfy only the associative property. We propose an automata-based analysis for the upper bound and use the reachability problem for alternating pushdown systems to show the lower bound.