@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@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.},
}
