A formalization of elliptic curves for cryptography

Abstract : This thesis is in the domain of formalization of mathematics and ofverification of cryptographic algorithms. The implementation ofcryptographic algorithms is often a complicated task becausecryptographic programs are optimized in order to satisfy bothefficiency and security criteria. As a result it is not alwaysobvious that a cryptographique program actually corresponds to themathematical algorithm, i.e. that the program is correct. Errors incryprtographic programs may be disastrous for the security of anentire cryptosystem, hence certification of their correctness isrequired. Formal systems and proof assistants such as Coq andIsabelle-HOL are often used to provide guarantees and proofs thatcryptographic programs are correct. Elliptic curves are widely usedin cryptography, mainly as efficient groups for asymmetriccryptography. To develop formal proofs of correctness forelliptic-curve schemes, formal theory of elliptic curves is needed.Our motivation in this thesis is to formalize elliptic curve theoryusing the Coq proof assistant, which enables formal analysis ofelliptic-curve schemes and algorithms. For this purpose, we used theSsreflect extension and the mathematical libraries developed by theMathematical Components team during the formalization of the FourColor Theorem. Our central result is a formal proof of Picard’stheorem for elliptic curves: there exists an isomorphism between thePicard group of divisor classes and the group of points of an ellipticcurve. An important immediate consequence of this proposition is theassociativity of the elliptic curve group operation. Furthermore, wepresent a formal proof of correctness for the GLV algorithm for scalarmultiplication on elliptic curve groups. The GLV algorithm exploitsproperties of the elliptic curve group in order to acceleratecomputation. It is composed of three independent algorithms:multiexponentiation on a generic group, decomposition of the scalarand computing endomorphisms on algebraic curves. This developmentincludes theory about endomorphisms on elliptic curves and is morethan 5000 lines of code. An application of our formalization is alsopresented.
Complete list of metadatas

Cited literature [106 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/tel-01563979
Contributor : Abes Star <>
Submitted on : Tuesday, July 18, 2017 - 1:25:05 PM
Last modification on : Thursday, April 11, 2019 - 7:52:33 AM
Long-term archiving on : Saturday, January 27, 2018 - 7:50:50 AM

File

43038_BARTZIA_2017_archivage.p...
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-01563979, version 1

Collections

Citation

Evmorfia-Iro Bartzia. A formalization of elliptic curves for cryptography. Cryptography and Security [cs.CR]. Université Paris-Saclay, 2017. English. ⟨NNT : 2017SACLX002⟩. ⟨tel-01563979⟩

Share

Metrics

Record views

624

Files downloads

874