The Foundational Cryptography Framework

TL;DR

The Foundational Cryptography Framework (FCF) is a comprehensive tool within Coq for formalizing and verifying cryptographic security proofs, supporting a wide range of schemes and providing concrete bounds.

Contribution

FCF introduces a general-purpose, Coq-based framework that streamlines the development and checking of cryptographic security proofs with probabilistic programming and reasoning capabilities.

Findings

Supports modeling of diverse cryptographic schemes

Enables formal proofs with concrete security bounds

Reduces proof development effort in cryptography

Abstract

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.