A Verified Extensible Library of Elliptic Curves

Abstract : 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.
Type de document :
Communication dans un congrès
29th IEEE Computer Security Foundations Symposium (CSF), Jun 2016, Lisboa, Portugal. IEEE Computer Security Foundations Symposium (CSF 2016), 2016, 〈10.1109/CSF.2016.28〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01425957
Contributeur : Bhargavan Karthikeyan <>
Soumis le : mercredi 4 janvier 2017 - 09:20:49
Dernière modification le : vendredi 6 janvier 2017 - 01:22:41

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

324