Skip to Main content Skip to Navigation

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.
Complete list of metadatas

Cited literature [37 references]  Display  Hide  Download

https://hal.inria.fr/hal-01425957
Contributor : Bhargavan Karthikeyan <>
Submitted on : Saturday, December 8, 2018 - 10:25:33 AM
Last modification on : Monday, December 10, 2018 - 8:39:19 AM
Document(s) archivé(s) le : Saturday, March 9, 2019 - 12:32:22 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

565

Files downloads

439