Les méthodes formelles ont fait leurs preuves dans l’étude des protocoles de sécurité et plusieurs outils existent, permettant d’automatiser ces vérifications. Hélas, ils se montrent parfois dans l’incapacité d’analyser certains protocoles, à cause des primitives cryptographiques employées ou des propriétés que l’on cherche à démontrer. On étudie deux systèmes existants: un protocole de vote par internet Norvégien et un protocole pour les votes en réunion du CNRS. Nous analysons les garanties de sécurité qu’ils proposent, dans différents scénarios de corruption. Malgré les résultats réutilisables obtenus, ces preuves démontrent également la difficulté de les effectuer à la main. Une nouvelle piste dans l’automatisation de telles preuves pourrait alors venir des systèmes de types. Basés sur le développement récent d’un système de types permettant de traiter des propriétés d’équivalence, nous l’avons utilisé afin de démontrer des propriétés comme l’anonymat du vote. Nous avons appliqué cette méthode Helios, un système de vote par internet bien connu. Il existe une autre famille de protocoles de sécurité : les APIs. Ces interfaces permettent l’utilisation d’informations stockées dans des dispositifs sécurisés sans qu’il soit normalement possible de les en ex- traire. Des travaux récents montrent que ces interfaces sont également vulnérables. Cette thèse présente un nouveau design d’API, incluant une fonctionnalité de révocation, rarement présente dans les solutions existantes. Nous démontrons, par une analyse formelle, qu’aucune combinaison de commandes ne permet de faire fuir des clefs sensées rester secrètes, même si l’adversaire parvient à en brute-forcer certaines / Formal methods have been used to analyze security protocols and several tools have even been developed to tackle automatically different proof techniques and ease the verification of such protocols. However, for electronic voting and APIs, current tools tend to reach their limits because they can’t handle some cryptographic primitives, or the security properties, involved in those protocols. We work on two cases studies of existing and deployed systems: a Norwegian e-voting protocol and a CNRS boardroom voting protocol. We analyze them using the applied pi-calculus model and we discuss in details about their security properties, in different corruption scenarios. Even including several reusable results, these proofs are complex and, therefore, expose a real need for automation. Thus, we focus on a possible lead in direction of this needed automation: type-systems. We build upon a recent work describing a new type-system designed to deal with equivalence properties, in order to apply this on the verification of equivalence-based properties in electronic voting like ballot-secrecy. We present an application of this method through Helios, a well-known e-voting system. Another family of advanced security protocols are APIs: secure interfaces devoted to allow access to some information stored into a secured trusted hardware without leaking it outside. Recet work seems to show that these interfaces are also vulnerable. In this thesis, we provide a new design for APIs, including revocation. In addition, we include a formal analysis of this API showing that a malicious combination of API’s commands does not leak any key, even when the adversary may brute-force some of them

Cette thèse porte sur l'étude de différents aspects de la sécurité des protocoles de vote électronique à distance. Ces protocoles décrivent comment organiser des élections par Internet de manière sécurisée. Ils ont notamment pour but d'apporter des garanties de secret du vote, et de vérifiabilité - ie, il doit être possible de s'assurer que les votes sont correctement comptabilisés. Nos contributions portent sur deux aspects principaux. Premièrement, nous proposons une nouvelle technique d'analyse automatique de propriétés d'équivalence, dans le modèle symbolique. De nombreuses propriétés en lien avec la vie privée s'expriment comme des propriétés d'équivalence, telles que le secret du vote en particulier, mais aussi l'anonymat ou la non-traçabilité. Notre approche repose sur le typage: nous mettons au point un système de typage qui permet d'analyser deux protocoles pour prouver leur équivalence. Nous montrons que notre système de typage est correct, c'est-à-dire qu'il implique effectivement l'équivalence de traces, à la fois pour des nombres bornés et non bornés de sessions. Nous comparons l'implémentation d'un prototype de notre système avec les autres outils existants pour l'équivalence symbolique, sur divers protocoles de la littérature. Cette étude de cas montre que notre procédure est bien plus efficace que la plupart des autres outils - au prix d'une perte de précision (notre outil peut parfois échouer à prouver certaines équivalences). Notre seconde contribution est une étude des définitions du secret du vote et de la vérifiabilité - ou, plus précisément, la vérifiabilité individuelle, une propriété qui requiert que chaque votant soit en mesure de vérifier que son propre vote a bien été pris en compte. Nous prouvons, aussi bien dans les modèles symboliques que calculatoire, que le secret du vote implique la vérifiabilité individuelle, alors même que l'intuition et des résultats voisins déjà établis semblaient indiquer que ces deux propriétés s'opposent. Notre étude met également en évidence une limitation des définitions existantes du secret du vote par jeux cryptographiques : elles supposent une urne honnête, et par conséquent expriment des garanties significativement plus faibles que celles que les protocoles visent à assurer. Nous proposons donc une nouvelle définition (par jeu) du secret du vote, contre une urne malhonnête. Nous relions notre définition à une notion de secret du vote par simulation, pour montrer qu'elle apporte des garanties fortes. Enfin, nous menons une étude de cas sur plusieurs systèmes de vote existants. / In this thesis we study several aspects of the security of remote electronic voting protocols. Such protocols describe how to securely organise elections over the Internet. They notably aim to guarantee vote privacy - ie, votes must remain secret -and verifiability - it must be possible to check that votes are correctly counted. Our contributions are on two aspects. First, we propose a new approach to automatically prove equivalence properties in the symbolic model. Many privacy properties can be expressed as equivalence properties, such as in particular vote privacy, but also anonymity or unlinkability. Our approach relies on typing: we design a type system that can typecheck two protocols to prove their equivalence. We show that our type system %, together with some additional conditions on the messages exchanged by the protocols, soundly implies trace equivalence, both for bounded and unbounded numbers of sessions. We compare a prototype implementation of our typechecker with other existing tools for symbolic equivalence, on a variety of protocols from the literature. This case study shows that our procedure is much more efficient than most other tools - at the price of losing precision (our tool may fail to prove some equivalences). Our second contribution is a study of the definitions of privacy and verifiability - more precisely, individual verifiability, a property that requires each voter to be able to check that their own vote is counted. We prove that, both in symbolic and computational models, privacy implies individual verifiability, contrary to intuition and related previous results that seem to indicate that these two properties are opposed. Our study also highlights a limitation of existing game-based definitions of privacy: they assume the ballot box is trusted, which makes for significantly weaker guarantees than what protocols aim for. Hence we propose a new game-based definition for vote privacy against a dishonest ballot box. We relate our definition to a simulation-based notion of privacy, to show that it provides meaningful guarantees, and conduct a case study on several voting schemes.

Le chiffrement à base de réseaux euclidiens a connu un grand essor durant les vingt dernières années. Autant grâce à l’apparition de nouvelles primitives telles que le chiffrement complètement homomorphe, que grâce à l’amélioration des primitives existantes, comme le chiffrement á clef publique ou les signatures digitales, qui commencent désormais à rivaliser avec leurs homologues fondés sur la théorie des nombres. Cela dit les preuves à divulgation nulle de connaissance, bien qu’elles représentent un des piliers des protocols de confidentialité, n’ont pas autant progressé, que ce soit au niveau de leur expressivité que de leur efficacité. Cette thèse s’attelle dans un premier temps à améliorer l’état de l’art en matière de preuves à divulgation nulle de connaissance. Nous construisons une preuve d’appartenance à un sous ensemble dont la taille est indépendante de l’ensemble en question. Nous construisons de même une preuve de connaissance amortie qui est plus efficace et plus simple que toutes les constructions qui la précèdent. Notre second propos est d’utiliser ces preuves à divulgation nulle de connaissance pour construire de nouvelles primitives cryptographiques. Nous concevons une signature de groupe dont la taille est indépendante du groupe en question, ainsi qu’un schéma de vote électronique hautement efficace, y compris pour des élections à grand échelle. / Lattice based cryptography has developed greatly in the last two decades, both with new and stimulating results such as fully-homomorphic encryption, and with great progress in the efficiency of existing cryptographic primitives like encryption and signatures which are becoming competitive with their number theoretic counterparts. On the other hand, even though they are a crucial part of many privacy-based protocols, zero-knowledge proofs of knowledge are still lagging behind in expressiveness and efficiency. The first goal of this thesis is to improve the quality of lattice-based proofs of knowledge. We construct new zero-knowledge proofs of knowledge such as a subset membership proof with size independent of the subset. We also work towards making zero-knowledge proofs more practical, by introducing a new amortized proof of knowledge that subsumes all previous results. Our second objective will be to use the proofs of knowledge we designed to construct novel and efficient cryptographic primitives. We build a group signature whose size does not depend on the size of the group, as well as a practical and highly scalable lattice-based e-voting scheme.

Le chiffrement homomorphe est une branche de la cryptologie, dans laquelle les schémas de chiffrement offrent la possibilité de faire des calculs sur les messages chiffrés, sans besoin de les déchiffrer. L’intérêt pratique de ces schémas est dû à l’énorme quantité d'applications pour lesquels ils peuvent être utilisés. En sont un exemple le vote électronique, les calculs sur des données sensibles, comme des données médicales ou financières, le cloud computing, etc..Le premier schéma de chiffrement (complètement) homomorphe n'a été proposé qu'en 2009 par Gentry. Il a introduit une technique appelée bootstrapping, utilisée pour réduire le bruit des chiffrés : en effet, dans tous les schémas de chiffrement homomorphe proposés, les chiffrés contiennent une petite quantité de bruit, nécessaire pour des raisons de sécurité. Quand on fait des calculs sur les chiffrés bruités, le bruit augmente et, après avoir évalué un certain nombre d’opérations, ce bruit devient trop grand et, s'il n'est pas contrôlé, risque de compromettre le résultat des calculs.Le bootstrapping est du coup fondamental pour la construction des schémas de chiffrement homomorphes, mais est une technique très coûteuse, qu'il s'agisse de la mémoire nécessaire ou du temps de calcul. Les travaux qui on suivi la publication de Gentry ont eu comme objectif celui de proposer de nouveaux schémas et d’améliorer le bootstrapping pour rendre le chiffrement homomorphe faisable en pratique. L’une des constructions les plus célèbres est GSW, proposé par Gentry, Sahai et Waters en 2013. La sécurité du schéma GSW se fonde sur le problème LWE (learning with errors), considéré comme difficile en pratique. Le bootstrapping le plus rapide, exécuté sur un schéma de type GSW, a été proposé en 2015 par Ducas et Micciancio. Dans cette thèse on propose une nouvelle variante du schéma de chiffrement homomorphe de Ducas et Micciancio, appelée TFHE.Le schéma TFHE améliore les résultats précédents, en proposant un bootstrapping plus rapide (de l'ordre de quelques millisecondes) et des clés de bootstrapping plus petites, pour un même niveau de sécurité. TFHE utilise des chiffrés de type TLWE et TGSW (scalaire et ring) : l’accélération du bootstrapping est principalement due à l’utilisation d’un produit externe entre TLWE et TGSW, contrairement au produit externe GSW utilisé dans la majorité des constructions précédentes.Deux types de bootstrapping sont présentés. Le premier, appelé gate bootstrapping, est exécuté après l’évaluation homomorphique d’une porte logique (binaire ou Mux) ; le deuxième, appelé circuit bootstrapping, peut être exécuté après l’évaluation d’un nombre d'opérations homomorphiques plus grand, pour rafraîchir le résultat ou pour le rendre compatible avec la suite des calculs.Dans cette thèse on propose aussi de nouvelles techniques pour accélérer l’évaluation des calculs homomorphiques, sans bootstrapping, et des techniques de packing des données. En particulier, on présente un packing, appelé vertical packing, qui peut être utilisé pour évaluer efficacement des look-up table, on propose une évaluation via automates déterministes pondérés, et on présente un compteur homomorphe appelé TBSR qui peut être utilisé pour évaluer des fonctions arithmétiques.Pendant les travaux de thèse, le schéma TFHE a été implémenté et il est disponible en open source.La thèse contient aussi des travaux annexes. Le premier travail concerne l’étude d’un premier modèle théorique de vote électronique post-quantique basé sur le chiffrement homomorphe, le deuxième analyse la sécurité des familles de chiffrement homomorphe dans le cas d'une utilisation pratique sur le cloud, et le troisième ouvre sur une solution différente pour le calcul sécurisé, le calcul multi-partite. / Fully homomorphic encryption is a new branch of cryptology, allowing to perform computations on encrypted data, without having to decrypt them. The main interest of homomorphic encryption schemes is the large number of practical applications for which they can be used. Examples are given by electronic voting, computations on sensitive data, such as medical or financial data, cloud computing, etc..The first fully homomorphic encryption scheme has been proposed in 2009 by Gentry. He introduced a new technique, called bootstrapping, used to reduce the noise in ciphertexts: in fact, in all the proposed homomorphic encryption schemes, the ciphertexts contain a small amount of noise, which is necessary for security reasons. If we perform computations on noisy ciphertexts, the noise increases and, after a certain number of operations, the noise becomes to large and it could compromise the correctness of the final result, if not controlled.Bootstrapping is then fundamental to construct fully homomorphic encryption schemes, but it is very costly in terms of both memory and time consuming.After Gentry’s breakthrough, the presented schemes had the goal to propose new constructions and to improve bootstrapping, in order to make homomorphic encryption practical. One of the most known schemes is GSW, proposed by Gentry, Sahai et Waters in 2013. The security of GSW is based on the LWE (learning with errors) problem, which is considered hard in practice. The most rapid bootstrapping on a GSW-based scheme has been presented by Ducas and Micciancio in 2015. In this thesis, we propose a new variant of the scheme proposed by Ducas and Micciancio, that we call TFHE.The TFHE scheme improves previous results, by performing a faster bootstrapping (in the range of a few milliseconds) and by using smaller bootstrapping keys, for the same security level. TFHE uses TLWE and TGSW ciphertexts (both scalar and ring): the acceleration of bootstrapping is mainly due to the replacement of the internal GSW product, used in the majority of previous constructions, with an external product between TLWE and TGSW.Two kinds of bootstrapping are presented. The first one, called gate bootstrapping, is performed after the evaluation of a homomorphic gate (binary or Mux); the second one, called circuit bootstrapping, can be executed after the evaluation of a larger number of homomorphic operations, in order to refresh the result or to make it compatible with the following computations.In this thesis, we also propose new techniques to improve homomorphic computations without bootstrapping and new packing techniques. In particular, we present a vertical packing, that can be used to efficiently evaluate look-up tables, we propose an evaluation via weighted deterministic automata, and we present a homomorphic counter, called TBSR, that can be used to evaluate arithmetic functions.During the thesis, the TFHE scheme has been implemented and it is available in open source.The thesis contains also ancillary works. The first one concerns the study of the first model of post-quantum electronic voting based on fully homomorphic encryption, the second one analyzes the security of homomorphic encryption in a practical cloud implementation scenario, and the third one opens up about a different solution for secure computing, multi-party computation.

De Kheops à Internet, des nanotechnologies à la téléportation, les nouvelles technologies rythment la vie des hommes. Fruits de leur intelligence, outils de grands travaux, moteurs de diffusion des savoirs, elles sont cause et effet des progrès de l’humanité. Innervant les relations de travail subordonnées comme tous les compartiments de la société, elles retiennent l’attention du juriste tant elles sont susceptibles de remodeler l’organisation de l’entreprise, de provoquer l’exclusion de la communauté de travail (au moins autant que de rapprocher ceux qui la composent), de provoquer l’entremêlement des vies personnelle et professionnelle. Nul compartiment du droit des relations de travail n’échappe à la pression des nouvelles technologies : au recrutement des salariés elles peuvent donner un nouveau visage ; à la conclusion du contrat de travail elles peuvent offrir instantanéité et dématérialisation ; au temps de son exécution elles imposent normes de sécurité (pour que, de chacun, le corps soit préservé) et normes de vie (pour que, de chacun, l’âme et l’esprit demeurent hors du champ de lecture de l’employeur). Et que dire du jeu de relations collectives remodelées à coup de communications syndicales dématérialisées, de vote électronique, de réunions virtuelles d’instance de représentation du personnel ? Le paysage se transforme. Le corpus normatif, parfois, peine à suivre. Le temps des diseurs de droit n’est pas celui de la science. Mais la science ne peut aller sans que le législateur et le juge, un jour, s’en saisissent. D’intérêts contradictoires où s’entremêlent impératif d’évolution (de l’entreprise) et de protection (du salarié), il leur appartient d’assurer la conciliation. / Over the centuries, from Cheops to the Internet and from nanotechnology to teleportation, new technologies have constantly been at the centre of individuals’ lives. Produced by human intelligence, they appear to be a key to innovation, a tool for the dissemination of knowledge and they enable the progress and evolution of mankind. These new technologies obviously drew lawyers’ attention as they have a direct impact on society as a whole, but also more specifically on the relationship between employers and employees. Moreover, they tend to reshape the organisation of corporations and lead to the entanglement of professional and private life. As a matter of fact, labour law is under pressure: recruitment procedures can be altered by new technologies, the conclusion of employment contracts is nowadays electronic and instantaneous, and security and privacy rules have been established (not to mention electronic trade union communications, e-voting or e-meetings for staff representative bodies). In short, the whole framework is changing. Unfortunately, lawmakers are usually overtaken by events as science and law evolve at a very different pace. However, sooner or later, legal boundaries are set. Currently, courts’ main challenge is to try to make technological progress and protection of employees compatible.