Combining algorithms for deciding knowledge in security protocols

Combining algorithms for deciding knowledge in security protocols. Mathilde Arnaud, Véronique Cortier, and Stéphanie Delaune. In Proceedings of the 6th International Symposium on Frontiers of Combining Systems (FroCoS'07), pp. 103–117, Lecture Notes in Artificial Intelligence 4720, Springer, Liverpool, UK, September 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. Those notions are well-studied and a lot of decidability results already exist to deal with a variety of equational theories.
We show that decidability results can be easily combined for any disjoint equational theories: if the deducibility and indistinguishability relations are decidable for two disjoint theories, they are also decidable for their union. As an application, new decidability results can be obtained using this combination theorem.

BibTeX

@inproceedings{ACD-frocos07,
  address =       {Liverpool, UK},
  author =        {Arnaud, Mathilde and Cortier, V{\'e}ronique and
                   Delaune, St{\'e}phanie},
  booktitle =     {{P}roceedings of the 6th {I}nternational {S}ymposium
                   on {F}rontiers of {C}ombining {S}ystems
                   ({FroCoS}'07)},
  editor =        {Wolter, Franck},
  month =         sep,
  pages =         {103-117},
  publisher =     {Springer},
  series =        {Lecture Notes in Artificial Intelligence},
  title =         {Combining algorithms for deciding knowledge in
                   security protocols},
  volume =        {4720},
  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. Those notions
                   are well-studied and a lot of decidability results
                   already exist to deal with a variety of equational
                   theories.\par We~show that decidability results can
                   be easily combined for any disjoint equational
                   theories: if the deducibility and
                   indistinguishability relations are decidable for two
                   disjoint theories, they are also decidable for their
                   union. As~an application, new decidability results
                   can be obtained using this combination theorem.},
  doi =           {10.1007/978-3-540-74621-8_7},
}