Paper 2005/074

Computationally sound implementations of equational theories against passive adversaries

Mathieu Baudet, Vëronique Cortier, and Steve Kremer

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 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, we establish new soundness results for the Exclusive Or, as well as a theory of ciphers and lists.

Metadata
Available format(s)
PDF PS
Category
Foundations
Publication info
Published elsewhere. preprint submitted to Elsevier
Keywords
cryptographic protocolscomputational soundness of formal methodsstatic equivalenceequational theories
Contact author(s)
baudet @ lsv ens-cachan fr
History
2008-12-30: revised
2005-03-08: received
See all versions
Short URL
https://ia.cr/2005/074
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2005/074,
      author = {Mathieu Baudet and Vëronique Cortier and Steve Kremer},
      title = {Computationally sound implementations of equational theories against passive adversaries},
      howpublished = {Cryptology ePrint Archive, Paper 2005/074},
      year = {2005},
      note = {\url{https://eprint.iacr.org/2005/074}},
      url = {https://eprint.iacr.org/2005/074}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.