Deciding knowledge in security protocols under equational theories

Deciding knowledge in security protocols under equational theories. Martin Abadi and Véronique Cortier. Theoretical Computer Science, 387(1-2):2–32, November 2006. Top cited article 2005-2010 TCS paper award.

Download

[PDF] [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

@Article{AbadiCortierTCS06,
  author = 	 {Martin Abadi and V\'eronique Cortier},
  title = 	 {Deciding knowledge in security protocols under equational theories},
  journal = 	 {Theoretical Computer Science},
  year = 	 {2006},
  volume = 	 {387},
  number = 	 {1-2},
  pages = 	 {2-32},
  month = 	 {November},
  DOI = {10.1007/978-3-540-27836-8_7},
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.},
note = {{\bf Top cited article 2005-2010 TCS paper award}}
}