International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Computationally sound implementations of equational theories against passive adversaries

Authors:
Mathieu Baudet
Veronique Cortier
Steve Kremer
Download:
URL: http://eprint.iacr.org/2005/074
Search ePrint
Search Google
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.
BibTeX
@misc{eprint-2005-12411,
  title={Computationally sound implementations of equational theories against passive adversaries},
  booktitle={IACR Eprint archive},
  keywords={foundations / cryptographic protocols, computational soundness of formal methods, static equivalence, equational theories},
  url={http://eprint.iacr.org/2005/074},
  note={ baudet@lsv.ens-cachan.fr 12846 received 4 Mar 2005},
  author={Mathieu Baudet and Veronique Cortier and Steve Kremer},
  year=2005
}