Computing knowledge in security protocols under convergent equational theories

Abstract

In the symbolic analysis of security protocols, two classical notions of knowledge, deducibility and indistinguishability, yield corresponding decision problems. We propose a procedure for both problems under arbitrary convergent equational theories. Our procedure terminates on a wide range of equational theories. In particular, we obtain a new decidability result for a theory we encountered when studying electronic voting protocols. We also provide a prototype implementation. © 2009 Springer Berlin Heidelberg.