Decidability and combination results for two notions of knowledge in security protocols

Decidability and combination results for two notions of knowledge in security protocols. Véronique Cortier and Stéphanie Delaune. Journal of Automated Reasoning, 48, Springer, 2012.

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 considered: deducibility and indistinguishability. Those notions are well-studied and several decidability results already exist to deal with a variety of equational theories. Most of the existing results are dedicated to specific equational theories and only few results, especially in the case of indistinguishability, have been obtained for equational theories with associative and commutative properties (AC).
In this paper, we show that existing 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. We also propose a general setting for solving deducibility and indistinguishability for an important class (called monoidal) of equational theories involving AC operators.
As a consequence of these two results, new decidability and complexity results can be obtained for many relevant equational theories.

BibTeX

@article{Combinaison-Eq-journal,
  author =        {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
  journal =       {Journal of Automated Reasoning},
  publisher =     {Springer},
  title =         {Decidability and combination results for two notions
                   of knowledge in security protocols},
  year =          {2012},
  volume = {48},
  issue = {8},
  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
                   considered: deducibility and indistinguishability.
                   Those notions are well-studied and several
                   decidability results already exist to deal with a
                   variety of equational theories. Most of the existing
                   results are dedicated to specific equational theories
                   and only few results, especially in the case of
                   indistinguishability, have been obtained for
                   equational theories with associative and commutative
                   properties~(AC).\par In this paper, we show that
                   existing 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. We also propose a general
                   setting for solving deducibility and
                   indistinguishability for an important class (called
                   \emph{monoidal}) of equational theories involving AC
                   operators.\par As a consequence of these two results,
                   new decidability and complexity results can be
                   obtained for many relevant equational theories.},
  doi =           {10.1007/s10817-010-9208-8},
}