## 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.

### 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}}
}