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 formaliza-tion 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.
https://hal.inria.fr/hal-01102288 Contributor : Bruno BlanchetConnect in order to contact the contributor Submitted on : Sunday, October 4, 2015 - 11:48:29 PM Last modification on : Friday, January 21, 2022 - 3:13:39 AM Long-term archiving on: : Tuesday, January 5, 2016 - 10:19:13 AM