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.
Type de document :
Communication dans un congrès
Gerwin Klein; Ruben Gamboa. Interactive Theorem Proving, Jul 2014, Vienna, Austria. Springer, 8558, pp.77-92, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-08970-6_6〉
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01102288
Contributeur : Bruno Blanchet <>
Soumis le : dimanche 4 octobre 2015 - 23:48:29
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : mardi 5 janvier 2016 - 10:19:13

Fichier

A-Formal-Library-for-Elliptic-...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Evmorfia-Iro Bartzia, Pierre-Yves Strub. A Formal Library for Elliptic Curves in the Coq Proof Assistant. Gerwin Klein; Ruben Gamboa. Interactive Theorem Proving, Jul 2014, Vienna, Austria. Springer, 8558, pp.77-92, 2014, Lecture Notes in Computer Science. 〈10.1007/978-3-319-08970-6_6〉. 〈hal-01102288〉

Partager

Métriques

Consultations de la notice

245

Téléchargements de fichiers

279