A Verified Extensible Library of Elliptic Curves - INRIA - Institut National de Recherche en Informatique et en Automatique Accéder directement au contenu
Communication Dans Un Congrès Année : 2016

A Verified Extensible Library of Elliptic Curves

Résumé

In response to increasing demand for elliptic curve cryptography, and specifically for curves that are free from the suspicion of influence by the NSA, new elliptic curves such as Curve25519 and Curve448 are currently being standardized, implemented, and deployed in major protocols such as Transport Layer Security. As with all new cryptographic code, the correctness of these curve implementations is of concern, because any bug or backdoor in this code can potentially compromise the security of important Internet protocols. We present a principled approach towards the verification of elliptic curve implementations by writing them in the dependently-typed programming language F* and proving them functionally correct against a readable mathematical specification derived from a previous Coq development. A key technical innovation in our work is the use of templates to write and verify arbitrary precision arithmetic once and for all for a variety of Bignum representations used in different curves. We also show how to use abstract types to enforce a coding discipline that mitigates side-channels at the source level. We present a verified F* library that implements the popular curves Curve25519, Curve448, and NIST-P256, and we show how developers can add new curves to this library with minimal programming and verification effort.
Fichier principal
Vignette du fichier
paper.pdf (492.67 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01425957 , version 1 (08-12-2018)

Identifiants

Citer

Jean Karim Zinzindohoue, Evmorfia-Iro Bartzia, Karthikeyan Bhargavan. A Verified Extensible Library of Elliptic Curves. 29th IEEE Computer Security Foundations Symposium (CSF), Jun 2016, Lisboa, Portugal. ⟨10.1109/CSF.2016.28⟩. ⟨hal-01425957⟩

Collections

INRIA INRIA2
1427 Consultations
546 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More