A Certification Toolbox for Cryptographic Algorithms
This is a toolbox built on top of the proof assistant Coq. It allows one to make game-based security proofs for cryptographic algorithms.
A gentle introduction to the toolbox is included in this paper. An earlier version was introduced in this paper.
In this paper the toolbox is used to make a formal proof of security of an implementation in SmartMIPS Assembly of a pseudorandom number generator.
An independent review of this toolbox and an extension to support the random-oracle model are respectively available in sections 2.3 and 3.2 of this deliverable of the European Union CACE project.
Requirements
- Coq 8.3
- A recent version of Objective Caml
- the Pocklington library (for its proof of Fermat's little theorem)
Documentation
(index)
Examples
- ElGamal: the encryption primitive ElGamal where plaintexts are element of a cyclic group, based on the DDH problem
- HashedElGamal: the encryption primitive ElGamal where plaintexts are bitstrings, based on DDH and entropy smoothing
- GoldwasserMicali: the encryption primitive of Goldwasser and Micali, based on the quadratic residuosity problem
- BBS: the pseudorandom bit generator of Blum, Blum and Shub, based on the quadratic residuosity problem
Cryptography Library
- HardProblem: mathematical problems believed to be hard
- Security: security notions
General Library
- Bitstring: bitstrings of fixed length
- Group: elementary group theory
- Distribution: finite probability distributions
- Swap: a tactic to swap binders in distributions
- Tactics: tactics for manipulating distributions
- Zstar: the multiplicative group of integers modulo
- LittleFermat: Fermat's little theorem
Addenda to the standard library of Coq
Download
On request by e-mail:
Contributors
José Carlos Bacelar Almeida, Ricardo Coelho, and Henrique Castro (University of Minho) contributed a part of MiscLists.