Iro Bartzia, Pierre-Yves Strub
The theory of elliptic curves is a subject where one finds diverse branches of mathematics, such as, complex analysis, algebraic geometry, representation theory and number theory. It has been an active field of study since the 19th century. Elliptic curves have been used to approach a wide range of problems such as the fast factorisation of integers and the search for congruent numbers. In the 20th century, they have regained interest because of their applications in cryptography, first suggested in 1985 independently by Neal Koblitz and Victor Miller. Their use in cryptography relies principally on the existence of a group law for the set of points on an elliptic curve. This group is a very good candidate for cryptographic groups used in public key cryptography because of the hardness of the Discrete Logarithm Problem on it (relative to the parameters of the curve). Elliptic curves also allow the definition of new cryptographic primitives, such as identity-based encryption, based on bilinear (Weil and Tate) pairings. In any case, elliptic curve theory remains a subject of active research because of its wide range of applications, as well as the rich mathematics behind it.
This work is concerned with proving the security of cryptographic schemes based on elliptic curves. Proving security for cryptographic schemes can be an extremely delicate task because of the level of details that the proof requires, as well as the broad set of concepts and reasoning methods from complexity, probability and group theory that are involved. Machine-checked proofs are often used in cryptography in order to increase confidence in cryptographic proofs. For instance, CertiCrypt is a fully machine-checked framework for developing and verifying cryptographic game-playing proofs, built on top of the Coq proof assistant. Up to date, it has been used to formally prove the security of well known cryptographic schemes such as the OAEP padding, hashed El Gamal encryption and Full Domain Hash digital signatures.
You can download the Coq source of our formalization here. You need Coq v8.3pl2 with ssreflect r3350.
Windows users can download the Coq bundle which includes all the necessary tools.