Faculté informatique et communications IC, Département de systèmes de communication, Institut de systèmes de communication ISC (Laboratoire pour les communications informatiques et leurs applications 1 LCA1)

Building blocks for secure services : authenticated key transport and rational exchange protocols

Buttyán, Levente ; Hubaux, Jean-Pierre (Dir.)

Thèse sciences Ecole polytechnique fédérale de Lausanne EPFL : 2001 ; no 2511.

Ajouter à la liste personnelle
    Summary
    This thesis is concerned with two security mechanisms: authenticated key transport and rational exchange protocols. These mechanisms are potential building blocks in the security architecture of a range of different services. Authenticated key transport protocols are used to build secure channels between entities, which protect their communications against eaves-dropping and alteration by an outside attacker. In contrast, rational exchange protocols can be used to protect the entities involved in an exchange transaction from each other. This is important, because often the entities do not trust each other, and both fear that the other will gain an advantage by misbehaving. Rational exchange protocols alleviate this problem by ensuring that a misbehaving party cannot gain any advantages. This means that misbehavior becomes uninteresting and it should happen only rarely. The thesis is focused on the construction of formal models for authenticated key transport and rational exchange protocols. In the first part of the thesis, we propose a formal model for key transport protocols, which is based on a logic of belief. Building on this model, we also propose an original systematic protocol construction approach. The main idea is that we reverse some implications that can be derived from the axioms of the logic, and turn them into synthesis rules. The synthesis rules can be used to construct a protocol and to derive a set of assumptions starting from a set of goals. The main advantage is that the resulting protocol is guaranteed to be correct in the sense that all the specified goals can be derived from the protocol and the assumptions using the underlying logic. Another important advantage is that all the assumptions upon which the correctness of the protocol depends are made explicit. The protocol obtained in the synthesis process is an abstract protocol, in which idealized messages that contain logical formulae are sent on channels with various access properties. The abstract protocol can then be implemented in several ways by replacing the idealized messages and the channels with appropriate bit strings and cryptographic primitives, respectively. We illustrate the usage of the logic and the synthesis rules through an example: We analyze an authenticated key transport protocol proposed in the literature, identify several weaknesses, show how these can be exploited by various attacks, and finally, we redesign the protocol using the proposed systematic approach. We obtain a protocol that resists against the presented attacks, and in addition, it is simpler than the original one. In the second part of the thesis, we propose an original formal model for exchange protocols, which is based on game theory. In this model, an exchange protocol is represented as a set of strategies in a game played by the protocol parties and the network that they use to communicate with each other. We give formal definitions for various properties of exchange protocols in this model, including rationality and fairness. Most importantly, rationality is defined in terms of a Nash equilibrium in the protocol game. The model and the formal definitions allow us to rigorously study the relationship between rational exchange and fair exchange, and to prove that fairness implies rationality (given that the protocol satisfies some further usual properties), but the reverse is not true in general. We illustrate how the formal model can be used for rigorous verification of existing protocols by analyzing two exchange protocols, and formally proving that they satisfy the definition of rational exchange. We also present an original application of rational exchange: We show how the concept of rationality can be used to improve a family of micropayment schemes with respect to fairness without substantial loss in efficiency. Finally, in the third part of the thesis, we extend the concept of rational exchange, and describe how similar ideas can be used to stimulate the nodes of a self-organizing ad hoc network for cooperation. More precisely, we propose an original approach to stimulate the nodes for packet forwarding. Like in rational exchange protocols, our design does not guarantee that a node cannot deny packet forwarding, but it ensures that it cannot gain any advantages by doing so. We analyze the proposed solution analytically and by means of simulation.
    Résumé
    Cette thèse de doctorat porte sur l'étude de deux mécanismes de sécurité: le transport authentifié de clés cryptographiques et les protocoles d'échange rationnel. Ces mécanismes pourraient être utilisés comme blocs servant à construire des architectures sécuritaires pour différents types de services. Ainsi, les protocoles de transport authentifié de clés cryptographiques sont-ils employés pour construire des canaux sécurisés entre les entités, protégeant leurs transmissions des attaques extérieures aussi bien passives qu'actives. Les protocoles d'échange rationnel quant à eux peuvent être employés pour protéger les entités impliquées dans une transaction les uns des autres. Ce dernier point est important car, souvent, les différentes parties ne se font pas confiance, chacun craignant que l'autre triche pour augmenter ses gains. Les protocoles d'échange rationnel allègent ce problème en garantissant qu'un tricheur ne gagne rien à se comporter de la sorte. Ceci signifie que mal agir devient inintéressant et qu'il ne devrait donc se produire que rarement. Dans la présente thèse, on va mettre l'accent sur la construction des modèles formels pour le transport authentifié de clés cryptographiques et les protocoles d'échange rationnel. Dans la première partie de cette thèse, nous proposons un modèle formel pour les protocoles de transport authentifié, basé sur une logique de croyance. En s'appuyant sur ce modèle, nous proposons également une approche originale pour la construction systématique de protocoles. L'idée principale consiste à inverser des implications qui peuvent être dérivées des axiomes de la logique et les transformer en règles de synthèse. Ces règles de synthèse peuvent être employées pour construire un protocole et pour obtenir des hypothèses à partir d'un ensemble de buts qu'on désire atteindre. L'avantage principal d'une telle méthode est l'assurance que le protocole résultant est correct dans le sens où tous les buts indiqués peuvent être déduits du protocole et des hypothèses en utilisant la logique que nous avions définie. Un autre avantage important réside dans le fait que les hypothèses permettant d'atteindre les buts recherchés sont explicites. Le protocole résultant est un protocole abstrait, dans lequel les messages idéalisés qui contiennent des formules logiques sont envoyés via des canaux ayant diverses propriétés d'accès. Le protocole abstrait peut alors être implémenté de plusieurs manières, en remplaçant les messages idéalisés et les canaux, respectivement, par les chaînes binaires et les primitives cryptographiques appropriées. Nous illustrons l'utilisation de la logique et des règles de synthèse par un exemple: Nous analysons un protocole de transport de clés authentifié proposé dans la littérature, y identifions des faiblesses, montrons comment celles-ci peuvent être exploitées dans diverses attaques, et finalement remodelons le protocole en utilisant notre approche systématique. Nous obtenons un protocole qui résiste aux attaques précédemment identifiées, et qui plus est, représente un niveau de complexité inférieur au protocole initial. Dans la deuxième partie de la thèse, nous proposons un modèle formel original pour les protocoles d'échange, basé sur la théorie des jeux. Dans ce modèle, un protocole d'échange est représenté comme un ensemble de stratégies dans un jeu auquel participent les différentes parties impliquées dans le protocole ainsi que le réseau qu'ils utilisent pour communiquer entre eux. Nous donnons dans ce modèle des définitions formelles des différentes propriétés des protocoles d'échange telles que la rationalité et l'équité. La rationalité est définie en termes d'équilibre de Nash. Le modèle et les définitions formelles nous permettent d'étudier rigoureusement le rapport entre l'échange rationnel et l'échange équitable, et de montrer qu'équité implique rationalité (à condition que le protocole satisfasse certaines autres propriétés usuelles), mais que l'inverse n'est pas vrai en général. Nous montrons comment le modèle formel peut être utilisé pour la vérification rigoureuse des protocoles existants en analysant deux protocoles d'échange, et en montrant formellement qu'ils satisfont la définition de l'échange rationnel. Nous présentons également une application originale d'échange rationnel: Nous montrons comment le concept de la rationalité peut être employé à améliorer une classe de schémas de micro-paiements, en termes l'équité, sans perte substantielle d'efficacité. Finalement, dans la dernière partie de cette thèse, nous étendons le concept de l'échange rationnel et décrivons comment des idées similaires peuvent être employées pour stimuler la coopération dans les réseaux ad hoc auto-organisateurs. Plus précisément, nous proposons une approche originale pour inciter les noeuds à relayer les paquets dans les réseaux ad hoc. Comme pour les protocoles d'échange rationnel, notre conception ne garantit pas qu'un noeud accepte toujours de relayer les paquets pour les autres, mais il nous assure au moins que ce noeud ne gagne rien en agissant de la sorte. Nous étudions la solution proposée analytiquement et au moyen de simulations.