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

https://hal.inria.fr/hal-01102288
Contributor : Bruno Blanchet <>
Submitted on : Sunday, October 4, 2015 - 11:48:29 PM
Last modification on : Friday, May 25, 2018 - 12:02:06 PM
Long-term archiving on: : Tuesday, January 5, 2016 - 10:19:13 AM

File

A-Formal-Library-for-Elliptic-...
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

414

Files downloads

798