Computationally Sound Implementations of Equational Theories against Passive Adversaries

Computationally Sound Implementations of Equational Theories against Passive Adversaries. Mathieu Baudet, Véronique Cortier, and Steve Kremer. Information and Computation, 207(4):496–520, Elsevier Science Publishers, April 2009.

Download

[PDF] [HTML]

Abstract

In this paper we study the link between formal and cryptographic models for security protocols in the presence of passive adversaries. In contrast to other works, we do not consider a fixed set of primitives but aim at results for arbitrary equational theories. We define a framework for comparing a cryptographic implementation and its idealization with respect to various security notions. In particular, we concentrate on the computational soundness of static equivalence, a standard tool in cryptographic pi calculi. We present a soundness criterion, which for many theories is not only sufficient but also necessary. Finally, to illustrate our framework, we establish the soundness of static equivalence for the exclusive OR and a theory of ciphers and lists.

BibTeX

@article{BCK-IC09,
  author =        {Baudet, Mathieu and Cortier, V{\'e}ronique and
                   Kremer, Steve},
  journal =       {Information and Computation},
  month =         apr,
  number =        {4},
  pages =         {496-520},
  publisher =     {Elsevier Science Publishers},
  title =         {Computationally Sound Implementations of Equational
                   Theories against Passive Adversaries},
  volume =        {207},
  year =          {2009},
  abstract =      {In~this paper we study the link between formal and
                   cryptographic models for security protocols in the
                   presence of passive adversaries. In~contrast to other
                   works, we~do not consider a fixed set of primitives
                   but aim at results for arbitrary equational theories.
                   We~define a framework for comparing a cryptographic
                   implementation and its idealization with respect to
                   various security notions. In~particular, we
                   concentrate on the computational soundness of static
                   equivalence, a standard tool in cryptographic pi
                   calculi. We~present a soundness criterion, which for
                   many theories is not only sufficient but also
                   necessary. Finally, to~illustrate our framework,
                   we~establish the soundness of static equivalence for
                   the exclusive OR and a theory of ciphers and lists.},
  doi =           {10.1016/j.ic.2008.12.005},
}