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.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 2015
- Accession Number
- AD1034943
Entities
People
- Adam Petcher
Organizations
- Harvard University