  We present the Foundational Cryptography Framework (FCF) for developing and
checking complete proofs of security for cryptographic schemes within a proof
assistant. This is a general-purpose framework that is capable of modeling and
reasoning about a wide range of cryptographic schemes, security definitions,
and assumptions. Security is proven in the computational model, and the proof
provides concrete bounds as well as asymptotic conclusions. FCF provides a
language for probabilistic programs, a theory that is used to reason about
programs, and a library of tactics and definitions that are useful in proofs
about cryptography. The framework is designed to leverage fully the existing
theory and capabilities of the Coq proof assistant in order to reduce the
effort required to develop proofs.
