Deciding knowledge in security protocols under equational theories

Deciding knowledge in security protocols under equational theories. Martin Abadi and Véronique Cortier. Rapport de recherche RR-5169, INRIA, 2004.

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

@techreport{ABADI:2004:INRIA-00071420:1,
    hal_id = {inria-00071420},
    title = {{Deciding knowledge in security protocols under equational theories}},
    author = {Abadi, Martin and Cortier, V{\'e}ronique},
    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.}},
    keywords = {decision; knowledge; cryptographic protocols; deduction; equivalence},
    language = {Anglais},
    affiliation = {CASSIS - INRIA Lorraine - LORIA / LIFC},
    pages = {22},
    type = {Rapport de recherche},
    institution = {INRIA},
    number = {RR-5169},
    year = {2004},
}