Le travail présenté dans cette thèse est une contribution aux méthodes formelles de spécification et de vérification. Les spécifications formelles sont utilisées pour décrire un logiciel, ou plus généralement un système, d'une manière mathématique sans ambiguïté. Des techniques de vérification formelle sont définies sur la base de ces spécifications afin d'assurer l'exactitude d'un système donné. Cependant, les méthodes formelles ne sont souvent pas pratiques et facile à utiliser dans des systèmes réels. L'une des raisons est que de nombreux formalismes de spécification ne sont pas assez riches pour couvrir à la fois les exigences orientées données et orientées comportement. Certains langages de spécification ont été proposés pour couvrir ce genre d'exigences. Le langage Circus se distingue parmi ces langues par une syntaxe et une sémantique riche et complètement intégrées.L'objectif de cette thèse est de fournir un cadre formel pour la spécification et la vérification de systèmes complexes. Les spécifications sont écrites en Circus et la vérification est effectuée soit par des tests ou par des preuves de théorèmes. Des environnements similaires de spécification et de vérification ont déjà été proposés dans la littérature. Une spécificité de notre approche est de combiner des preuves de théorème avec la génération de test. En outre, la plupart des méthodes de génération de tests sont basés sur une caractérisation syntaxique des langages étudiés. Notre environnement est différent car il est basé sur la sémantique dénotationnelle et opérationnelle de Circus. L'assistant de preuves Isabelle/HOL constitue la plateforme formelle au-dessus de laquelle nous avons construit notre environnement de spécification et de vérification.La première contribution principale de notre travail est l'environnement formel de spécification et de preuve Isabelle/Circus, basé sur la sémantique dénotationnelle de Circus. Sur la base d'Isabelle/HOL nous avons fourni une intégration vérifiée d'UTP, la base de la sémantique de Circus. Cette intégration est utilisée pour formaliser la sémantique dénotationnelle du langage Circus. L'environnement Isabelle/Circus associe à cette sémantique des outils de parsing qui aident à écrire des spécifications Circus. Le support de preuve d'Isabelle/HOL peut être utilisé directement pour raisonner sur ces spécifications grâce à la représentation superficielle de la sémantique (shallow embedding). Nous présentons une application de l'environnement à des preuves de raffinement sur des processus Circus (impliquant à la fois des données et des aspects comportementaux).La deuxième contribution est l'environnement de test CirTA construit au-dessus d'Isabelle/Circus. Cet environnement fournit deux tactiques de génération de tests symboliques qui permettent la vérification de deux notions de raffinement: l'inclusion des traces et la réduction de blocages. L'environnement est basé sur une formalisation symbolique de la sémantique opérationnelle de Circus avec Isabelle/Circus. Plusieurs définitions symboliques et tactiques de génération de test sont définies dans le cadre de CirTA. L'infrastructure formelle permet de représenter explicitement les théories de test ainsi que les hypothèses de sélection de test. Des techniques de preuve et de calculs symboliques sont la base des tactiques de génération de test. L'environnement de génération de test a été utilisé dans une étude de cas pour tester un système existant de contrôle de message. Une spécification du système est écrite en Circus, et est utilisé pour générer des tests pour les deux relations de conformité définies pour Circus. Les tests sont ensuite compilés sous forme de méthodes de test JUnit qui sont ensuite exécutées sur une implémentation Java du système étudié.

La programmation par aspects est un paradigme de programmation qui permet de mieux séparer les préoccupations d'une application. Un aspect est défini pour chaque préoccupation qui ne peut pas être isolée dans un module. Les aspects sont ensuite ajoutés au programme de base par un processus automatique appelé tissage. Cependant, l'expressivité des langages d'aspect généraux permet de modifier totalement la sémantique du programme de base (par ex., un aspect peut remplacer certains appels de méthode par du code arbitraire). Ce comportement peut entraîner la perte des avantages (lisibilité, maintenabilité, réutilisabilité, etc.) d'une meilleure modularisation des préoccupations. Il devient impossible de raisonner sur le programme de base sans regarder le programme tissé. Cette thèse apporte une réponse aux problèmes ci-dessus en définissant des catégories d'aspects dont l'impact sur la sémantique du programme de base reste sous contrôle. Pour chaque catégorie d'aspects, nous déterminons l'ensemble des propriétés du programme de base qui est préservé par tissage. L'appartenance d'un aspect à une catégorie est garantie par construction grâce à des langages d'aspect dédiés pour chaque catégorie. L'utilisation de ces langages assure que le tissage préservera l'ensemble des propriétés associé à la catégorie concernée. Les propriétés préservées sont représentées comme des sous ensembles de LTL et de CTL*. Nous prouvons formellement que quelque soit le programme de base, le tissage de n'importe quel aspect d'une catégorie préserve les propriétés de la catégorie correspondante. Ces langages et catégories sont définis dans un cadre formel indépendant de tout langage de base ou d'aspect. L'expressivité de ce cadre est montrée en décrivant des primitives complexes de langages d'aspect comme AspectJ et CaesarJ et en effectuant une preuve de correction de transformation d'aspect.

Le langage mathématique courant et les langages mathématiques formelssont très éloignés. Par <> nousentendons la prose que le mathématicien utilise tous les jours dansses articles et ses livres. C'est une langue naturelle avec desexpressions symboliques et des notations spécifiques. Cette langue està la fois flexible et structurée mais reste sémantiquementintelligible par tous les mathématiciens.Cependant, il est très difficile de formaliser automatiquement cettelangue. Les raisons principales sont: la complexité et l'ambiguïté deslangues naturelles en général, le mélange inhabituel entre languenaturelle et notations symboliques tout aussi ambiguë et les sautsdans le raisonnement qui sont pour l'instant bien au-delà descapacités des prouveurs de théorèmes automatiques ou interactifs.Pour contourner ce problème, les assistants de preuves actuelsutilisent des langages formels précis dans un système logique biendéterminé, imposant ainsi de fortes restrictions par rapport auxlangues naturelles. En général ces langages ressemblent à des langagesde programmation avec un nombre limité de constructions possibles etune absence d'ambiguïté.Ainsi, le monde des mathématiques est séparé en deux, la vastemajorité qui utilise la langue naturelle et un petit nombre utilisantaussi des méthodes formelles. Cette seconde communauté est elle-mêmesubdivisée en autant de groupes qu'il y a d'assistants de preuves. Onperd alors l'intelligibilité des preuves pour tous les mathématiciens.Pour résoudre ce problème, on peut se demander:est-il possible d'écrire un programme qui comprend la langue naturellemathématique et qui la traduit vers un langage formel afin depermettre sa validation?Ce problème se subdivise naturellement en deux sous-problèmes tous lesdeux très difficiles:1. l'analyse grammaticale des textes mathématiques et leur traductiondans un langage formel,2. la validation des preuves écrites dans ce langage formel.Le but du projet MathNat (Mathematics in controlled Natural languages)est de faire un premier pas pour répondre à cette question trèsdifficile, en se concentrant essentiellement sur la première question.Pour cela, nous développons CLM (Controlled Language for Mathematics)qui est un sous-ensemble de l'anglais avec une grammaire et un lexiquerestreint, mais qui inclut tout de même quelques ingrédientsimportants des langues naturelles comme les pronoms anaphoriques, lesréférences, la possibilité d'écrire la même chose de plusieursmanières, des adjectifs distributifs ou non, ...Le second composant de MathNath est MathAbs (Mathematical Abstractlanguage). C'est un langage formel, indépendant du choix d'un systèmelogique permettant de représenter la sémantique des textes enpréservant leur structure et le fil du raisonnement. MathAbs est conçucomme un langage intermédiaire entre CLM et un système logique formelpermettant la vérification des preuves.Nous proposons un système qui permet de traduire CLM vers MathAbsdonnant ainsi une sémantique précise à CLM. Nous considèrons que cetravail est déjà un progrès notable, même si pour l'instant on estloin de pouvoir vérifier formellement toutes les preuves en MathAbsainsi générées.Pour le second problème, nous avons réalisé une petite expérience entraduisant MathAbs vers une liste de formules en logique du premierordre dont la validité garantit la correction de la preuve. Nous avonsensuite essayé de vérifier ces formules avec des prouveurs dethéorèmes automatiques validant ainsi quelques exemples.

Cette thèse se propose de remédier à l'absence de formalisme dédié aux preuves de sécurité concrète à travers 3 contributions. Nous présentons d'abord la logique CIL (Computational Indistinguishability Logic), qui permet de raisonner sur les systèmes cryptographiques. Elle contient un petit nombre de règles qui correspondent aux raisonnements souvent utilisés dans les preuves. Leur formalisation est basée sur des outils classiques comme les contextes ou les bisimulations. Deuxièmement, pour plus d'automatisation des preuves, nous avons conçu une logique de Hoare dédiée aux chiffrement asymétrique dans le modèle de l'oracle aléatoire. Elle est appliquée avec succès sur des exemples de schémas existants. Enfin, nous proposons un théorème générique de réduction pour la preuve d'indifférentiabilité d'un oracle aléatoire de fonctions de hachage cryptographiques. La preuve du théorème, formalisée en CIL, en démontre l'applicabilité. Les exemples de Keccak et Chop-Merkle-Damgard illustrent ce résultat.

The research work presented in this manuscript is of algorithmic kind: it is mainly composed of polynomial, fixed parameter and approximation algorithms, while hardness results are also mentioned.<br /> <br />This work is about building and comparing labelled trees. These objects find application in different areas, but notoriously in phylogenetics, where they represent evolutionary relationships of organisms or sequences.<br /><br />Most of this work can be considered as investigating solutions to so-called \emph{supertree} problems. Supertrees are large trees built by a dynamic programming approach from smaller trees. For instance, the latter are gene trees from which a comprehensive tree on many living species is to be built, such as the \emph{Tree of Life}. <br /><br />First definitions are introduced, then a part of the manuscript is dedicated to quartet tree building methods. The next part details tree comparison methods, mainly variants of the maximum agreement subtree method. Next follows a part on supertree problems in all generality. <br />The manuscript ends with a report of the research plan for the next few years. <br /><br />Several journal papers illustrating the material described in this manuscript are adjoined in appendix.

Cette thèse se propose de remédier à l'absence de formalisme dédié aux preuves de sécurité concrète à travers 3 contributions. Nous présentons d'abord la logique CIL (Computational Indistinguishability Logic), qui permet de raisonner sur les systèmes cryptographiques. Elle contient un petit nombre de règles qui correspondent aux raisonnements souvent utilisés dans les preuves. Leur formalisation est basée sur des outils classiques comme les contextes ou les bisimulations. Deuxièmement, pour plus d'automatisation des preuves, nous avons conçu une logique de Hoare dédiée aux chiffrement asymétrique dans le modèle de l'oracle aléatoire. Elle est appliquée avec succès sur des exemples de schémas existants. Enfin, nous proposons un théorème générique de réduction pour la preuve d'indifférentiabilité d'un oracle aléatoire de fonctions de hachage cryptographiques. La preuve du théorème, formalisée en CIL, en démontre l'applicabilité. Les exemples de Keccak et Chop-Merkle-Damgard illustrent ce résultat. / In this thesis, we address the lack of formalisms to carry out concrete security proofs. Our contributions are threefold. First, we present a logic, named Computational Indistinguishability Logic (CIL), for reasoning about cryptographic systems. It consists in a small set of rules capturing reasoning principles common to many proofs. Their formalization relies on classic tools such as bisimulation relations and contexts. Second, and in order to increase proof automation, it presents a Hoare logic dedicated to asymmetric encryption schemes in the Random Oracle Model that yields an automated and sound verification method. It has been successfully applied to existing encryption schemes. Third, it presents a general reduction theorem for proving indifferentiability of iterative hash constructions from a random oracle. The theorem is proven in CIL demonstrating the usefulness of the logic and has been applied to constructions such as the SHA-3 candidate Keccak and the Chop-MD construction.

Nous nous intéressons à des formules de la logique du premier ordre où certaines constantes sont interprétées dans un domaine défini inductivement, comme les entiers. Le problème de la validité n'est pas semi-décidable pour ces formules. Le but de cette thèse est donc d'accroître les capacités des procédures de preuve les plus efficaces pour la logique du premier ordre (fondées sur le calcul de résolution et de superposition) afin de tenir compte de ces constantes particulières. Pour cela, nous adaptons le calcul de superposition en ajoutant notamment un mécanisme de détection de cycles qui simule une forme d'induction mathématique. Nous étudions dans un premier temps le cas particulier des entiers, puis nous généralisons certains des résultats obtenus au cas où les constantes inductives sont définies à l'aide de constructeurs monadiques (des mots). Nous présentons des classes syntaxiques pour lesquelles nous pouvons assurer la complétude et/ou la décidabilité. Nous décrivons un outil appelé SuperInd, fondé sur le démonstrateur Prover9, implémentant les résultats précédents. Enfin, nous décrivons certaines expérimentations et procédons à des comparaisons avec d'autres approches. / We consider first order formulas where some constant symbols are defined in an inductive domain. The validity problem is not semi-decidable for these formulas. This work aims to increase the capabilities of the usual first order proof procedures (usually based on superposition and resolution calculus) to handle these particular constant symbols. Thus, we adapt the superposition calculus using a loop detection mechanism encoding a form of mathematical induction. We first consider the particular case of natural numbers, then we generalize some of these results to the case where the inductive constant symbols are defined with monadic constructors (words). We present some syntactic classes for which we can ensure completeness and/or decidability. We describe a new tool named SuperInd, based on the theorem prover Prover9, implementing our previous results. Finally we describe some experimentations and some comparisons with other approaches.

Notre société utilise de nombreux systèmes de communications. Parce que ces systèmes sont omniprésents et sont utilisés pour échanger des informations sensibles, ils doivent être protégés. Cela est fait à l'aide de protocoles cryptographiques. Il est crucial que ces protocoles assurent bien les propriétés de sécurité qu'ils affirment avoir, car les échecs peuvent avoir des conséquences importantes. Malheureusement, concevoir des protocoles cryptographiques est notoirement difficile, comme le montre la régularité avec laquelle de nouvelles attaques sont découvertes. Nous pensons que la vérification formelle est le meilleur moyen d'avoir de bonnes garanties dans la sécurité d'un protocole: il s'agit de prouver mathématiquement qu'un protocole satisfait une certaine propriété de sécurité.Notre objectif est de développer les techniques permettant de vérifier formellement des propriétés d'équivalence sur des protocoles cryptographiques, en utilisant une méthode qui fournit de fortes garanties de sécurités, tout en étant adaptée à des procédures de preuve automatique. Dans cette thèse, nous défendons l'idée que le modèle Bana-Comon pour les propriétés d'équivalences satisfait ces objectifs. Nous soutenons cette affirmation à l'aide de trois contributions.Tout d'abord, nous étayons le modèle Bana-Comon en concevant des axiomes pour les fonctions usuelles des protocoles de sécurités, et pour plusieurs hypothèses cryptographiques. Dans un second temps, nous illustrons l'utilité de ces axiomes et du modèle en réalisant des études de cas de protocoles concrets: nous étudions deux protocoles RFID, KCL et LAK, ainsi que le protocole d'authentification 5G-AKA, qui est utilisé dans les réseaux de téléphonie mobile. Pour chacun de ces protocoles, nous montrons des attaques existentes ou nouvelles, proposons des versions corrigées de ces protocoles, et prouvons que celles-ci sont sécurisées. Finalement, nous étudions le problème de l'automatisation de la recherche de preuves dans le modèle Bana-Comon. Pour cela, nous prouvons la décidabilité d'un ensemble de règles d'inférences qui est une axiomatisation correcte, bien que incomplète, de l'indistingabilité calculatoire, lorsque l'on utilise un schéma de chiffrement IND-CCA2. Du point de vue d'un cryptographe, cela peut être interprété comme la décidabilité d'un ensemble de transformations de jeux. / Our society extensively relies on communications systems. Because such systems are used to exchange sensitive information and are pervasive, they need to be secured. Cryptographic protocols are what allow us to have secure communications. It is crucial that such protocols do not fail in providing the security properties they claim, as failures have dire consequences. Unfortunately, designing cryptographic protocols is notoriously hard, and major protocols are regularly and successfully attacked. We argue that formal verification is the best way to get a strong confidence in a protocol security. Basically, the goal is to mathematically prove that a protocol satisfies some security property.Our objective is to develop techniques to formally verify equivalence properties of cryptographic protocols, using a method that provides strong security guarantees while being amenable to automated deduction techniques. In this thesis, we argue that the Bana-Comon model for equivalence properties meets these goals. We support our claim through three different contributions.First, we design axioms for the usual functions used in security protocols, and for several cryptographic hypothesis. Second, we illustrate the usefulness of these axioms and of the model by completing case studies of concrete protocols: we study two RFID protocols, KCL et LAK, as well as the 5G-AKA authentication protocol used in mobile communication systems. For each of these protocols, we show existing or new attacks against current versions, propose fixes, and prove that the fixed versions are secure. Finally, we study the problem of proof automation in the Bana-Comon model, by showing the decidability of a set of inference rules which is a sound, though incomplete, axiomatization of computational indistinguishability when using an IND-CCA2 encryption scheme. From a cryptographer's point of view, this can be seen as the decidability of a fixed set of cryptographic game transformations.

Le travail présenté dans cette thèse concerne l'étude de la notion de conversion inhérente à tous système de types dépendants. Plusieurs présentations de ces systèmes ont été étudiées pour des usages variés: typage, recherche de preuve, cohérence de logique... Chacune de ces représentation est accompagnée d'une notion d'égalité différente, suivant les besoins du moment. Mais il n'est pas certains que toutes ces représentations parlent en fin de compte d'une seule et même logique. Nous nous intéressons ici à une famille assez conséquente de systèmes de types, appelés Systèmes de Types Purs, et nous allons prouver que pour ces systèmes, toutes les représentations habituellement utilisées sont en fait équivalentes, c'est à dire qu'il existe des traductions constructives entre chacune de ces présentations. Ces traductions reposent toutes sur la manière de porter une égalité d'un système à l'autre. Ce travail se concentre donc sur les mécanismes de ces égalités, et prouve qu'il est possible de typer n'importe quelle égalité syntaxique en égalité sémantique, et ainsi qu'il est donc possible de passer d'un système à l'autre. L'intégralité de cette thèse a en outre été vérifiée et certifiée correcte à l'aide de l'assistant à la preuve Coq, qui a activement été utilisé tout au long de l'élaboration des preuves. ~

Cette thèse de doctorat étudie l'interprétation calculatoire des preuves de la logique classique. Elle présente trois calculs reflétant trois approches différentes de la question. <br /><br /> Cette thèse est donc composée de trois parties. <br /><br /> La première partie introduit le *X calcul, dont les termes représentent des preuves dans le calcul des séquents classique. Les règles de réduction du *X calcul capture la plupart des caractéristiques de l'élimination des coupures du calcul des séquents. Ce calcul introduit des termes permettant une<br />implémentation implicite de l'effacement et de la duplication. Pour autant que nous sachions, c'est le premier tel calcul pour la logique classique. <br /><br /> La deuxième partie étudie la possibilité de représenter les calculs classiques au moyen de diagrammes. Nous présentons le dX calcul, qui est le calcul diagrammatique de la logique classique, et dont les diagrammes sont issus des<br />*X-termes. La différence principale réside dans le fait que dX fonctionne à un niveau supérieur d'abstraction. Il capture l'essence des preuves du calcul des séquents ainsi que l'essence de l'élimination classique des coupures. <br /><br /> La troisième partie relie les deux premières. Elle présente le $copy;X calcul qui est une version unidimensionnelle du calcul par diagramme. Nous commencons par le *X, où nous identifions explicitement les termes qui doivent l'être. Ceux-ci<br />sont les termes qui encodent les preuves des séquents qui sont équivalentes modulo permutation de règles d'inférence indépendantes. Ces termes ont également la même représentation par diagramme. Une telle identification induit une relation de congruence sur les termes. La relation de réduction est définie modulo la congruence, et les règles de réduction correspondent à celle du dX calcul.