**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.

**Permalink:** http://www.ut.ee/~unruh/publications/backes09cosp.html