Skip to Main content Skip to Navigation
Conference papers

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 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Bruno Blanchet Connect 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


Files produced by the author(s)




Evmorfia-Iro Bartzia, Pierre-yves Strub. A Formal Library for Elliptic Curves in the Coq Proof Assistant. Interactive Theorem Proving, Jul 2014, Vienna, Austria. pp.77-92, ⟨10.1007/978-3-319-08970-6_6⟩. ⟨hal-01102288⟩



Record views


Files downloads