Deciding Knowledge in Security Protocols for Monoidal Equational Theories

Deciding Knowledge in Security Protocols for Monoidal Equational Theories. Véronique Cortier and Stéphanie Delaune. In Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'07), pp. 196–210, Lecture Notes in Artificial Intelligence 4790, Springer, Yerevan, Armenia, October 2007.

Download

[PDF] [HTML]

Abstract

In formal approaches, messages sent over a network are usually modeled by terms together with an equational theory, axiomatizing the properties of the cryptographic functions (encryption, exclusive or, ...). The analysis of cryptographic protocols requires a precise understanding of the attacker knowledge. Two standard notions are usually used: deducibility and indistinguishability. Only few results have been obtained (in an ad-hoc way) for equational theories with associative and commutative properties, especially in the case of static equivalence. The main contribution of this paper is to propose a general setting for solving deducibility and indistinguishability for an important class (called monoidal) of these theories. Our setting relies on the correspondence between a monoidal theory \(E\) and a semiring \(S_E\) which allows us to give an algebraic characterization of the deducibility and indistinguishability problems. As a consequence we recover easily existing decidability results and obtain several new ones.

BibTeX

@inproceedings{CortierDelaune-LPAR07-monoidal,
  address =       {Yerevan, Armenia},
  author =        {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
  booktitle =     {{P}roceedings of the 14th {I}nternational
                   {C}onference on {L}ogic for {P}rogramming,
                   {A}rtificial {I}ntelligence, and {R}easoning
                   ({LPAR}'07)},
  editor =        {Dershowitz, Nachum and Voronkov, Andrei},
  month =         oct,
  pages =         {196-210},
  publisher =     {Springer},
  series =        {Lecture Notes in Artificial Intelligence},
  title =         {Deciding Knowledge in Security Protocols for Monoidal
                   Equational Theories},
  volume =        {4790},
  year =          {2007},
  abstract =      {In formal approaches, messages sent over a network
                   are usually modeled by terms together with an
                   equational theory, axiomatizing the properties of the
                   cryptographic functions (encryption, exclusive
                   or,~...). The~analysis of cryptographic protocols
                   requires a precise understanding of the attacker
                   knowledge. Two standard notions are usually used:
                   deducibility and indistinguishability. Only few
                   results have been obtained (in~an ad-hoc~way) for
                   equational theories with associative and commutative
                   properties, especially in the case of static
                   equivalence. The~main contribution of this paper is
                   to propose a general setting for solving deducibility
                   and indistinguishability for an important class
                   (called monoidal) of these theories. Our~setting
                   relies on the correspondence between a monoidal
                   theory~{\(E\)} and a semiring~{\(S_E\)} which allows
                   us to give an algebraic characterization of the
                   deducibility and indistinguishability problems. As~a
                   consequence we recover easily existing decidability
                   results and obtain several new ones.},
  doi =           {10.1007/978-3-540-75560-9_16},
}