International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Paper: A Universally Composable Cryptographic Library

Authors:
Michael Backes
Birgit Pfitzmann
Michael Waidner
Download:
URL: http://eprint.iacr.org/2003/015
Search ePrint
Search Google
Abstract: Bridging the gap between formal methods and cryptography has recently received a lot of interest, i.e., investigating to what extent proofs of cryptographic protocols made with abstracted cryptographic operations are valid for real implementations. However, a major goal has not been achieved yet: a soundness proof for an abstract crypto-library as needed for the cryptographic protocols typically proved with formal methods, e.g., authentication and key exchange protocols. Prior work that directly justifies the typical Dolev-Yao abstraction is restricted to passive adversaries and certain protocol environments. Prior work starting from the cryptographic side entirely hides the cryptographic objects, so that the operations are not composable: While secure channels or signing of application data is modeled, one cannot encrypt a signature or sign a key. We make the major step towards this goal: We specify an abstract crypto-library that allows composed operations, define a cryptographic realization, and prove that the abstraction is sound for arbitrary active attacks in arbitrary reactive scenarios. The library currently contains public-key encryption and signatures, nonces, lists, and application data. The proof is a novel combination of a probabilistic, imperfect bisimulation with cryptographic reductions and static information-flow analysis.
BibTeX
@misc{eprint-2003-11733,
  title={A Universally Composable Cryptographic Library},
  booktitle={IACR Eprint archive},
  keywords={foundations / cryptographic protocols, security analysis of protocols, cryptographically composable operators},
  url={http://eprint.iacr.org/2003/015},
  note={ mbc@zurich.ibm.com 12076 received 24 Jan 2003},
  author={Michael Backes and Birgit Pfitzmann and Michael Waidner},
  year=2003
}