Deciding knowledge in security protocols under equational theories

Deciding knowledge in security protocols under equational theories. M. Abadi and V. Cortier. In Proceedings of the 31st Int. Coll. Automata, Languages, and Programming (ICALP'2004), pp. 46–58, Lecture Notes in Computer Science 3142, Springer, Turku, Finland, July 2004.

Download

[PDF] [PS] [HTML]

Abstract

The analysis of security protocols requires precise formulations of the knowledge of protocol participants and attackers. In formal approaches, this knowledge is often treated in terms of message deducibility and indistinguishability relations. In this paper we study the decidability of these two relations. The messages in question may employ functions (encryption, decryption, etc.) axiomatized in an equational theory. Our main positive results say that, for a large and useful class of equational theories, deducibility and indistinguishability are both decidable in polynomial time.

BibTeX

@inproceedings{AC04Icalp,
   author = "M. Abadi and V. Cortier",
   title = "Deciding knowledge in security protocols
under  equational theories",
   booktitle = "Proceedings of the 31st Int. Coll. Automata, Languages, and Programming (ICALP'2004)",
   month = {July},
   volume = "3142",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "46-58",
   address = 	 {Turku, Finland},
   year = "2004",
  abstract = {The analysis of security protocols requires precise formulations of the knowledge of protocol participants and attackers. In formal approaches, this knowledge is often treated in terms of message deducibility and indistinguishability relations. In this paper we study the decidability of these two relations. The messages in question may employ functions (encryption, decryption, etc.) axiomatized in an equational theory. Our main positive results say that, for a large and useful class of equational theories, deducibility and indistinguishability are both decidable in polynomial time.},
  doi =           {10.1007/978-3-540-27836-8_7},
}