Computing Knowledge in Security Protocols under Convergent Equational Theories

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.

• Type: Conference
• Year: 2009
• Where: CADE
• Authors: Stéphanie Delaune, Stefan Ciobâca, Steve Kremer
• Keywords: Automated Reasoning, CADE 2009, Convergent Equational Theories, Electronic Voting Protocols, Yield Corresponding Decision