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 Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA'07), pp. 63–80, Wrocław, Poland, July 2007.

Download

[PDF]

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 \(SE\) 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{CD-arspa07,
  address =       {Wroc{\l}aw, Poland},
  author =        {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
  booktitle =     {{P}roceedings of the {J}oint {W}orkshop on
                   {F}oundations of {C}omputer {S}ecurity and
                   {A}utomated {R}easoning for {S}ecurity {P}rotocol
                   {A}nalysis ({FCS-ARSPA}'07)},
  editor =        {Degano, Pierpaolo and K{\"u}sters, Ralf and
                   Vigan{\`o}, Luca and Zdancewic, Steve},
  month =         jul,
  pages =         {63-80},
  title =         {Deciding knowledge in security protocols for monoidal
                   equational theories},
  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~\(SE\) 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.},
}