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

Deciding knowledge in security protocols under (many more) equational theories. M. Abadi and V. Cortier. In Proc. 18th IEEE Computer Security Foundations Workshop (CSFW'05), pp. 62–76, IEEE Comp. Soc. Press, Aix-en-Provence, France, June 2005.

Download

[PDF] [PS] [HTML]

Abstract

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

BibTeX

@InProceedings{CortierCSFW05,
  author = 	 {M. Abadi and V. Cortier},
  title = 	 {Deciding knowledge in security protocols under (many more) equational theories},
  booktitle = {Proc. 18th IEEE Computer Security Foundations Workshop (CSFW'05)},
  pages = 	 {62-76},
  year = 	 {2005},
  address = 	 {Aix-en-Provence, France},
  month = 	 {June},
  publisher = {IEEE Comp. Soc. Press},
  abstract = {In the analysis of security protocols, the knowledge of attackers is often described in terms of message deducibility and indistinguishability relations. In this paper, we pursue the study of these two relations. We establish general decidability theorems for both. These theorems require only loose, abstract conditions on the equational theory for messages. They subsume previous results for a syntacticallydefined class of theories that allows basic equations for functions such as encryption, decryption, and digital signatures. They also apply to many other useful theories, for example with blind digital signatures, homomorphic encryption, XOR, and other associative-commutative functions.},
  doi =           {10.1109/CSFW.2005.14},
}