A Formal Library for Elliptic Curves in the Coq Proof Assistant

ABSTRACT. A preliminary step towards the verification of elliptic curve cryptographic algorithms is the development of formal libraries with the corresponding mathematical theory.

In this paper we present a formalization of elliptic curves' theory, in the SSReflect extension of the Coq proof assistant.

Our central contribution is a library containing many of the objects and core properties related to elliptic curve theory.

We demonstrate the applicability of our library by formally proving a non-trivial property of elliptic curves: the existence of an isomorphism between a curve and its Picard group of divisors.