Dans cette thèse, nous nous intéressons à la résolution du problème de la satisfiabilité propositionnelle (SAT). Ce problème fondamental en théorie de la complexité est aujourd'hui utilisé dans de nombreux domaines comme la planification, la bio-informatique, la vérification de matériels et de logiciels. En dépit d'énormes progrès observés ces dernières années dans la résolution pratique du problème SAT, il existe encore une forte demande d'algorithmes efficaces pouvant permettre de résoudre les problèmes difficiles. C'est dans ce contexte que se situent les différentes contributions apportées par cette thèse. Ces contributions s'attellent principalement autour de deux composants clés des solveurs SAT : l'apprentissage de clauses et les heuristiques de choix de variables de branchement. Premièrement, nous proposons une méthode de résolution permettant d'exploiter les fonctions booléennes cachées généralement introduites lors de la phase d'encodage CNF pour réduire la taille des clauses apprises au cours de la recherche. Ensuite, nous proposons une approche de résolution basée sur le principe d'intensification qui indique les variables sur lesquelles le solveur devrait brancher prioritairement à chaque redémarrage. Ce principe permet ainsi au solveur de diriger la recherche sur la sous-formule booléenne la plus contraignante et de tirer profit du travail de recherche déjà accompli en évitant d'explorer le même sous-espace de recherche plusieurs fois. Dans une troisième contribution, nous proposons un nouveau schéma d'apprentissage de clauses qui permet de dériver une classe particulière de clauses Bi-Assertives et nous montrons que leur exploitation améliore significativement les performances des solveurs SAT CDCL issus de l'état de l'art. Finalement, nous nous sommes intéressés aux principales stratégies de gestion de la base de clauses apprises utilisées dans la littérature. En effet, partant de deux stratégies de réduction simples : élimination des clauses de manière aléatoire et celle utilisant la taille des clauses comme critère pour juger la qualité d'une clause apprise, et motiver par les résultats obtenus à partir de ces stratégies, nous proposons plusieurs nouvelles stratégies efficaces qui combinent le maintien de clauses courtes (de taille bornée par k), tout en supprimant aléatoirement les clauses de longueurs supérieures à k. Ces nouvelles stratégies nous permettent d'identifier les clauses les plus pertinentes pour le processus de recherche. / In this thesis, we focus on propositional satisfiability problem (SAT). This fundamental problem in complexity theory is now used in many application domains such as planning, bioinformatic, hardware and software verification. Despite enormous progress observed in recent years in practical SAT solving, there is still a strong demand of efficient algorithms that can help to solve hard problems. Our contributions fit in this context. We focus on improving two of the key components of SAT solvers: clause learning and variable ordering heuristics. First, we propose a resolution method that allows to exploit hidden Boolean functions generally introduced during the encoding phase CNF to reduce the size of clauses learned during the search. Then, we propose an resolution approach based on the intensification principle that circumscribe the variables on which the solver should branch in priority at each restart. This principle allows the solver to direct the search to the most constrained sub-formula and takes advantage of the previous search to avoid exploring the same part of the search space several times. In a third contribution, we propose a new clause learning scheme that allows to derive a particular Bi-Asserting clauses and we show that their exploitation significantly improves the performance of the state-of-the art CDCL SAT solvers. Finally, we were interested to the main learned clauses database reduction strategies used in the literature. Indeed, starting from two simple strategies : random and size-bounded reduction strategies, and motivated by the results obtained from these strategies, we proposed several new effective ones that combine maintaing short clauses (of size bounded by k), while deleting randomly clauses of size greater than k. Several other efficient variants are proposed. These new strategies allow us to identify the most important learned clauses for the search process.

Dans cette thèse, nous étudions la sécurité de primitives cryptographiques. Ces systèmes sont fondés sur des transformations utilisant des objets mathématiques représentés de multiples manières. Nous utilisons alors certaines structures inhérentes à leurs composantes, et jusqu'alors non prises en compte, pour mettre en évidence de nouvelles vulnérabilités. Par l'exploitation de diverses représentations, nous avons ainsi cryptanalysé des chiffrements authentifiés de la compétition CAESAR, des chiffrements à flot spécifiques et des constructions génériques. Nous avons donné des critères de conception en vue de la standardisation par le NIST de chiffrements à bas coût. Dans le cas des chiffrements à flot, nous avons défini de nouveaux critères cryptographiques plus pertinents que les critères usuels. Plus précisément, nous analysons la sécurité des chiffrements par bloc légers au regard des récentes attaques par invariant, et nous montrons comment les éviter par un choix approprié de la couche linéaire de diffusion et des constantes de tour. Nous proposons une nouvelle cryptanalyse des registres filtrés, grâce à la décomposition des éléments dans les sous-groupes multiplicatifs du corps fini à 2^n éléments. L'analyse du chiffrement FLIP, mais aussi du générateur pseudo-aléatoire de Goldreich a mis en évidence des faiblesses exploitables dans des attaques de type ``supposer et déterminer'', qui nécessitent la prise en compte de nouveaux critères sur les fonctions booléennes utilisées dans ce contexte. Enfin, nous cryptanalysons une version simplifiée du chiffrement authentifié Ketje en utilisant plusieurs techniques, permettant ainsi d'affiner l'évaluation de sa sécurité. / In this thesis, we study the security of symmetric cryptographic primitives. These systems are based on transformations relying on mathematical objects that can be represented in multiple ways. We then exploit different induced structures to highlight new vulnerabilities. By exploiting various representations, we cryptanalyzed some schemes submitted to the CAESAR competition, and also some dedicated and generic stream ciphers. We exhibited design criteria for lightweight block ciphers in view of the NIST standardization process and in the case of stream ciphers we defined new cryptographic criteria more relevant than the usual ones. More precisely, we study the security of lightweight block ciphers with respect to the recent invariant attacks, and we show how to avoid them with an appropriate choice of the linear layer and the round constants. We propose a new cryptanalysis of the filtered registers, by decomposing elements in the multiplicative subgroups of the finite field with 2^n elements. The analysis of the FLIP cipher, but also of the Goldreich pseudo-random generator, revealed weaknesses that are exploitable in ``guess and determine'' attacks. This leads to new criteria on the Boolean functions used in this context. Finally, we cryptanalyze a weaker version of the authenticated encryption scheme Ketje using several techniques, in order to refine the security evaluation of this cipher.

Cette thèse traite de la synchronisation des systèmes dynamiques. La synchronisation est étudiée pour une configuration de type maître-esclave, c'est-à-dire pour des systèmes couplés de façon unidirectionnelle. Ce type de configuration s'avère d'un intérêt tout particulier car elle correspond à des architectures de communications chiffrées un-vers-un ou un-vers-plusieurs. Une attention spécifique est portée sur l'autosynchronisation, comportement qui caractérise la synchronisation par le simple couplage maître-esclave et donc en l'absence de tout contrôle extérieur. Elle joue un rôle majeur dans les communications impliquant des chiffreurs par flot autosynchronisants. L'étude de l'autosynchronisation dans le contexte cryptographique s'appuie sur la théorie du contrôle. Un lien original entre l'autosynchronisation et le principe de chiffrement/déchiffrement en cryptographie est mis en évidence. Il fait appel à la propriété de platitude des systèmes dynamiques, un concept emprunté à l'automatique. On montre que les systèmes dynamiques plats définissent complètement l'ensemble des systèmes autosynchronisants et permettent d'élargir les structures existantes des chiffreurs autosynchronisants. La platitude est tout d'abord étudiée pour deux types de systèmes non linéaires~: les systèmes linéaires commutés et à paramètres variants (LPV). La caractérisation des sorties plates s'appuie sur le concept de semigroupes nilpotents et un algorithme performant est proposé. Une approche constructive pour réaliser des structures maître-esclave autosynchronisantes est proposée sur la base de systèmes plats et les notions d'inversibilité à gauche et à droite empruntées à la théorie du contrôle. Par la suite, l'autosynchronisation est étudiée dans le contexte booléen privilégié en cryptographie. Elle est caractérisée en premier lieu au travers la notion d'influence. Ensuite, différentes représentations matricielles associées aux fonctions booléennes sont proposées. Ces représentations s'avèrent particulièrement intéressantes pour l'analyse des propriétés liées à la sécurité. Un lien entre l'autosynchronisation et les structures propres des représentations matricielles est établi. Une approche orientée graphes est finalement élaborée pour la caractérisation. De nouvelles constructions de structures autosynchronisantes en sont déduites et des éléments de sécurité sont discutés. Enfin, une plateforme de test à base de FPGA qui a été réalisée est décrite.

Les travaux de cette thèse portent sur les critères de sécurité des<br />algorithmes de chiffrement à clé secrète et ont été menés suivant deux<br />axes. Le premier concerne la sécurité des chiffrements symétriques<br />itératifs par blocs contre les attaques par distingueur sur le dernier<br />tour. Les résultats portent en particulier sur la généralisation d'une<br />attaque différentielle d'ordre supérieur menée sur l'algorithme<br />MISTY1. L'origine de cette attaque ainsi que de sa généralisation a pu<br />être expliquée grâce aux propriétés du spectre de Walsh des fonctions<br />de non-linéarité maximale utilisées. Ainsi il a été possible<br />d'élaborer une attaque générique sur tous les chiffrements de Feistel<br />à cinq tours utilisant des fonctions dont le spectre de Walsh est<br />divisible par une grande puissance de 2 car cette propriété permet<br />d'obtenir une borne supérieure sur le degré de la composition de<br />telles fonctions, nettement plus faible que la borne<br />triviale. Cette attaque suggère ainsi un nouveau critère de sécurité<br />qui porte sur la divisibilité du spectre de Walsh des fonctions de<br />tour utilisées dans les chiffrements itératifs par blocs. La deuxième<br />partie de la thèse porte sur l'étude des fonctions booléennes<br />symétriques, et en particulier sur l'existence éventuelle de<br />propriétés cryptographiques. À partir d'une propriété structurelle de<br />périodicité d'une représentation d'une fonction booléenne symétrique,<br />les propriétés de degré algébrique, d'équilibre, de résilience, de<br />critère de propagation et de non-linéarité ont été étudiées, ce qui a<br />permis d'améliorer les résultats existants. Par ailleurs, le calcul<br />explicite du spectre de Walsh des fonctions booléennes symétriques de<br />degré 2 et 3 a été réalisé, ainsi que la détermination de toutes les<br />fonctions symétriques équilibrées de degré inférieur ou égal à 7,<br />indépendamment du nombre de variables.