Skip to Main content Skip to Navigation
Conference papers

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 metadata

Cited literature [37 references]  Display  Hide  Download
Contributor : Bhargavan Karthikeyan Connect in order to contact the contributor
Submitted on : Saturday, December 8, 2018 - 10:25:33 AM
Last modification on : Friday, January 21, 2022 - 3:19:51 AM
Long-term archiving on: : Saturday, March 9, 2019 - 12:32:22 PM


Files produced by the author(s)




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⟩



Les métriques sont temporairement indisponibles