In the context of modelling cryptographic tools like blind signatures and homomorphic encryption, the DolevYao model is typically extended with an operator over which encryption is distributive. We consider one such theory which lacks any obvious locality property and show that its derivability problem is hard: in fact, it is dexptime-complete. e result holds also when blind pairing is associative. e lower bound contrasts with ptime decidability for restricted theories of blind signatures, and the upper bound with non-elementary decidability for abelian group operators with distributive encryption.
Anguraj Baskar, Ramaswamy Ramanujam, S. P. Suresh