Thèse de doctorat : Informatique : Paris 12 : 2005. Thèse de doctorat : Informatique : Oldenburg, Carl v. Ossietzky Universität : 2005. / Thèse soutenue en co-tutelle. Titre provenant de l'écran-titre. Bibliogr. p. 166173. Index.

Cette thèse se situe dans le cadre de l'analyse symbolique des protocoles Les contributions sont représentées par l'obtention de résultats de décidabilité et de transfert dans les directions suivantes qui sont des thèmes majeurs en vérification des protocoles : - traitement des primitives cryptographiques : chiffrement CBC, signatures en aveugle; - propriétés de sécurité : secret fort, existence de cycles de clefs; - approches pour la sécurité : construction de protocoles sûrs. Ainsi, nous avons montré la décidabilité (d'une part) de l'existence de cycles de clefs et (d'autre part) du secret pour des protocoles utilisant le mode de chiffrement CBC ou des signatures en aveugle. Nous avons aussi transféré la sécurité des protocoles d'un cadre faible vers un cadre plus fort dans les sens suivants. D'une part, nous avons montré qu'une propriété de secret faible implique sous certaines hypothèses une propriété de secret plus forte. D'une autre part, nous avons construit des protocoles sûrs à partir de protocoles ayant des propriétés plus faibles. / This thesis is developed in the framework of the symbolic analysis of security protocols. The contributions are represented by decidability and transfer results in the following directions which are major topics in protocol verification: - treatment of the cryptographic primitives: CBC encryption, blind signatures; - security properties: strong secrecy, existence of key cycles; - approaches for protocol security: construction of the secure protocols. Thus, we showed the decidability (on the one hand) of the existence of key cycles for a bounded number of sessions using a generalized constraint system approach, and (on the other hand) of secrecy for protocols using the CBC encryption or blind signatures for an unbounded number of sessions by using a refined resolution strategy on a new fragment of Horn clauses. We also transferred protocol security from a weak framework towards a stronger framework in the following directions. On the one hand, we showed that a weak property of secrecy (i.e. reachability-based secrecy) implies under certain well-motivated assumptions a stronger secrecy property (i.e. equivalence-based secrecy). On the other hand, we built protocols secure against active adversaries considering an unbounded number of sessions, by transforming protocols which are secure in a non-adversarial setting.

Cette thèse se consacre à l'application de techniques de réalisabilité dans le cadre de l'étude du sens calculatoire de la logique. Dans une première partie, nous rappelons le formalisme de la réalisabilité classique de Krivine, dans lequel nous menons ensuite une étude du contenu opérationnel de tautologies purement classiques. Cette exploration du sens calculatoire de la disjonction classique révèle des comportements riches, avec une forte intuition interactive, qui s'interprètent avantageusement comme des structures de contrôle typées. Afin de mieux comprendre la nature de ces mécanismes, nous définissons ensuite une technique de réalisabilité à la Krivine pour un modèle de calcul concurrent, dans le but d'obtenir une notion de constructivité qui ne soit plus fondée sur l'idée de fonction, mais sur celle de processus interactif. Le cadre ainsi obtenu donne une interprétation réellement concurrente de la logique linéaire dans un calcul de processus dérivé du pi-calcul, permettant d'appliquer au cas concurrent la méthode de spécification précédemment étudiée dans le cas séquentiel. Par la suite, l'étude des traductions de la logique classique vers la logique linéaire mène à reconstruire systématiquement des décompositions interactives du calcul fonctionnel, permettant ainsi de faire le lien au niveau logique entre les réalisabilités classique et concurrente. Dans une dernière partie, nous étudions plus en détail le mode de calcul issu des algèbres de processus, afin de comprendre son système d'ordonnancement. Cette étude mène à la définition d'un modèle de calcul plus géométrique qui permet une exploration formelle de la notion de causalité dans les calculs concurrents.

Le calcul réparti est de plus en plus utilisé bien qu'il reste très mal maîtrisé. Cette thèse porte sur le Dpi-calcul, une extension simple du pi-calcul dans laquelle tous les processus sont placés dans des localités afin de décrire leur répartition. Dans ce calcul, les processus peuvent communiquer localement et migrer entre localités. À côté des canaux de communication et des localités, on identifie une nouvelle famille d'identifiants, les passeports, permettant un contrôle fin des migrations de processus : un processus doit disposer d'un passeport adéquat pour entrer dans une localité.<br /><br />Afin de structurer le calcul, on met en place un système de types qui associe un type à chaque identifiant pour vérifier qu'un processus n'utilise que les droits qu'il possède. L'ordre de sous-typage sur les types est étendu aux types de passeports suivant les localités d'origine des processus migrant. On démontre que cet ordre admet des bornes inférieures sous certaines conditions. On prouve également que les processus se conformant à cette politique de typage conservent cette propriété au cours de leurs réductions.<br /><br />On étudie aussi l'équivalence observationnelle : quand des processus exhibent-ils des comportements indiscernables pour un observateur ? En présence de passeports, il est indispensable d'imposer à l'observateur d'être loyal, c'est-à-dire d'exiger la possession de passeports pour observer les communications ayant lieu dans les localités correspondantes. Ces contraintes définissent une congruence dite barbue loyale. On développe ensuite un système de transitions étiquetées tel que la bisimilarité loyale engendrée coïncide avec cette congruence barbue loyale.

Durant leur exécution, les systèmes concurrents manipulent diverses ressources dynamiques en nombre : fichiers, liens de communication, mémoire, etc. Les propriétés comportementales de ces systèmes sont alors étroitement liées aux manipulations de ces ressources qu'ils allouent, utilisent, puis détruisent. Nous proposons dans cette thèse une analyse quantitative, effectuée de manière statique, de ce type de ressources pour les systèmes concurrents et dynamiques. Les systèmes que l'on considère peuvent être des programmes concurrents et parallèles (le langage Piccolo développé dans le cadre de ce travail en est un exemple), ou encore la modélisation de systèmes plus généraux. Pour atteindre cette généricité, notre travail repose fortement sur les algèbres de processus, et plus particulièrement sur le pi-calcul pour lequel nous proposons une variante sémantique ainsi que plusieurs abstractions adaptées à l'observation des ressources en particulier. Le socle théorique de notre analyse est présenté sous la forme d'un nouveau type d'automates nominaux : les nu-automates. Ils permettent de raisonner spécifiquement sur les ressources dynamiques, tant pour caractériser les notions quantitatives de consommation en ressources que pour de futures analyses qualitatives. À partir de ce formalisme nous réalisons ensuite un ensemble d'algorithmes ayant pour but de mettre en oeuvre les résultats introduits sur les nu-automates. Enfin, nous proposons plusieurs expérimentations, sur la base d'exemples classiques du pi-calcul, de notre prototype d'analyse de ressources. / Concurrent activities involve undoubtedly many dynamic resources manupulations: files, communication links, memory, etc. Then, the behavioral properties of such systems are closely linked to their usage of those resources that they allocate, use, and finally destroy. In this work, we develop a quantitative static analysis of concurrent and parallel systems for this kind of resources. Systems that we consider can be concurrent and parallel programs (written for example in the Piccolo programming language which was developped during this thesis), or models descriptions of more general systems. To be generic, our work lies on process algebra, specifically pi-calculs for which we propose a variant semantics in addition to several resources abstractions strategies. The underlying theory is developped as a nominal automata framework (namely the nu-automata). They allow one to reason about dynamic resources usage to charaterize both quantitative and qualitative properties. From this formalism we establish an algorithmic framework that enforce the qualitative results defined on nu-automata. Finally, our resources abstractions and resources analysis are tested experimentally on classical pi-calculus examples using our prototype analysis tool.

Cette thèse se situe dans le cadre de l'analyse symbolique des protocoles Les contributions sont représentées par l'obtention de résultats de décidabilité et de transfert dans les directions suivantes qui sont des thèmes majeurs en vérification des protocoles :<ul><li>traitement des primitives cryptographiques : chiffrement CBC, signatures en aveugle;</li><li>propriétés de sécurité : secret fort, existence de cycles de clefs;</li><li>approches pour la sécurité : construction de protocoles sûrs.</li></ul>Ainsi, nous avons montré la décidabilité (d'une part) de l'existence de cycles de clefs et (d'autre part) du secret pour des protocoles utilisant le mode de chiffrement CBC ou des signatures en aveugle. Nous avons aussi transféré la sécurité des protocoles d'un cadre faible vers un cadre plus fort dans les sens suivants. D'une part, nous avons montré qu'une propriété de secret faible implique sous certaines hypothèses une propriété de secret plus forte. D'une autre part, nous avons construit des protocoles sûrs à partir de protocoles ayant des propriétés plus faibles.

La logique linéaire fait désormais partie des outils standards en théorie de la démonstration et, de manière plus générale, dans l'étude de la correspondance de Curry-Howard. Nous présentons ici trois directions importantes d'application de méthodes issues de la logique linéaire : - la théorie de la démonstration de la logique classique et ses aspects calculatoires via notamment la sémantique des jeux ; - la complexité implicite à travers les modèles dénotationnels des logiques linéaires à complexité bornée ; - la théorie de la concurrence et ses fondements logiques grâce aux ingrédients apportés par la logique linéaire différentielle. Les approches linéaires offrent ainsi un cadre commun pour l'étude de différents aspects logiques du calcul.