Security proof of cryptographic algorithms with Coq

Authors: Ulisses Araújo Costa, Pedro Pereira

This project is included in my Msc of Cryptography. Here I have to study the theoretical framework developed by David Nowak, and learn how to do cryptographic proofs using Coq proof assistant. Nowadays is very important to start apply a lot of formalism to this kind of proofs.
Because, like Bellare and Rogaway said:“many proofs in cryptography have become essentially unverifiable. Our field may be approaching a crisis of rigor.”. So is extremely necessary to start using mechanical methods to prove the algorithms.

More information: A Framework for Game-Based Security Proofs, On formal verification of arithmetic-based cryptographic primitives