2009 CoSPAGeneralFrameworkforComputa

• (Backes et al., 2009) ⇒ Michael Backes, Dennis Hofheinz, and Dominique Unruh. (2009). “CoSP: A General Framework for Computational Soundness Proofs.” In: Proceedings of the 16th ACM conference on Computer and communications security. ISBN:978-1-60558-894-0 doi:10.1145/1653662.1653672

Subject Headings:

Cited By

• http://scholar.google.com/scholar?q=%222009%22+CoSP%3A+A+General+Framework+for+Computational+Soundness+Proofs
• http://dl.acm.org/citation.cfm?id=1653662.1653672&preflayout=flat#citedby

Quotes

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 π-calculus under active attacks. Concretely, we embed the applied π-calculus into CoSP and give a sound implementation of public-key encryption and digital signatures.

References

;

	Author	volume	Date Value	title	type	journal	titleUrl	doi	note	year
2009 CoSPAGeneralFrameworkforComputa	Michael Backes Dennis Hofheinz Dominique Unruh			CoSP: A General Framework for Computational Soundness Proofs				10.1145/1653662.1653672		2009