Les protocoles de sécurité sont des programmes informatiques qui définissent des règles d'échange entre les points d'un réseau et permettent de sécuriser les communications. Ils sont utilisés par exemple dans les distributeurs de billets, les abonnements aux chaînes de télévision payantes, la téléphonie mobile, le commerce électronique. Leur objectif est de garantir le secret d'une donnée, d'authentifier un des participants, de garantir l'anonymat ou la non-répudiation, etc. Ces programmes sont exécutés sur des réseaux ouverts facilement accessibles (comme internet). Aussi, pour démontrer qu'ils remplissent bien leurs objectifs, il est nécessaire de prendre en compte les attaques dont ils peuvent faire l'objet. L'objet de mon mémoire d'habilitation à diriger des recherches est de montrer que les méthodes formelles peuvent être utilisées avec succès pour entreprendre une analyse fine des protocoles cryptographiques, à travers une palette variée d'outils. Nous présentons des procédures pour déterminer de façon automatique si un protocole est sûr. Nous avons proposés différents algorithmes en fonction des propriétés de sécurité considérées ainsi que des primitives cryptographiques utilisées (chiffrement, signature, hachage, ou exclusif, etc.). D'autre part, nous caractérisons des conditions qui permettent de combiner les résultats précédents et de concevoir les protocoles de façon modulaire. Ces résultats se basent sur des modèles symboliques, très différents de ceux utilisés en cryptographie où la notion de sécurité est basée sur la théorie de la complexité. Cette notion de sécurité est mieux adaptée pour identifier toutes les attaques possibles dans la réalité mais, en contrepartie, les (lourdes) preuves de sécurité sont effectuées à la main et semblent difficilement automatisables. Nous avons identifié des hypothèses cryptographiques qui permettent de relier les approches cryptographiques et symboliques. Il est alors possible d'obtenir des preuves de sécurité à un niveau cryptographique, directement à partir des preuves établies (automatiquement) dans un cadre symbolique.

Les logiques modales sont des logiques permettant la représentation et l'inférence de connaissances. La logique hybride est une extension de la logique modale de base contenant des nominaux, permettant de faire référence à un unique individu ou monde du modèle. Dans cette thèse nous présentons plusieurs algorithmes de tableaux pour logiques hybrides expressives. Nous présentons aussi une implémentation de ces calculs, et nous décrivons les tests de correction et de performance que nous avons effectués, ainsi que les outils les permettant. De plus, nous étudions en détail une famille particulière de logiques liée aux logiques hybrides : les logiques avec opérateurs de comptage. Nous étudions la complexité et la décidabilité de certains de ces langages / Modal logics are logics enabling representing and inferring knowledge. Hybrid logic is an extension of the basic modal logic that contains nominals which enable to refer to a single individual or world of the model. In this thesis, we present several tableaux-based algorithms for expressive hybrid logics. We also present an implementation of these calculi and we describe correctness and performance tests we carried out, and the tools that enable these. Moreover, we study a particular family of logics related to hybrid logics: logics with counting operators.We investigate previous results, and study the complexity and decidability of certain of these languages

Cette thèse se divise en trois parties. Dans l'introduction, nous rappelons d'abord les problèmes et les motivations philosophiques a l'origine de l'étude des logiques polyvalentes. Nous élaborons une methode qui permet d'obtenir mécaniquement a partir de la définition matricielle d'une logique, des règles d'inférence pour les connecteurs propositionnels d'un calcul des tableaux. Un traitement similaire est fait pour les règles d'inférence pour les quantificateurs. Le raffinement étudie alors est une skolemisation paresseuse. Elle permet l'utilisation de l'unification pour calculer les instances utiles a la construction d'un tableau ferme. Une implémentation dans atinf les concrétise. Nous proposons les logiques polyvalentes avec égalité graduelle, un calcul par resolution-paramodulation ordonnées. La première partie finit par une extension qui consiste a munir les valeurs de vérité de structures de treillis ou de treillis bi-dimensionnels. Au traitement systématique des logiques finies suit une étude de deux cas typiques de logiques polyvalentes infinies du premier ordre une étude systématique étant théoriquement impossible : les logiques de post et de Ukasiewicz. Le lien entre les logiques de Horn et les logiques de post est utilise, pour proposer une automatisation des logiques de post basée sur une sémantique des mondes possibles. A partir de cette sémantique nous définissons un calcul des tableaux préfixes. Afin d'augmenter l'efficacité, des contraintes, résolues en temps polynomial sur les préfixes sont introduites. Chaque développement inclut une étude bibliographique très documentée du domaine de la logique mathématique, de l'intelligence artificielle et de la déduction automatique

Le domaine de cette thèse est la déduction automatique, c.-à-d. le développement d'algorithmes dont le but est de prouver automatiquement des conjectures mathématiques. Dans cette thèse, les conjectures que nous voulons prouver appartiennent à une extension de la logique propositionnelle, appelée "schémas de formules". Ces objets permettent de représenter de façon finie une infinité de formules propositionnelles (de même que, p.ex., les langages réguliers permettent de représenter de façon finie des ensembles infinis de mots). Démontrer un schéma de formules revient alors à démontrer (en une fois) l'infinité de formules qu'il représente. Nous montrons que le problème de démontrer des schémas de formules est indécidable en général. La suite de la thèse s'articule autour de la définition d'algorithmes essayant tout de même de prouver automatiquement des schémas (mais, bien sûr, qui ne terminent pas en général). Ces algorithmes nous permettent d'identifier des classes décidables de schémas, c.-à-d. des classes pour lesquelles il existe un algorithme qui termine sur n'importe quelle entrée en répondant si le schéma est vrai ou pas. L'un de ces algorithmes a donné lieu à l'implémentation d'un prototype. Les méthodes de preuves présentées mélangent méthodes de preuve classiques en logique propositionnelle (DPLL ou tableaux sémantiques) et raisonnement par récurrence. Le raisonnement par récurrence est effectuée par l'utilisation de "preuves cycliques", c.-à-d. des preuves infinies dans lesquelles nous détectons des cycles. Dans ce cas, nous pouvons ramener les preuves infinies à des objets finis, ce que nous pouvons appeler des "schémas de preuves".

Cette thèse porte sur la vérification des règles ajoutées de l'Atelier B en utilisant une plate-forme appelée BCARe qui repose sur un plongement de la théorie sous-jacente à la méthode B (théorie de B) dans l'assistant à la preuve Coq. En particulier, nous proposons trois approches pour prouver la validité d'une règle, ce qui revient à prouver une formule exprimée dans la théorie de B. Ces trois approches ont été évaluées sur les règles de la base de règles de SIEMENS IC-MOL. La première approche dite autarcique est développée avec le langage de tactiques de Coq Ltac. Elle repose sur une première étape qui consiste à déplier tous les opérateurs ensemblistes pour obtenir une formule de la logique du premier ordre. Puis nous appliquons une procédure de décision qui met en oeuvre une heuristique naïve en ce qui concerne les instanciations. La deuxième approche, dite sceptique,appelle le prouveur automatique de théorèmes Zenon après avoir effectué l'étape de normalisation précédente. Nous vérifions ensuite les preuves trouvées par Zenon dans le plongement profond de B en Coq. La troisième approche évite l'étape de normalisation précédente grâce à une extension de Zenon utilisant des règles d'inférence spécifiques à la théorie de B. Ces règles sont obtenues grâce à la technique de superdéduction. Cette dernière approche est généralisée en une extension de Zenon à toute théorie grâce à un calcul dynamique des règles de superdéduction. Ce nouvel outil, appelé Super Zenon, peut par exemple prouver des problèmes issus de la bibliothèque de problèmes TPTP.

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.

Dans une première partie, nous montrons qu'il est possible d'établir une correspondance naturelle entre les preuves en déduction naturelle de la validité d'une formule et les réfutations par resolution d'un ensemble de clauses obtenues en appliquant a la négation de cette formule une mise sous forme clausale non standard utilisant une technique de renommage. En particulier, nous montrons qu'il est possible de simuler le fonctionnement d'un calcul des sequents proche de celui de Gentzen par la resolution et nous montrons comment traduire des réfutations par resolution en preuve en déduction naturelle. De plus, nous proposons plusieurs ameliorations de cette mise sous forme clausale avec renommage permettant de faciliter la recherche d'une réfutation par resolution. Dans une deuxième partie, nous décrivons en détail des techniques permettant une mise en œuvre efficace de la resolution avec sortes ordonnées ainsi qu'un principe d'indexation des clauses permettant de résoudre efficacement de nombreux problèmes-clés (tels ceux poses par la subsomption, l'utilisation de systèmes de réécriture...). Ces algorithmes ont ete utilises dans l'implémentation d'un démonstrateur par resolution que nous avons réalisé dans le cadre d'atinf

Il existe de nombreux démonstrateurs automatiques qui effectuent des raisonnements modulo une théorie équationnelle, c'est-à-dire enconsidérant non pas des termes, mais des classes d'équivalence de termes. En général, les travaux accomplis dans ce domaine ont pour but de concevoir des techniques pour faire de la déduction modulo une théorie particulière. Dans [Avenhaus & Plaisted, 2001], Jürgen Avenhaus et David Plaisted ont cherché à déterminer des techniques qui pourraient être employées dans le traitement non plus d'une théorie particulière, mais de toute une classe de théories équationnelles: les théories permutatives. Les auteurs ont introduit les notions de terme stratifié et d'ensemble stratifié, et décrit les procédures qui devraient être implémentées dans un démonstrateur automatique basé sur ces termes stratifiés. Les propriétés de régularité de ces théories font qu'il est possible d'employer des techniques efficaces de théorie algorithmique des groupes pour les traiter. Les auteurs espéraient que l'efficacité de ces techniques contrebalancerait le nombre élevé de clauses qui pourraient être générées dans un démonstrateur automatique basé sur ces termes stratifiés. Cependant, les algorithmes proposés pour faire de la déduction avec des termes stratifiés sont basés sur une énumération explicite des éléments des groupes, et sont donc exponentiels. Dans ce mémoire, nous développons les travaux d'Avenhaus et Plaisted, et modifions leur formalisme pour pouvoir faire l'usage le plus intensif possible des techniques de théorie algorithmique des groupes.

Nous étudions des méthodes de recherche simultanée de refutation et de modèle. Nous proposons une méthode pour la construction de modèles finis réduisant de façon importante l'espace de recherche des approches existantes. Nous nous intéressons ensuite à la recherche de modèles infinis. Nous étendons les méthodes RAMC (Refutation And Model Construction) et RAMCET (Refutation And Model Construction with Equational Tableaux) définie par R. Caferra et N. Zabel en introduisant de nouvelles règles et stratégies. Ces extensions augmentent strictement les capacités de la méthode, à la fois pour la recherche de preuve et de contre-exemple. Nous montrons que les méthodes proposées sont des procédures de décision uniforme pour une large clase de formules logiques. Ensuite, nous proposons et étudions de nouveaux formalismes pour représenter les modèles: les termes avec exposants entiers et les automates d'arbres. Nous prouvons la décidabilité de la théorie du premier ordre sur les termes avec exposants. Nous proposons également une nouvelle approche pour la découverte et l'utilisation de l'analogie en recherche simultanée de preuve et de contre-exemple et nous montrons comment utiliser la méthode RAMC en Programmation Logique (pour étendre les capacités des interpréteurs, détecter, voire corriger des erreurs dans les programmes etc.). Enfin, nous décrivons le système RAMC-ATINF implémentant certaines des idées proposées et nous donnons quelques résultats expérimentaux.

Les logiques modales sont des logiques permettant la représentation et l'inférence de connaissances. La logique hybride est une extension de la logique modale de base contenant des nominaux, permettant de faire référence à un unique individu ou monde du modèle. Dans cette thèse nous présentons plusieurs algorithmes de tableaux pour logiques hybrides expressives. Nous présentons aussi une implémentation de ces calculs, et nous décrivons les tests de correction et de performance que nous avons effectués, ainsi que les outils les permettant. De plus, nous étudions en détail une famille particulière de logiques liée aux logiques hybrides : les logiques avec opérateurs de comptage. Nous étudions la complexité et la décidabilité de certains de ces langages.