Foundational Cryptography Framework for machine-checked proofs of cryptography in the computational model.
Getting Started:
-
cd src/FCF
-
make
Then open a simple example from the “src/examples” directory in Proof General. A good place to start is “ElGamal.v.” Interactively step through this proof to learn how to develop a simple proof of non-adaptive security in the concrete setting. PRF_Encryption_IND_CPA.v contains a more complex proof of adaptive security along with a proof in the asymptotic setting.
The publications describing FCF are available at adam.petcher.net.