The Foundational Cryptography Framework
Adam Petcher, Greg Morrisett

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsCryptographic Implementations and Security · Advanced Authentication Protocols Security · Cryptography and Data Security
