International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

A general framework for computational soundness proofs - or - The computational soundness of the applied pi-calculus

Authors:
Michael Backes
Dennis Hofheinz
Dominique Unruh
Download:
URL: http://eprint.iacr.org/2009/080
Search ePrint
Search Google
Abstract: We provide a general framework for conducting computational soundness proofs of symbolic models. Our framework considers arbitrary sets of constructors, deduction rules, and computational implementations, and it abstracts away from many details that are not core for proving computational soundness such as message scheduling, corruption models, and even the internal structure of a protocol. We identify several properties of a so-called simulator such that the existence of a simulator with all these properties already entails computational soundness in the sense of preservation of trace properties in our framework. This simulator-based characterization allows for proving soundness results in a conceptually modular and generic way. We exemplify the usefulness of our framework by proving the first computational soundness result for the full-fledged applied $\pi$-calculus under active attacks. Concretely, we embed the applied $\pi$-calculus into our framework and give a sound implementation of public-key encryption.
BibTeX
@misc{eprint-2009-18192,
  title={A general framework for computational soundness proofs - or - The computational soundness of the applied pi-calculus},
  booktitle={IACR Eprint archive},
  keywords={foundations / computational soundness, applied pi-calculus},
  url={http://eprint.iacr.org/2009/080},
  note={ backes@mpi-sws.mpg.de 14291 received 16 Feb 2009},
  author={Michael Backes and Dennis Hofheinz and Dominique Unruh},
  year=2009
}