A formalization of elliptic curves for cryptography

Résumé : Le sujet de ma thèse s’inscrit dans le domaine des preuves formelleset de la vérification des algorithmescryptographiques. L’implémentation des algorithmes cryptographiquesest souvent une tâche assez compliquée, parce qu’ils sont optimiséspour être efficaces et sûrs en même temps. Par conséquent, il n’estpas toujours évident qu’un programme cryptographique en tant quefonction, corresponde exactement à l’algorithme mathématique,c’est-à-dire que le programme soit correct. Les erreurs dans lesprogrammes cryptographiques peuvent mettre en danger la sécurité desystèmes cryptographiques entiers et donc, des preuves de correctionsont souvent nécessaires. Les systèmes formels et les assistants depreuves comme Coq et Isabelle-HOL sont utilisés pour développer despreuves de correction des programmes. Les courbes elliptiques sontlargement utilisées en cryptographie surtout en tant que groupecryptographique très efficace. Pour le développement des preuvesformelles des algorithmes utilisant les courbes elliptiques, unethéorie formelle de celles-ci est nécessaire. Dans ce contexte, nousavons développé une théorie formelle des courbes elliptiques enutilisant l’assistant de preuves Coq. Cette théorie est par la suiteutilisée pour prouver la correction des algorithmes de multiplicationscalaire sur le groupe des points d’une courbe elliptique.Plus précisément, mes travaux de thèse peuvent être divisées en deuxparties principales. La première concerne le développement de lathéorie des courbes elliptiques en utilisant l'assistant des preuvesCoq. Notre développement de plus de 15000 lignes de code Coqcomprend la formalisation des courbes elliptiques données par uneéquation de Weierstrass, la théorie des corps des fonctionsrationnelles sur une courbe, la théorie des groupes libres et desdiviseurs des fonctions rationnelles sur une courbe. Notre résultatprincipal est la formalisation du théorème de Picard; une conséquencedirecte de ce théorème est l’associativité de l’opération du groupedes points d’une courbe elliptique qui est un résultat non trivial àprouver. La seconde partie de ma thèse concerne la vérification del'algorithme GLV pour effectuer la multiplication scalaire sur descourbes elliptiques. Pour ce développement, nous avons vérifier troisalgorithmes indépendants: la multiexponentiation dans un groupe, ladécomposition du scalaire et le calcul des endomorphismes sur unecourbe elliptique. Nous avons également développé une formalisationdu plan projectif et des courbes en coordonnées projectives et nousavons prouvé que les deux représentations (affine et projective) sontisomorphes.Notre travail est à la fois une première approche à la formalisationde la géométrie algébrique élémentaire qui est intégré dans lesbibliothèques de Ssreflect mais qui sert aussi à la certification devéritables programmes cryptographiques.
Type de document :
Thèse
Cryptography and Security [cs.CR]. Université Paris-Saclay, 2017. English. 〈NNT : 2017SACLX002〉
Liste complète des métadonnées

Littérature citée [106 références]  Voir  Masquer  Télécharger

https://pastel.archives-ouvertes.fr/tel-01563979
Contributeur : Abes Star <>
Soumis le : mardi 18 juillet 2017 - 13:25:05
Dernière modification le : jeudi 26 avril 2018 - 10:28:17
Document(s) archivé(s) le : samedi 27 janvier 2018 - 07:50:50

Fichier

43038_BARTZIA_2017_archivage.p...
Version validée par le jury (STAR)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

508

Téléchargements de fichiers

532