Les travaux de cette thèse s'inscrivent dans le cadre de la cryptographie, et plus précisément de la cryptographie quantique. Le but est de concevoir un système permettant de transmettre simultanément une clé de cryptage et un signal horloge dans une même fibre optique (à la longueur d'onde des télécommunications soit 1550 nm) en essayant d'éviter les effets de la dispersion chromatique. En effet le signal représentant la clé de cryptage doit être réalisé sous forme d'impulsions fortement atténuées simulant des photons uniques et dans ces conditions il est nécessaire de disposer au niveau du détecteur d'un signal horloge donnant l'instant d'arrivée des impulsions. Nous fabriquons deux signaux de longueurs d'onde très proches (écart de 0,88 pm) grâce à un modulateur acousto-optique, chacune servant de porteuse à un des deux signaux. A la réception il est nécessaire de séparer ces deux longueurs d'ondes et pour cela un filtre basé sur un interféromètre de Fabry-Pérot a été conçu, réalisé, testé et mis en oeuvre au laboratoire. Puis nous avons aussi réalisé un photodétecteur basé sur une photodiode à avalanche, dont nous pouvons abaisser la température de fonctionnement jusqu'à environ 0°C. Le système a été entièrement réalisé et nous avons pu montrer la faisabilité de cette technique. Des améliorations restent à apporter en particulier sur la stabilité du filtre optique et sur le fonctionnement du détecteur en mode comptage de photons.

Longtemps considérée comme une curiosité de laboratoire, la distribution quantique de clés s'est aujourd'hui imposée comme une solution viable de sécurisation des données. Les lois fondamentales de la physique quantique permettent en effet de garantir la sécurité inconditionnelle des clés secrètes distribuées.<br /><br />Nous avons proposé un système de distribution quantique de clés par photons uniques exploitant un véritable codage en fréquence de l'information. Cette nouvelle méthode de codage permet de s'affranchir de dispositifs interférométriques et offre donc une grande robustesse. Un démonstrateur basé sur des composants optiques intégrés standard a été réalisé et a permis de valider expérimentalement le principe de codage. Nous avons ensuite étudié un système mettant en oeuvre un protocole de cryptographie quantique par « variables continues », codant l'information sur l'amplitude et la phase d'états cohérents. Le dispositif proposé est basé sur un multiplexage fréquentiel du signal porteur d'information et d'un oscillateur local. <br /><br />Les débits atteints par les systèmes de distribution de clés ne sont pas uniquement limités par des contraintes technologiques, mais aussi par l'efficacité des protocoles de réconciliation utilisés. Nous avons proposé un algorithme de réconciliation de variables continues efficace, basé sur des codes LDPC et permettant d'envisager de réelles distributions de clés à haut débit avec les protocoles à variables continues.

Reproduction de : Thèse de doctorat : Sciences : Mathématiques : Toulon : 2005. / Titre provenant du cadre-titre. Bibliographie p.213-218.

Depuis 2000 les couplages sont devenus un très bon outil pour la conception de nouveaux protocoles cryptographiques. Les signatures courtes et le chiffrement basé sur l'identité sont devenus réalisables grâce aux couplages. Les travaux réalisés dans cette thèse comprennent deux aspects complémentaires. Une partie consiste en l'implémentation optimisée de couplages sur différentes courbes elliptiques, en fonction des protocoles visés. Une implémentation sur des courbes supersingulières en grande caractéristique et sur des courbes de Barreto-Naehrig est détaillée. La bibliothèque développée au Laboratoire Chiffre de Thales est utilisée avec des courbes de Barreto-Naehrig dans un protocole de diffusion chiffrée. La seconde application évalue la différence de temps de calcul pour des protocoles utilisant les couplages sur des courbes d'ordre composé (un large module RSA) et la traduction de ces protocoles qui utilise plusieurs couplages sur des courbes plus habituelles. Les résultats montrent une différence d'un facteur de 30 à 250 en fonction des étapes des protocoles, ce qui est très important. Une seconde partie porte sur deux familles de courbes de genre deux. Les jacobiennes de ces courbes sont isogènes au produit de deux courbes elliptiques sur une extension de corps de petit degré. Cette isogénie permet de transférer les propriétés des courbes elliptiques vers les jacobiennes. Le comptage de points est aisé et ne requiert qu'un comptage de points sur une des courbes elliptiques isogènes, plus quelques ajustements. On présente aussi la construction de deux endomorphismes à la fois sur les jacobiennes et sur les courbes elliptiques. Ces deux endomorphismes permettent des multiplications scalaires efficaces en suivant la méthode de Gallant, Lambert et Vanstone, ici en dimension quatre.

La cryptographie visuelle consiste à partager entre plusieurs " Shadow Images " (SIs) un secret qui ne se révèlera à l'oeil de l'observateur qu'à leur superposition. Depuis les travaux de Naor et Shamir, ce procédé cryptographique a été étendu à Des schémas numériques variés, adaptés à diverses problématiques. En revanche, les travaux concernant son implémentation physique sont peu nombreux à ce jour. Cette thèse est consacrée à l'implémentation de la cryptographie visuelle sur des SIs imprimés en demi-tons en vue de l'authentification de documents. Le SI associé au document peut être imprimé sur support opaque ou transparent, les autres SIs étant imprimés sur films transparents. Nous avons résolu la difficulté de leur superposition par une méthode de Fourier permettant le recalage de la structure quasi-périodique d'un SI. La précision de cette méthode nous a permis de développer un système optique de superposition par projection. On verra que les phénomènes physiques responsables du rendu visuel de SIs superposés sont propices à une protection contre la copie illicite du SI associé à un document. La complexité de ces phénomènes et leur dépendance au type d'impression imposent une modélisation physique pour obtenir un rendu précis. Cette approche nous a conduit à considérer la problématique de la reproduction des couleurs et à développer des modèles spectraux adaptés à la superposition de supports imprimés non diffusants et/ou diffusants, en réflexion et en transmission. La précision de ces modèles prédictifs est tout à fait satisfaisante au regard de celle habituellement obtenue dans le domaine de la reproduction des couleurs. Cela nous a permis d'introduire une approche originale de la cryptographie visuelle par ajustement de couleur (color matching) : une même couleur, à une tolérance près basée sur la vision humaine, est générée par différents demi-tons imprimés sur les supports à superposer. La couleur du message peut ainsi constituer un secret partagé entre les SIs de la même façon que l'est le contenu du message. Chaque SI pris individuellement ne laisse fuir aucune information sur la couleur du message, qui ne sera révélée qu'à leur superposition. Cela peut permettre de prévenir une attaque par falsification du SI associé au document (cheating attack ). De plus, le rendu des couleurs étant très dépendant du système d'impression utilisé, une reproduction fidèle à partir d'un système d'impression différent est difficile. La difficulté peut être encore accrue par l'utilisation de caractéristiques d'impression non standard

IPv6, protocole succédant à IPv4, est en cours de déploiement dans l'Internet. Il repose fortement sur le mécanisme Neighbor Discovery Protocol (NDP). Celui-ci permet non seulement à deux nœuds IPv6 de pouvoir communiquer, à l'instar du mécanisme Address Resolution Protocol (ARP) en IPv4, mais il apporte aussi de nouvelles fonctionnalités, telles que l'autoconfiguration d'adresse IPv6. Aussi, sa sécurisation pour le bon fonctionnement de l'Internet en IPv6 est critique. Son mécanisme de sécurité standardisée à l'Internet Engineering Task Force (IETF) se nomme Secure Neighbor Discovery (SEND). Il s'appuie à la fois sur l'utilisation d'identifiants cryptographiques, adresses IPv6 appelées Cryptographically Generated Addresses (CGA) et qui sont générées à partir d'une paire de clés publique/privée, et de certificats électroniques X.509. L'objet de cette thèse est l'étude de ces identifiants cryptographiques, les adresses CGA, ainsi que le mécanisme SEND les employant, et leurs réutilisations potentielles pour la sécurisation IPv6. Dans une première partie de cette thèse, tout d'abord, nous posons l'état de l'art. Dans une deuxième partie de cette thèse, nous nous intéressons à la fiabilité du principal mécanisme connu employant les adresses CGA, le mécanisme SEND. Dans une troisième et dernière partie de cette thèse, nous présentons des utilisations des identifiants cryptographiques pour la sécurisation IPv6

Dans cette thèse, nous étudions les définitions et les constructions en boite noire avec des instantiations efficaces pour la diffusion chiffrée et le traçage de traîtres. Nous commençons par examiner les notions de sécurité pour la diffusion chiffrée présentes dans la littérature. Comme il n'y a pas de moyen facile de les comparer, nous proposons un cadre général et établissons des relations. Nous montrons alors comment les notions existantes s'inscrivent dans ce cadre. Ensuite, nous présentons une construction en boite noire d'un système de diffusion chiffrée dynamique décentralisée. Ce système ne repose sur aucune autorité de confiance, et de nouveaux utilisateurs peuvent joindre à tout moment. Le système satisfait la notion de sécurité la plus forte sous des hypothèses de sécurité classiques de ses composantes. Il admet une instantiation efficace qui est sûre sous la seule hypothèse DDH dans le modèle standard. Enfin, nous donnons une construction en boite noire d'un système de traçage de traîtres à base de messages, qui permet de tracer non seulement à partir des décodeurs pirates, mais aussi à partir des tatouages numériques contenus dans un message. Notre schéma est le premier à obtenir asymptotiquement le taux d'expansion optimal de 1. Nous montrons également que vus les débits de données actuels, le schéma est déjà pratique pour les choix de valeurs usuels.

Safety-critical systems - such as electronic flight control systems and nuclear reactor controls - must satisfy strict safety requirements. We are interested here in the application of formal methods - built upon solid mathematical bases - to verify the behavior of safety-critical systems. More specifically, we formally specify our algorithms and then prove them correct using the Coq proof assistant - a program capable of mechanically checking the correctness of our proofs, providing a very high degree of confidence. In this thesis, we apply formal methods to obtain safe Worst-Case Execution Time (WCET) estimations for C programs. The WCET is an important property related to the safety of critical systems, but its estimation requires sophisticated techniques. To guarantee the absence of errors during WCET estimation, we have formally verified a WCET estimation technique based on the combination of two main methods: a loop bound estimation and the WCET estimation via the Implicit Path Enumeration Technique (IPET). The loop bound estimation itself is decomposed in three steps: a program slicing, a value analysis based on abstract interpretation, and a loop bound calculation stage. Each stage has a chapter dedicated to its formal verification. The entire development has been integrated into the formally verified C compiler CompCert. We prove that the final estimation is correct and we evaluate its performances on a set of reference benchmarks. The contributions of this thesis include (a) the formalization of the techniques used to estimate the WCET, (b) the estimation tool itself (obtained from the formalization), and (c) the experimental evaluation. We conclude that our formally verified development obtains interesting results in terms of precision, but it requires special precautions to ensure the proof effort remains manageable. The parallel development of specifications and proofs is essential to this end. Future works include the formalization of hardware cost models, as well as the development of more sophisticated analyses to improve the precision of the estimated WCET.

Cette thèse est consacrée à la description et à l'étude de la sécurité de divers protocoles destinés à faire de l'authentification d'objets physiques à distance à base de comparaison de vecteurs binaires. L'objectif des protocoles proposés est de pouvoir réaliser une authentification en garantissant d'une part que les informations envoyées et reçues par le lecteur n'ont pas été manipulées par un adversaire extérieur et d'autre part sans révéler l'identité de l'objet testé à un tel adversaire, ou même, modulo certaines hypothèses raisonnables, aux composantes du système. Nous nous sommes fixés de plus comme objectif d'utiliser des méthodes de cryptographie sur courbe elliptique pour pouvoir profiter des bonnes propriétés de ces dernières, notamment une sécurité accrue par rapport à la taille des clefs utilisées. Nous présentons plusieurs protocoles atteignant l'objectif et établissons pour presque tous une preuve théorique de leur sécurité, grâce notamment à une nouvelle caractérisation d'une notion standard de sécurité.

Cette thèse est dédiée à la cryptanalyse de l'AES (Advanced Encryption Standard) qui est l'un des systèmes de chiffrement par bloc les plus répandu dans le monde. Nous y présentons une nouvelle technique pour résoudre un type particulier d'équations spécialement conçu pour attaquer l'AES. Cette technique est basée sur l'algèbre linéaire ainsi que sur la technique de la " Rencontre par le Milieu " et offre pour un système donné, plusieurs algorithmes de résolution de complexités différentes mais prédictibles. Ainsi nous avons conçu un programme pour trouver l'algorithme le plus rapide. Dans un premier temps nous l'avons appliqué directement aux systèmes d'équations décrivant un nombre réduit de tours d'AES et avons trouvé de nouvelles attaques lorsque la quantité de couples clair/chiffré est très limitée, améliorant celles trouvées manuellement par d'autres chercheurs. La technique étant générale nous avons pu utiliser le programme pour étudier d'autres modèles comme celui des attaques par fautes et celui des attaques à clé choisie ainsi que d'autres primitives cryptographiques comme la fonction d'authentification Pelican-MAC et le système de chiffrement par flot LEX. Enfin nous présentons une généralisation des attaques de Demirci et Selçuk publiées à la conférence FSE2008 ainsi qu'un algorithme qui nous a permis de trouver les meilleures attaques de cette classe, avec certaines parmi les meilleures connues à ce jour. Cet algorithme repose sur l'utilisation du précédent programme afin de déterminer le nombre de valeurs prises par des sous-ensembles d'octets de clé ou des états internes ainsi que la complexité de les énumérer.