A Foundational Proof Framework for Cryptography

Abstract

I present a state-of-the-art mechanized framework for developing and checking proofs of security for cryptographic schemes in the computational model. This system, called the Foundational Cryptography Framework (FCF) is based on the Coq proof assistant, and it provides a sophisticated mechanism for reasoning about cryptography on top of a simple semantics and a small trusted computing base. All of the theory and logic of FCF is proved correct within Coq, thus ensuring that all security results are trustworthy. FCF improves the state of the art by providing a fully foundational system that enjoys the same ease of use of current non-foundational systems.

Facts proved using FCF include the security of El Gamal encryption, HMAC, and an efficient searchable symmetric encryption (SSE) scheme. The proof related to the SSE scheme is among the most complex mechanized cryptographic proofs to date, and this proof demonstrates that FCF can be used to prove the security of complex schemes in a foundational manner.

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. Proofs provide concrete bounds as well as asymptotic security claims. The framework also includes an operational semantics that can be used to reason about the correctness and security of implementations of cryptographic systems.