The Foundational Cryptography Framework

Adam Petcher, Greg Morrisett

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 gener…