Deciding knowledge in security protocols under (many more) equational theories

In the analysis of security protocols, the knowledge of at-tackers is often described in terms of message deducibility and indistinguishability relations. In this paper, we pursue the study of of these two relations. We establish general de-cidability theorems for both. These theorems require only loose, abstract conditions on the equational theory for mes-sages. They subsume previous results for a syntactically de-fined class of theories that allows basic equations for func-tions such as encryption, decryption, and digital signatures. They also apply to many other useful theories, for exam-ple with blind digital signatures, homomorphic encryption, XOR, and other associative-commutative functions.