A Formal Library for Elliptic Curves in the Coq Proof Assistant

Evmorfia-Iro Bartzia 1 Pierre-Yves Strub 2, *
* Auteur correspondant
1 PROSECCO - Programming securely with cryptography
Inria Paris-Rocquencourt
2 Institute IMDEA Software [Madrid]
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

INRIA

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〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

245

Téléchargements de fichiers

279

Contact


archive-ouverte@inria.fr