Paper 2009/080

CoSP: A General Framework For Computational Soundness Proofs

Michael Backes, Dennis Hofheinz, and Dominique Unruh

Abstract

We describe CoSP, a general framework for conducting computational soundness proofs of symbolic models and for embedding these proofs into formal calculi. CoSP considers arbitrary equational theories and computational implementations, and it abstracts away many details that are not crucial for proving computational soundness, such as message scheduling, corruption models, and even the internal structure of a protocol. CoSP enables soundness results, in the sense of preservation of trace properties, to be proven in a conceptually modular and generic way: proving x cryptographic primitives sound for y calculi only requires x+y proofs (instead of x*y proofs without this framework), and the process of embedding calculi is conceptually decoupled from computational soundness proofs of cryptographic primitives. We exemplify the usefulness of CoSP 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 CoSP and give a sound implementation of public-key encryption and digital signatures.

Note: Erata will be published at: http://crypto.m2ci.org/unruh/publications/erata/cosp-erata.pdf Version history: 2009-02-18: Initial revision 2009-06-03: Support for signatures has been added. The proofs have been made more detailed and the introduction extended. 2009-10-26: In definition of CoSP protocols: Merged constructor and destructor nodes into one type, computation nodes. In Section 3: Added nonces to the message type for the encryption theory (were missing). Some corrections in the proofs of Section 3.

Metadata
Available format(s)
PDF
Publication info
Published elsewhere. A short version appears at ACM CCS 2009
Keywords
symbolic cryptographyDolev-Yao modelcomputational soundness
Contact author(s)
unruh @ mmci uni-saarland de
History
2009-10-26: last of 2 revisions
2009-02-18: received
See all versions
Short URL
https://ia.cr/2009/080
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2009/080,
      author = {Michael Backes and Dennis Hofheinz and Dominique Unruh},
      title = {{CoSP}: A General Framework For Computational Soundness Proofs},
      howpublished = {Cryptology {ePrint} Archive, Paper 2009/080},
      year = {2009},
      url = {https://eprint.iacr.org/2009/080}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.