Steve Kremer: 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. Computationally Sound Implementations of Equational Theories against Passive Adversaries. In Proceedings of the 32nd International Colloquium on Automata, Languages and Programming (ICALP'05), pp. 652–663, Lecture Notes in Computer Science 3580, Springer, Lisboa, Portugal, July 2005.
doi:10.1007/11523468_53

Download

[PDF] [PDF (long version)] [PS (long version)] [HTML]

Abstract

In this paper we study the link between formal and cryptographic models for security protocols in the presence of a passive adversary. In contrast to other works, we do not consider a fixed set of primitives but aim at results for an arbitrary equational theory. We define a framework for comparing a cryptographic implementation and its idealization w.r.t. various security notions. In particular, we concentrate on the computationnal 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, we establish new soundness results for the Exclusive Or, as well as a theory of ciphers and lists.

BibTeX

@inproceedings{BCK-ICALP2005,
  abstract =      {In this paper we study the link between formal and
                   cryptographic models for security protocols in the
                   presence of a passive adversary. In contrast to other
                   works, we do not consider a fixed set of primitives
                   but aim at results for an arbitrary equational
                   theory. We define a framework for comparing a
                   cryptographic implementation and its idealization
                   w.r.t.\ various security notions. In particular, we
                   concentrate on the computationnal 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, we establish new soundness
                   results for the Exclusive Or, as well as a theory of
                   ciphers and lists.},
  address =       {Lisboa, Portugal},
  author =        {Baudet, Mathieu and Cortier, V{\'e}ronique and
                   Kremer, Steve},
  booktitle =     {{P}roceedings of the 32nd {I}nternational
                   {C}olloquium on {A}utomata, {L}anguages and
                   {P}rogramming ({ICALP}'05)},
  DOI =           {10.1007/11523468_53},
  editor =        {Caires, Lu{\'\i}s and Italiano, Giuseppe F. and
                   Monteiro, Lu{\'\i}s and Palamidessi, Catuscia and
                   Yung, Moti},
  month =         jul,
  pages =         {652-663},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Computationally Sound Implementations of Equational
                   Theories against Passive Adversaries},
  volume =        {3580},
  year =          {2005},
  acronym =       {{ICALP}'05},
  nmonth =        {7},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BCK-icalp05.pdf},
}