Dans cette thèse, nous étudions la modélisation de la dépendance stochastique entre composantes d'un vecteur aléatoire sous l'angle des copules. La première partie des travaux consiste en une exploration numérique des notions de copule et de mesure de dépendance stochastique dans le contexte de la modélisation des incertitudes en simulation numérique. La seconde partie des travaux porte sur l'étude des transformations de Nataf et de Rosenblatt. Nous montrons que la transformation de Nataf consiste à supposer que le vecteur aléatoire est muni d'une copule Gaussienne. Nous généralisons cette transformation à une distribution absolument continue à copule elliptique quelconque. Nous montrons également l'équivalence entre les transformations de Nataf et de Rosenblatt dans le cas d'une copule Gaussienne. La troisième partie étudie la notion de dépendance stochastique sous contrainte. Nous caractérisons les lois jointes de statistiques d'ordre continues en termes de lois marginales et de copules, et nous proposons une nouvelle famille de copules adaptée à cette modélisation. Nous caractérisons l'existence et l'unicité d'un élément maximal dans cette famille. La quatrième partie s'intéresse aux lois multivariées discrètes, pour lesquelles la notion de copule n'est plus en bijection avec celle de fonction de répartition jointe. Nous établissons un algorithme innovant pour le calcul de probabilités rectangulaires pour une large classe de tels modèles, surclassant les meilleurs algorithmes disponibles tant en termes de précision numérique que de temps de calcul et d'occupation mémoire.

Alors qu'initialement utilisés pour résoudre le Problème du Logarithme Discret (DLP) dans le groupe de points d'une courbe elliptique, les couplages sont très à la mode en cryptographie ces années car ils permettent de construire de nouveaux protocoles cryptographiques. Cependant, le calcul efficace du couplage dépend de l'arithmétique du modèle de courbe elliptique choisi et du corps sur lequel cette courbe est définie. Dans cette thèse, nous calculons le couplage sur deux modèles de Jacobi de courbes elliptiques puis nous introduisons et étudions l'arithmétique d'un nouveau modèle d'Ewards de courbe elliptique défini en toutes caractéristiques. Plus précisément, Nous utilisons l'interprétation géométrique de la loi de groupe sur l'intersection des quadriques de Jacobi pour obtenir pour la première fois dans la littérature, les formules explicites de la fonction de Miller pour le calcul du couplage de Tate sur cette courbe. Pour un calcul de couplage avec un degré de plongement pair, nous définissons la tordue quadratique pour obtenir des étapes de doublement et d'addition efficaces dans l'algorithme de Miller. Ensuite nous utilisons un isomorphisme entre la quartique spéciale de Jacobi Ed: Y²=dX⁴+Z⁴ et le modèle de Weierstrass pour obtenir la fonction de Miller nécessaire au calcul du couplage de Tate. Pour un degré de plongement divisible par 4, nous définissons la tordue d'ordre 4 de cette courbe pour obtenir un résultat meilleur du calcul du couplage de Tate par rapport aux courbes elliptiques sous forme de Weierstrass. Notre résultat améliore en même temps les derniers résultats obtenus sur cette courbe. Ce résultat est donc le meilleur connu à ce jour, à notre connaissance, pour le calcul du couplage de Tate sur les courbes possédant des tordues d'ordre 4. En 2006, Hess et al. introduisent le couplage Ate, qui est une version améliorée du couplage de Tate. Nous calculons ce couplage et ses variantes sur la même quartique. Nous y obtenons encore des résultats meilleurs. Notre troisième contribution est l'introduction d'un nouveau modèle d'Edwards de courbe elliptique d'équation 1+x²+y²+x²y²=Xxy. Ce modèle est ordinaire sur les corps de caractéristique 2 et nous montrons qu'il est birationnellement équivalent au modèle original d'Edwards x²+y²=c²(1+x²y²) en caractéristique différente de 2. Pour ce faire, nous utilisons la théorie des fonctions thêta et un modèle intermédiaire que nous appelons modèle thêta de niveau 4. Nous utilisons les relations de Riemann des fonctions thêta pour étudier l'arithmétique de ces deux courbes. Nous obtenons d'une part une loi de groupe complète, unifiée et en particulier compétitive en caractéristique 2 et d'autre part nous présentons les meilleures formules d'addition différentielle sur le modèle thêta de niveau 4.

De nombreuses applications imposent des contraintes de sécurité élevées (notamment au sens confidentialité et intégrité des informations manipulées). Ma thèse s'intéresse à l'accélération matérielle du système de cryptographie asymétrique basé sur les courbes elliptiques (ECC). L'environnement des systèmes visés étant rarement maîtrisé, je prends en compte l'existence potentielle d'attaquants avec un accès physique au circuit.C’est dans ce contexte qu’un crypto-processeur très flexible, compatible aussi bien avec des cibles ASIC que FPGA, a été développé. Dans le but de choisir des protections contre les attaques dites matérielles (analyse de consommation, génération de fautes, etc.), j’évalue la sécurité vis-à-vis des attaques par canaux cachés et le coût de la contre-mesure basée sur l'unification des opérations élémentaires sur des courbes elliptiques. En montant une nouvelle attaque contre un circuit mettant en œuvre des courbes quartiques de Jacobi, je montre qu’il est possible de détecter la réutilisation d’opérandes. Des expérimentations réelles m’ont permis de retrouver le secret en exploitant seulement quelques traces de puissance consommée. Je présente aussi une nouvelle protection permettant de choisir un compromis entre le niveau de sécurité, les performances et le coût. Elle est basée sur une accélération par fenêtrage aléatoire et l'utilisation optimisée d'opérations fictives. / Many applications require achieving high security level (confidentiality or integrity). My thesis is about hardware acceleration of asymmetric cryptography based on elliptic curves (ECC). These systems are rarely in a controlled environment. With this in mind, I consider potential attackers with physical access to the cryptographic device.In this context, a very flexible crypto-processor was developed that can be implemented as an ASIC or on FPGAs. To choose protections against physical attacks (power consumption analysis, fault injection, etc), I evaluate the security against side-channel attacks and the cost of the counter-measure based on operation unification. By mounting a new attack against a chip using Jacobi quartic curves, I show that re-using operands is detectable. By exploiting only some power consumption traces, I manage to recover the secret. I present also a new counter-measure allowing finding a compromise between security level, performances, and overheads. It uses random windows to accelerate computation, mixed to an optimized usage of dummy operations.

Cette thèse traite de deux problèmes dont le lien n’est pas apparent (1) A` quoi ressemble l’abélianisé AK du groupe de Galois absolu d’un corps quadratique imaginaire K, comme groupe topologique? (2) A` quoi ressemble le groupe des points adéliques d’une courbe elliptique sur Q, comme groupe topologique? Pour la première question, la restriction au groupe de Galois abélianisé nous permet d’utiliser la théorie du corps de classes pour analyser AK . Les travaux précédents dans ce domaine, qui remontent à Kubota et Onabe, décrivent le dual de Pontryagin de AK en termes de familles in- finies d’invariants de Ulm à chaque premier p, très indirectement. Notre approche directe par théorie du corps de classes montre que AK con- tient un sous-groupe UK d’indice fini isomorphe au groupe des unités Oˆ* de la complétion profinie Oˆ de l’anneau des entiers de K, et décrit explicitement le groupe topologique UK , essentiellement indépendamment du corps quadratique imaginaire K. Plus précisément, pour tout corps quadratique imaginaire différent de Q(i) et Q(v-2),on a UK ∼= U = Zˆ2 × Y Z/nZ. (n=1) Le caractère exceptionnel de Q(v-2) n’apparaît pas dans les travaux de Kubota et Onabe, et leurs résultats doivent être corrigés sur ce point.Passer du sous-groupe universel UK à AK revient à un problème d’extension pour des groupes adéliques qu’il est possible de résoudre en passant à une extension de quotients convenables impliquant le quotient Zˆ-libre maximal UK/TK de UK . Par résoudre , nous entendons que, pour chaque K suffisamment petit pour permettre des calculs de groupe de classes explicites, nous obtenons un algorithme praticable décidant le comportement de cette extension. Si elle est totalement non-scindée, alors AK est isomorphe comme groupe topologique au groupe universel U . Réciproquement, si l’extension tensorisée par Zp se scinde pour un premier p impair, alors AK n’est pas isomorphe à U . Pour le premier 2, la situation est particulière, mais elle reste contrôlée grâce à l’abondance de résultats sur la 2-partie des groupes de classes de corps quadratiques.Nos expérimentations numériques ont permis de mieux comprendre la distribution des types d’isomorphismes de AK quand K varie, et nous conduisent à des conjectures telles que pour 100% des corps quadratiques imaginaires K de nombre de classes premier, AK est isomorphe au groupe universel U .Pour notre deuxième problème, qui apparaît implicitement dans [?, Section 9, Question 1] (dans le but de reconstruire le corps de nombres K à partir du groupe des points adéliques E(AK ) d’une courbe elliptique convenable sur K), nous pouvons appliquer les techniques usuelles pour les courbes elliptiques sur les corps de nombres, en suivant les mêmes étapes que pour déterminer la structure du groupe Oˆ* rencontré dans notre premier problème. Il s’avère que, dans le cas K = Q que nous traitons au Chapitre 4, le groupe des points adéliques de presque toutes les courbes elliptiques sur Q est isomorphe à un groupe universel E = R/Z × Zˆ × Y Z/nZ (n=1)de nature similaire au groupe U . Cette universalité du groupe des points adéliques des courbes elliptiques provient de la tendance qu’ont les représentations galoisiennes attachées (sur le groupe des points de torsion à valeurs dans Q) à être maximales. Pour K = Q, la représentation galoisienne est maximale si est seulement si la courbe E est une courbe de Serre, et Nathan Jones [?] a récemment démontré que presque toutes les courbes elliptiques sur Q sont de cette nature. En fait, l’universalité de E(AK ) suit d’hypothèses bien plus faibles, et il n’est pas facile de construire des familles de courbes elliptiques dont le groupe des points adéliques n’est pas universel. Nous donnons un tel exemple à la fin du Chapitre 4. / The present thesis focuses on two questions that are not obviously related. Namely,(1) What does the absolute abelian Galois group AK of an imaginary quadratic number field K look like, as a topological group?(2) What does the adelic point group of an elliptic curve over Q look like, as a topological group?For the first question, the focus on abelian Galois groups provides us with class field theory as a tool to analyze AK . The older work in this area, which goes back to Kubota and Onabe, provides a description of the Pontryagin dual of AK in terms of infinite families, at each prime p, of so called Ulm invariants and is very indirect. Our direct class field theoretic approach shows that AK contains a subgroup UK of finite index isomorphic to the unit group Oˆ∗ of the profinite completion Oˆ of the ring of integers of K, and provides a completely explicit description of the topological group UK that is almost independent of the imaginary quadratic field K. More precisely, for all imaginary quadratic number fields different from Q(i) and Q(√−2), we have UK ∼= U = Zˆ2 × Y Z/nZ. (n=1)The exceptional nature of Q(√−2) was missed by Kubota and Onabe, and their theorems need to be corrected in this respect.Passing from the ‘universal’ subgroup UK to AK amounts to a group extension problem for adelic groups that may be ‘solved’ by passing to a suitable quotient extension involving the maximal Zˆ-free quotientUK/TK of UK . By ‘solved’ we mean that for each K that is sufficiently small to allow explicit class group computations for K, we obtain a practical algorithm to compute the splitting behavior of the extension. In case the quotient extension is totally non-split, the conclusion is that AK is isomorphic as a topological group to the universal group U . Conversely, any splitting of the p-part of the quotient extension at an odd prime p leads to groups AK that are not isomorphic to U . For the prime 2, the situation is special, but our control of it is much greater as a result of the wealth of theorems on 2-parts of quadratic class groups.Based on numerical experimentation, we have gained a basic under- standing of the distribution of isomorphism types of AK for varying K, and this leads to challenging conjectures such as “100% of all imagi- nary quadratic fields of prime class number have AK isomorphic to the universal group U ”.In the case of our second question, which occurs implicitly in [?, Section 9, Question 1] with a view towards recovering a number field K from the adelic point group E(AK ) of a suitable elliptic curve over K, we can directly apply the standard tools for elliptic curves over number fields in a method that follows the lines of the determination of the structure of Oˆ∗ we encountered for our first question.It turns out that, for the case K = Q that is treated in Chapter 4, the adelic point group of ‘almost all’ elliptic curves over Q is isomorphic to a universal groupE = R/Z × Zˆ × Y Z/nZ (n=1)that is somewhat similar in nature to U . The reason for the universality of adelic point groups of elliptic curves lies in the tendency of elliptic curves to have Galois representations on their group of Q-valued torsion points that are very close to being maximal. For K = Q, maximality of the Galois representation of an elliptic curve E means that E is a so-called Serre-curve, and it has been proved recently by Nathan Jones [?] that ‘almost all’ elliptic curves over Q are of this nature. In fact, universality of E(AK ) requires much less than maximality of the Galois representation, and the result is that it actually requires some effort to construct families of elliptic curves with non-universal adelic point groups. We provide an example at the end of Chapter 4.

Cette thèse porte sur la famille des nombres dits multizêtas, et sur les relations qu'ils vérifient.Le premier chapitre est une introduction générale au domaine et se donne pour objectif de présenter brièvement les différents cadres dans lesquels s'inscrivent les résultats des trois autres chapitres, et d'énoncer ces résultats.Dans le chapitre 2, on étudie les relations linéaires entre zêtas simples et zêtas doubles, en établissant un lien rigoureux entre ces relations, les relations linéaires entre crochets de Poisson d'éléments de profondeur 1 de l'algèbre de Lie libre à deux générateurs, et l'espace des formes modulaires. Il s'agit en grande partie d'algèbre linéaire élémentaire sur des matrices définies explicitement.Le résultat principal du chapitre 3 a trait à une algèbre de Lie de dérivations déduite de l'étude de la catégorie des motifs elliptiques mixtes introduite par Hain et Matsumoto. Il démontre l'existence de relations linéaires observées par Pollack dans cette algèbre et provenant elles aussi des formes modulaires. Les démonstrations consistent majoritairement à adapter des techniques introduites par Ecalle à l'étude des propriétés de certains polynômes non commutatifs.Le quatrième et dernier chapitre propose une construction d'une algèbre de multizêtas elliptiques formels, en analogie avec les travaux de Hain et Matsumoto sur les motifs elliptiques mixtes et d'Enriquez sur les associateurs elliptiques. Celle-ci se place dans le formalisme écallien des moules ; on prouve deux résultats partiels qui corroborent la validité de cette dernière construction. / This thesis deals with the family of numbers called multiple zeta values, and on the relations they satisfy. The first chapter is a general introduction to the field and has the goal of briefly presenting the different settings into which the results of the three other chapters fit, and stating these results. In chapter 2, we study the linear relations between simple and double zeta values, establishing a rigorous connection between these relations, the linear relations between Poisson bracket of depth 1 elements of the free Lie algebra on two generators, and the space of modular forms. The proofs consist mainly in performing elementary linear algebra on explicitly defined matrices. The main result of chapter 3 involves a Lie algebra of derivations derived from the study of the category of mixed elliptic motives introduced by Hain and Matsumoto. We prove the existence of linear relations observed by Pollack in this algebra and which also come from modular forms. The bulk of the proofs rely on applying techniques introduced by Ecalle to the study of the properties of certain non-commutative polynomials. The fourth and last chapter proposes a construction of an elliptic formal multizeta algebra, in analogy with work by Hain and Matsumoto on mixed elliptic motives and Enriquez on elliptic associators. The latter falls within the écallian formalism of moulds, we prove two partial results which support the validity of said construction.

Nous nous intéressons à des résultats d'approximation et de régularité pour des solutions de viscosité d'équations elliptiques et paraboliques non-linéaires. Dans le chapitre 1, nous proposons, pour une classe générale d'équations elliptiques et paraboliques non-linéaires munies de conditions de Neumann inhomogènes, une interprétation de contrôle déterministe par des jeux répétés à deux personnes qui consiste à représenter la solution comme la limite de la suite des scores associés aux jeux. La condition de Neumann intervient par une pénalisation adaptée près de la frontière. En s'inspirant d'une approche abstraite proposée par Barles et Souganidis, nous prouvons la convergence en établissant des propriétés de monotonie, stabilité et consistance. Le chapitre 2 est consacré à des résultats de régularité sur les solutions d'équations paraboliques non-linéaires associés à un opérateur uniformément elliptique. Nous donnons une estimation de la mesure de Lebesgue de l'ensemble des points possédant un développement de Taylor quadratique global avec un contrôle sur la taille du terme cubique. Sous une hypothèse supplémentaire sur la régularité de la non-linéarité, nous en déduisons un résultat de régularité partielle höldérienne des solutions. Dans les chapitres 3 et 4, nous proposons une méthode générale pour obtenir des taux algébriques de convergence de solutions de schémas d'approximation vers la solution de viscosité sous l'hypothèse d'uniforme ellipticité de l'opérateur. Nous donnons un taux de convergence pour des schémas elliptiques obtenus par principe de programmation dynamique et nous prouvons un taux pour des schémas paraboliques par différences finies et implicites en temps. / In this thesis we study some approximation and regularity results for viscosity solutions of fully nonlinear elliptic and parabolic equations. In the first chapter, we consider a broad class of fully nonlinear elliptic and parabolic equations with inhomogeneous Neumann boundary conditions. We provide a deterministic control interpretation through two-person repeated games which represents the solution as the limit of the sequence of the scores associated to the games. The Neumann condition is modeled by a suitable penalization near the boundary. Inspiring by an abstract method of Barles and Souganidis, we prove the convergence of the score to the solution of the equation by establishing monotonicity, stability and consistency. The second chapter presents some regularity results about viscosity solutions of parabolic equations associated to a uniformly elliptic operator. First we obtain a Lebesgue measure estimate on the points having a quadratic Taylor expansion with a controlled cubic term. Under an additional assumption on the regularity of the nonlinearity, we deduce a partial regularity result about the Hölder regularity of these solutions. In the third and fourth chapters, we propose a general approach to determine algebraic rates of convergence of solutions of approximation schemes to the viscosity solution of fully nonlinear elliptic or parabolic equations under the assumption of uniform ellipticity of the operator. We first give the rate associated to the elliptic schemes derived by dynamic programming principles and proposed by Kohn and Serfaty. We then prove a rate of convergence for finite-difference schemes implicit in time associated to fully nonlinear parabolic equations.

Depuis les années 90, les attaques par canaux auxiliaires ont remis en cause le niveau de sécurité des algorithmes cryptographiques sur des composants embarqués. En effet, tout composant électronique produit des émanations physiques, telles que le rayonnement électromagnétique, la consommation de courant ou encore le temps d’exécution du calcul. Or il se trouve que ces émanations portent de l’information sur l’évolution de l’état interne. On parle donc de canal auxiliaire, car celui-ci permet à un attaquant avisé de retrouver des secrets cachés dans le composant par l’analyse de la « fuite » involontaire. Cette thèse présente d’une part deux nouvelles attaques ciblant la multiplication modulaire permettant d’attaquer des algorithmes cryptographiques protégés et d’autre part une démonstration formelle du niveau de sécurité d’une contre-mesure. La première attaque vise la multiplication scalaire sur les courbes elliptiques implémentée de façon régulière avec un masquage du scalaire. Cette attaque utilise une unique acquisition sur le composant visé et quelques acquisitions sur un composant similaire pour retrouver le scalaire entier. Une fuite horizontale durant la multiplication de grands nombres a été découverte et permet la détection et la correction d’erreurs afin de retrouver tous les bits du scalaire. La seconde attaque exploite une fuite due à la soustraction conditionnelle finale dans la multiplication modulaire de Montgomery. Une étude statistique de ces soustractions permet de remonter à l’enchaînement des multiplications ce qui met en échec un algorithme régulier dont les données d’entrée sont inconnues et masquées. Pour finir, nous avons prouvé formellement le niveau de sécurité de la contre-mesure contre les attaques par fautes du premier ordre nommée extension modulaire appliquée aux courbes elliptiques. / : Since the 1990s, side channel attacks have challenged the security level of cryptographic algorithms on embedded devices. Indeed, each electronic component produces physical emanations, such as the electromagnetic radiation, the power consumption or the execution time. Besides, these emanations reveal some information on the internal state of the computation. A wise attacker can retrieve secret data in the embedded device using the analyzes of the involuntary “leakage”, that is side channel attacks. This thesis focuses on the security evaluation of asymmetric cryptographic algorithm such as RSA and ECC. In these algorithms, the main leakages are observed on the modular multiplication. This thesis presents two attacks targeting the modular multiplication in protected algorithms, and a formal demonstration of security level of a countermeasure named modular extension. A first attack is against scalar multiplication on elliptic curve implemented with a regular algorithm and scalar blinding. This attack uses a unique acquisition on the targeted device and few acquisitionson another similar device to retrieve the whole scalar. A horizontal leakage during the modular multiplication over large numbers allows to detect and correct easily an error bit in the scalar. A second attack exploits the final subtraction at the end of Montgomery modular multiplication. By studying the dependency of consecutive multiplications, we can exploit the information of presence or absence of final subtraction in order to defeat two protections : regular algorithm and blinding input values. Finally, we prove formally the security level of modular extension against first order fault attacks applied on elliptic curves cryptography.

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. / 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.

Dans cette thèse nous appliquons des techniques provenant du calcul formel et de la théorie des langages afin d'améliorer les opérations élémentaires dans certaines tours de corps finis. Nous appliquons notre construction au problème du calcul d'isogénies entre courbes elliptiques et obtenons une variante plus rapide (à la fois en théorie et en pratique) de l'algorithme de Couveignes. Le document est divisé en quatre parties. Dans la partie I nous faisons des rappels d'algèbre et de théorie de la complexité. La partie II traite du principe de transposition : nous généralisons des idées de Bostan, Schost et Lecerf et nous montrons qu'il est possible de transposer automatiquement des programmes sans pertes en complexité-temps et avec une petite perte en complexité-espace. La partie III combine les résultats sur le principe de transposition avec des techniques classiques en théorie de l'élimination ; nous appliquons ces idées pour obtenir des algorithmes asymptotiquement optimaux pour l'arithmétique des tours d'Artin-Schreier de corps finis. Nous décrivons aussi une implantation de ces algorithmes. Enfin, dans la partie IV nous utilisons les résultats précédents afin d'accélérer l'algorithme de Couveignes et de comparer le résultat avec les autres algorithmes pour le calcul d'isogénies qui font l'état de l'art. Nous présentons aussi une nouvelle généralisation de l'algorithme de Couveignes qui calcule des isogénies de degré inconnu.

Cette thèse est dédiée à l'étude des problèmes de transport optimal, alternatifs au problème de Monge-Kantorovich : ils apparaissent naturellement dans des applications pratiques, telles que la conception des réseaux de transport optimal ou la modélisation des problèmes de circulation urbaine. En particulier, nous considérons des problèmes où le coût du transport a une dèpendance non linèaire de la masse : typiquement dans ce type de problèmes, le côut pour déplacer une masse $m$ pour une longueur $\ell$ est $\varphi(m)\, \ell$, où $\varphi$ est une fonction assignée, obtenant ainsi un coût total de type $\sum\varphi(m) \ell$. \par Deux cas importants sont abordés en détail dans ce travail : le cas où la fonction $\varphi$ est subadditive (transport branché), de sorte que la masse a intérêt à voyager ensemble, de manière à réduire le coût total; le cas où $\varphi$ est superadditive (transport congestionné), où au contraire, la masse tend à diffuser autant que possible. \par Dans le cas du transport branché, nous introduisons deux nouveaux modèles: dans le premièr, le transport est décrit par des courbes de mesures de probabilité que minimisent une fonctionnelle de type géodésique (avec un coefficient que pénalise le mesures qui ne sont pas atomiques). Le second est plus dans l'esprit de la formulation de Benamou et Brenier pour les distances de Wasserstein : en particulier, le transport est décrit par paires de ``courbe de mesures--champ de vitesse'', liées par l'équation de continuité, qui minimisent une énergie adéquate (non convexe). Pour les deux modèles, on démontre l'existence de configurations minimales et l'équivalence avec d'autres formulations existantes dans la littèrature. \par En ce qui concerne le cas du transport congestionné, nous passons en revue deux modèles déjà existants, afin de prouver leur équivalence: alors que le premier de ces modèles peut être considéré comme une approche Lagrangienne du problème et il a des liens intéressants avec des questions d'équilibre pour la circulation urbaine, le second est un problème d'optimisation convexe avec contraintes de divergence. \par La preuve de l'équivalence entre les deux modèles constitue le corps principal de la deuxième partie de cette thèse et contient différents éléments d'intérêt, y compris: la théorie des flots des champs de vecteurs peu réguliers (DiPerna-Lions), la construction de Dacorogna et Moser pour les applications de transport et en particulier les résultats de régularité (que nous prouvons ici) pour une équation elliptique très dégénérés, qui ne semble pas avoir été beaucoup étudiée.