La vérification des protocoles cryptographiques assure qu'il n'existe pas d'attaque possible lors d'une exécution du protocole face à un certain intrus ou permet de trouver une attaque. Nous affaiblissons "l'hypothèse de chiffrement parfait" : le seul moyen d'obtenir le contenu d'un message chiffré est de connaître la clef de déchiffrement. Si un protocole est prouvé sûr sous cette hypothèse, cela est insuffisant pour assurer qu'une information confidentielle échangée sur le réseau grâce à un protocole cryptographique entre deux participants reste secrète. Un des moyens pour affaiblir cette hypothèse de chiffrement parfait est de prendre en compte certaines propriétés algébriques dans le modèle de vérification afin d'analyser de manière plus réaliste les protocoles. Nous développons une approche formelle pour la vérification de la propriété de secret d'information pour les protocoles cryptographiques en présence de théories équationnelles et de l'homomorphisme.

Avec le développement des réseaux de communications comme Internet, le besoin d'assurer la sécurité des échanges a considérablement augmenté. Les communications " sécurisées " sont réalisées par l'utilisation de petits programmes appelés protocoles cryptographiques qui peuvent être attaqués même en présence d'un chiffrement parfait. De telles failles, qualifiées de " failles logiques ", sont souvent subtiles et difficiles à déceler à la simple vue du texte du protocole. Dans cette thèse, nous poussons les limites de l'analyse des protocoles au delà de cette hypothèse. En particulier, nous proposons des procédures de décision, pour le problème de la recherche d'attaques en présence d'opérateurs satisfaisant des propriétés algébriques.

La conception d'un protocole cryptographique obéit à de nombreux impératifs : algorithmes à utiliser, propriétés à garantir, moyen d'identification, etc. Il apparaît donc régulièrement de nouveaux protocoles qu'il convient de vérifier. Malgré l'apparente simplicité, concevoir un protocole cryptographique est une tâche difficile et sujette à de nombreuses erreurs. Des failles pour certains protocoles ont été découvertes des années après leur conception. La plupart des travaux existants se basent uniformément sur l'intrus de Dolev Yao et ne se généralisent pas automatiquement à un intrus disposant de capacités supplémentaires ou différentes. Dans cette thèse, nous allons présenter un système de déduction prenant le pouvoir de l'intrus comme paramètre. De plus, les règles de protocole seront vues comme une capacité additionnelle pour l'intrus. Le résultat principal est un théorème de normalisation de preuve permettant de réduire l'espace de recherche des attaques.

Les protocoles de communication asynchrones sont naturellement modélisés par des automates communicants via des canaux FIFO non bornés. Dans cette thèse nous nous intéressons aux variantes des Lossy Channel Systems pour lesquelles les pertes de messages dans les canaux sont probabilistes. Plus précisément, on considère des sémantiques sous forme de chaînes de Markov et de processus de décision markoviens. Un théorème général de convergence de points fixes dans les systèmes de transition bien structurés, permet de prouver pour les PLCS et NPLCS de nombreux résultats de décidabilité pour la vérification de propriétés du temps linéaire. Nous donnons également les limites des modèles par l'intermédiaire de résultats d'indécidabilité. Un prototype a fait l'objet de l'implémentation des algorithmes développés dans la thèse. Malgré la grande complexité des problèmes cet outil a permis de prouver des propriétés de vivacité sur des protocoles tels que le Bit Alterné et le protocole de Pachl.

Dans le domaine des systèmes informatisés où la fiabilité est la première priorité, les méthodes formelles ont prouvé leur efficacité pour la conception de logiciels sûrs. La dépendance à de tels systèmes augmente, et les contraintes rencontrées se font plus diverses et précises, en particulier les contraintes temporelles. Certaines méthodes formelles, notamment la méthode B, rendent la conception malaisée sous de telles contraintes, puisqu'elles n'ont pas été prévues pour cela à l'origine.<br /><br />Nous nous proposons donc d'étendre la méthode B pour lui permettre de spécifier et valider des systèmes à contraintes temporelles complexes. Nous utilisons pour ce faire des calculs de durées pour exprimer la sémantique du langage B et en déduire une extension conservative qui permet de l'utiliser à la fois dans son cadre d'origine et dans le cadre de systèmes à contraintes temporelles.<br /><br />Nous nous penchons également sur le problème de l'utilisation d'un outil de preuve générique pour valider des formules de calcul des durées. La généricité de ce type d'outil répond à la multiplication des méthodes formelles, mais pose le problème de l'intégration des fondations mathématiques de ces méthodes à un outil générique. Nous proposons donc d'étudier la mise en oeuvre en plongement léger du calcul des durées dans l'assistant de preuve Coq. Nous en déduisons un retour sur expérience de la définition d'une logique modale particulière dans un outil à vocation générique.

L'objectif de cette thèse est de profiter des avantages de deux formes de modélisation complémentaires pour représenter de manière formelle les systèmes d'information (SI). Un SI est un système informatisé qui permet de rassembler les informations d'une organisation et qui fournit des opérations pour les manipuler. Les SI considérés sont développés autour de systèmes de gestion de bases de données (SGBD). Notre motivation est d'utiliser des notations et des techniques formelles pour les concevoir, contrairement aux méthodes actuelles qui sont au mieux semi-formelles. D'une part, EB3 est un langage formel basé sur les traces d'événements qui a été défini pour la spécification des SI. En particulier, EB3 met en avant le comportement dynamique du système. D'autre part, B est un langage formel basé sur les états qui se prête bien à la spécification des propriétés statiques des SI. Nous avons défini une nouvelle approche, appelée EB4, qui bénéficie à la fois des avantages d'EB3 et B. Dans un premier temps, les processus décrits en EB3 sont utilisés pour représenter et pour valider le comportement du système. Ensuite, la spécification est traduite en B pour spécifier et vérifier les principales propriétés statiques du SI. Enfin, nous avons défini des techniques de synthèse automatique de transactions BD relationnelles à partir du modèle de données d'EB3 pour compléter le cycle de développement du SI.

Les exigences qui s'appliquent aux composants logiciels et aux logiciels embarqués justifient l'utilisation des meilleures techniques disponibles pour garantir la qualité des spécifications et conserver cette qualité lors du développement du code. Les méthodes formelles, et parmi elles la méthode B, permettent d'atteindre ce niveau de qualité. Cependant, ces méthodes utilisent des notations et des concepts spécifiques, qui génèrent souvent une faible lisibilité et une difficulté d'intégration dans les processus de développement et de certification. Ainsi, proposer des environnements de spécification, de développement de programmes et de logiciels, combinant des méthodes formelles et des méthodes semi-formelles largement utilisées dans les projets industriels, en l'occurrence B et UML, s'avère d'une grande importance. Notre intérêt porte précisément sur la méthode B qui est une méthode formelle utilisée pour modéliser des systèmes et prouver l'exactitude de leur conception par raffinements successifs. Mais les spécifications formelles sont difficiles à lire quand elles ne sont pas accompagnées d'une documentation. Cette lisibilité est essentielle pour une bonne compréhension de la spécification, notamment dans des phases de validation ou de certification. Aujourd'hui, en B, cette documentation est fournie sous forme de texte, avec, quelquefois, des schémas explicitant certaines caractéristiques du système. L'objectif de ce travail de thèse est de mettre en relation des spécifications en B avec des diagrammes UML, qui constituent un standard de facto dans le monde industriel et dont le caractère graphique améliore la lisibilité. Nous avons axé notre processus de dérivation de diagrammes de classes à partir de spécifications B autour d'une technique d'ingénierie inverse guidée par un ensemble de correspondances structurelles et sémantiques spécifiées à un méta-niveau. Quant à la dérivation de diagrammes d'états/transitions, elle a été orientée vers une technique d'abstraction de graphes d'accessibilité construits par une exploration exhaustive du comportement de la spécification.

Nous etendons les logiques temporelles du temps alternant ATL et ATL* au moyen de contextes strategiques et de contraintes sur la memoire : la premiere extension permet aux agents de s'en tenir a leurs strategies lors de l'evaluation des formules, contrairement a ATL ou chaque quantificateur de strategies ecrase les strategies anterieurement selectionnees. La seconde extension permet aux quantificateurs de strategies de se restreindre aux strategies sans memoire ou avec memoire bornee. Nous avons l'etudie l'expressivite de nos logiques. Nous montrons qu'elles expriment des proprietes importantes comme l'exstence d'equilibres, et nous les comparons formellement a d'autres formalismes proches (ATL, ATL*, Game Logic, Strategy Logic, ...). Nous avons aborde les problemes de model-checking. Nous donnons un algorithme PSPACE pour la logique n'impliquant que des strategies sans memoire, et un algorithme EXPSPACE pour le cas des strategies a memoire bornee. Dans le cas general, malgre leur forte expresssivite, nous prouvons que leur model-checking reste decidable par un algorithme a base d'automates d'arbres alternants qui permet d'evaluer une formule sur la classe complete des CGS avec n joueurs.

La mobilité est une composante importante de la liberté des personnes. L'évolution des moyens technologiques y contribue au premier chef. Outre la question du transport, celle du maintien du lien entre les individus est en ce sens particulièrement prégnante. Elle a mis à rude épreuve la notion de réseaux de télécommunications puisqu'il s'agit de répondre, pour des individus éparpillés ou concentrés, mais mobiles, au besoin de rester reliés. De l'ère des réseaux analogiques à celle des réseaux numériques, de l'ère des réseaux filaires à celle des réseaux sans fil et mobiles, la technologie n'a cessé d'évoluer. Ces dernières décennies ont vu apparaître des réseaux numériques sans fil, où non seulement il y a mobilité des utilisateurs mais aussi mobilité de l'infrastructure du réseau à laquelle ils contribuent. Ces réseaux se constituent de façon spontanée. Ils se maintiennent de manière autonome. On les désigne par le terme réseaux ad hoc mobiles (en anglais Mobile Ad hoc Networks ou MANET) qui s'oppose naturellement à celui de réseaux à infrastructure. La sécurité est une préoccupation générale des êtres humains. Ils en ressentent aussi le besoin en matière de réseaux. Ce besoin est particulièrement criant lorsque sont échangées des données critiques, financières ou stratégiques. La confidentialité des échanges, l'authentification des sources, l'assurance d'intégrité, la prévention de la récusation sont autant d'objectifs qu'il faut alors atteindre. Diverses solutions de sécurité ont été conçues dans cette optique pour les réseaux filaires puis ont ensuite été adaptées aux réseaux sans-fil et mobiles. Les architectures AAA (Authentication, Authorization, Accounting) en font partie. Elles sont en général utilisées dans un contexte commercial. Tant par leur facilité de déploiement que par la baisse des coûts de mise en œuvre qu'ils engendrent, les réseaux ad hoc mobiles, après avoir bien servi dans le domaine militaire, semblent avoir un avenir dans les applications commerciales. C'est pourquoi, nous nous proposons dans cette thèse de concevoir une architecture AAA adaptée aux spécificités de ces réseaux. Nous étudions d'abord les réseaux ad hoc mobiles et leurs caractéristiques. Ensuite, nous présentons les solutions de sécurité qui existent dans les réseaux à infrastructure. Nous examinons, en particulier, les solutions qui permettent le contrôle d'accès et dont sont engendrées les architectures AAA. Les solutions AAA proposées pour les MANETs sont par la suite analysées et classifiées afin de déterminer les manques et les vulnérabilités. Cette étude approfondie nous amène à proposer une architecture AAA répondant aux attentes identifiées. C'est une architecture distribuée qui répond, en particulier, au besoin d'autonomie des opérations dans les MANETs et où les protocoles exécutés peuvent impliquer simultanément plus de deux parties. Un ensemble de protocoles et de mécanismes d'authentification et d'autorisation s'intégrant avec la suite des protocoles IPv6 a été proposé. Leur sécurité a été discutée. Celle, en particulier du protocole d'authentification a fait l'objet de validation formelle. Contrairement aux protocoles utilisés dans la phase d'autorisation des services AAA proposés, le mode de communication multi-parties et multi-sauts du protocole d'authentification nous a poussé à mener une analyse approfondie de ses performances. Pour cela, nous avons eu recours, dans un premier temps, à la modélisation au moyen de calculs mathématiques explicites ensuite à la simulation. Les résultats obtenus montrent que ce protocole passe à l'échelle d'un MANET comprenant au moins cent nœuds. Dans certaines conditions d'implémentation que nous avons définies, ses performances, tant celle liée à sa probabilité de terminaison avec une issue favorable que celle portant sur son temps d'exécution, atteignent des valeurs optimales.

Cette thèse propose une nouvelle approche du parallélisme et de la concurrence, posant les bases d'un langage de programmation à la fois sûr et "secure" (garantissant la sécurité des données), fondé sur une sémantique formelle claire et simple, tout en étant adapté aux architectures multi-cœur. Nous avons adopté le paradigme synchrone, dans sa variante réactive, qui fournit une alternative simple à la programmation concurrente standard en limitant l'impact des erreurs dépendant du temps ("data-races"). Dans un premier temps, nous avons considéré un langage réactif d'orchestration, DSL, dans lequel on fait abstraction de la mémoire (Partie 1). Dans le but de pouvoir traiter la mémoire et la sécurité, nous avons ensuite étudié (Partie 2) un noyau réactif, CRL, qui utilise un opérateur de parallélisme déterministe. Nous avons prouvé la réactivité bornée des programmes de CRL. Nous avons ensuite équipé CRL de mécanismes pour contrôler le flux d'information (Partie 3). Pour cela, nous avons d'abord étendu CRL avec des niveaux de sécurité pour les données, puis nous avons défini dans le langage étendu, SSL, un système de types permettant d'éviter les fuites d'information. Parallèlement (Partie 4), nous avons ajouté la mémoire à CRL, en proposant le modèle DSLM. En utilisant une notion d'agent, nous avons structuré la mémoire de telle sorte qu'il ne puisse y avoir de "data-races". Nous avons également étudié l'implémentation de DSLM sur les architectures multi-cœur, fondée sur la notion de site et de migration d'un agent entre les sites. L'unification de SSL et de DSLM est une piste pour un travail futur.