CoSP: A Framework for Computational Soundness


Dolev-Yao abstractions of cryptographic operations are term algebras
that are meant to capture an attacker's knowledge and capabilities
against a set of cryptographic operations. Encryption, e.g., can be
modeled by simple rules of the form "dec(dk(r), enc(ek(r), m)) = m",
where "m" represents a plaintext, "ek(r),dk(r)" an encryption-
decryption key pair, and "enc" and "dec" functions of such terms.
Such rules also define a Dolev-Yao attacker that only applies the
rules. Dolev-Yao abstractions have been successfully used in automated
protocol verifiers. Another largely unexplored advantage of Dolev-Yao
abstraction is their power to enrich information flow control
techniques with automatically derivable declassification rules.

While Dolev-Yao abstractions provide a useful representation for
automated verification, each such abstraction has to be proven to
actually capture all relevant attacks. To this end, a statement of the
following form -- a computational soundness result -- has to be proven:
whenever a security property holds in a model where cryptography is
represented as Dolev-Yao abstractions and the corresponding Dolev-Yao
attacker is considered, this security property also holds in a model
where the actual cryptographic algorithms are used and cryptographic
attackers (i.e., arbitrary randomized poly-time machines) are considered.

In this talk, I will present CoSP, a unifying rigorous framework for
computational soundness proofs, including recent extension to
equivalence properties and interactive primitive. The big advantage of
CoSP is that it offers a reference point to which programming languages
can be modularly embedded in a sound way, as already done for RCF (a
core calculus for F#) and the applied pi-calculus. I will, furthermore,
briefly talk about a work in progress: we use CoSP to enrich the ADL
semantic (Cassandra's representation of DEX Bytecode) with computationally
sound declassification rules that are canonically derived from a
Dolev-Yao abstraction.