A Formal Library for Elliptic Curves in the Coq Proof Assistant - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2014

A Formal Library for Elliptic Curves in the Coq Proof Assistant

Résumé

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.
Fichier principal
Vignette du fichier
A-Formal-Library-for-Elliptic-Curves-in-the-Coq-Proof-Assistant.pdf (513.76 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01102288 , version 1 (04-10-2015)

Identifiants

Citer

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⟩

Collections

INRIA INRIA2
300 Consultations
829 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More