Th. doct.--Paris--ENST, 1989. / Bibliogr. p. 159-166.

Le maintien des personnes à domicile est une perspective sérieusement envisagée dans le contexte actuel de vieillissement de la population. Selon les statistiques, près d'un habitant sur trois aurait plus de 60 ans en 2050, contre un sur cinq en 2005. Cependant, les solutions actuelles de téléassistance (bouton alarme sur un collier par exemple) ont montré leurs limites. La thèse consiste à étudier des applications du futur permettant de fournir à une personne maintenue à domicile ou à l’hôpital une meilleure solution alternative fondée sur les réseaux de capteurs, capable de mesurer certains de ses paramètres physiologiques et de transmettre des données importantes aux infirmières ou médecins. Ces applications doivent s’adapter aux besoins médicaux et avoir un coût économique faible. Nous nous sommes focalisés sur des solutions de type réseaux de capteurs qui ont un coût de développement et de mise en œuvre faibles. Ce type de réseaux de capteurs offre de nouveaux services tels que la surveillance médicale et l'amélioration de la sécurité par la propagation d'alertes d'urgence. Cependant, la forte mobilité et le changement rapide de la topologie du réseau présentent un verrou scientifique et social. En outre, l'interférence de différents capteurs augmente la difficulté d'implantation de ce genre de réseaux IEEE 802.15.4. Depuis ces dernières années, plusieurs solutions ont été étudiées, comme nous le verrons dans cette thèse. Nous nous intéressons à la fiabilité de transmission dans cette thèse, car un réseau de capteurs est très limité par la capacité de calcul, de stockage et de transfert. Nous nous interrogeons dans un premier temps sur la meilleure méthode pour la livraison des données. Nous avons sélectionné les protocoles unicast et multicast issus du domaine MANET dans le but de comparer leurs avantages et inconvénients dans le contexte des applications de surveillance médicale. Nous nous sommes intéressés aux mécanismes de mise en place et au renforcement de la route dans chacun des protocoles. Les résultats de cette première étude montrent que les protocoles multicast s’adaptent mieux aux applications, car ils permettent de réduire le nombre de paquets transmis dans le réseau. Même si certains protocoles pourraient amener une meilleure performance (en ce qui concerne le débit utile) que d’autres, aucun protocole ne satisfait une application réelle. Nous travaillons sur l’exploitation d'un réseau hétérogène en distinguant les nœuds forts et les nœuds faibles. Dans ce cadre, nous avons proposé une nouvelle approche, HMR, qui permet de mieux assurer la performance du réseau par rapport aux solutions existantes. Une dernière problématique à étudier dans cette thèse est l’agrégation de données, car les données à transmettre dans le réseau sont souvent périodiquement générées avec des tailles très restreintes (quelques octets, par exemple). Nos études montrent que l’agrégation de données est une bonne solution. Cette thèse a donné lieu à deux publications en conférences internationales avec comité de lecture. / Keeping people at home is a perspective seriously considered in the current context of population aging. According to statistics, nearly one in three would have more than 60 years in 2050, against one in five in 2005. However, current solutions telecare (alarm button on a necklace, for example) have shown their limits. The thesis consists in studying future applications to provide, to a person kept at home or in the hospital, a better alternative solution based on sensor networks. A solution capable of measuring some of its physiological parameters and transmit important data nurses or doctors. These applications must adapt to the medical needs and have a low economic cost. We focused on solutions for sensor networks having a low-cost of development and implementation. This type of sensor networks offer new services such as medical monitoring and improving security by the propagation of emergency alerts. However, the high mobility and rapid change of the network topology present a scientific and social lock. Furthermore, interference of various sensors increases the difficulty of implantation of such networks IEEE 802.15.4. In recent years, several solutions have been studied, as discussed in this thesis. We are interested in the transmission reliability in this thesis, as a sensor network is very limited computing capacity, storage and transfer. We inquire in the first instance on the best method for data delivery. We selected unicast and multicast protocols from the field MANET in order to compare their advantages and disadvantages in the context of medical monitoring applications. We are interested in mechanisms of implementation and strengthening of the route in each of the protocols. The results of this first study show that the multicast protocols are better suited to these applications because they reduce the number of packets transmitted in the network. Although some protocols may lead to better performance (as regards the throughput) than others, no protocol satisfies a real application. We are working on the operation of a heterogeneous network distinguishing between strong and weak nodes. In this context, we proposed a new approach, HMR, to better ensure network performance over existing solutions. A final issue to consider in this thesis is the aggregation of data, because the data to be transmitted in the network are often periodically generated with very small size (a few bytes, for example). Our studies show that data aggregation is a good solution.

Cette these concerne la verification formelle et la composition de protocoles de securite, motivees en particulier par l'analyse des protocoles de vote electronique. Les chapitres 3 a 5 ont comme sujet la verification de protocoles de securite et le Chapitre 6 vise la composition.Nous montrons dans le Chapitre 3 comment reduire certains problemes d'une algebre quotient des termes a l'algebre libre des termes en utilisant des ensembles fortement complets de variants. Nous montrons que, si l'algebre quotient est donnee par un systeme de reecriture de termes convergent et optimalement reducteur (optimally reducing), alors des ensembles fortement complets de variants existent et sont finis et calculables.Dans le Chapitre 4, nous montrons que l'equivalence statique pour (des classes) de theories equationnelles, dont les theories sous-terme convergentes, la theorie de l'engagement a trappe (trapdoor commitment) et la theorie de signature en aveugle (blind signatures), est decidable en temps polynomial. Nous avons implemente de maniere efficace cette procedure.Dans le Chapitre 5, nous etendons la procedure de decision precedente a l'equivalence de traces. Nous utilisons des ensembles fortement complets de variants du Chapitre 3 pour reduire le probleme a l'algebre libre. Nous modelisons chaque trace du protocole comme une theorie de Horn et nous utilisons un raffinement de la resolution pour resoudre cette theorie. Meme si nous n'avons pas reussi a prouver que la procedure de resolution termine toujours, nous l'avons implementee et utilisee pour donner la premiere preuve automatique de l'anonymat dans le protocole de vote electronique FOO.Dans le Chapitre 6, nous etudions la composition de protocoles. Nous montrons que la composition de deux protocoles qui utilisent des primitives cryptographiques disjointes est sure s'ils ne revelent et ne reutilisent pas les secrets partages. Nous montrons qu'une forme d'etiquettage de protocoles est suffisante pour assurer la disjonction pour un ensemble fixe de primitives cryptographiques. / This thesis is about the formal verification and composition of security protocols, motivated by applications to electronic voting protocols. Chapters 3 to 5 concern the verification of security protocols while Chapter 6 concerns composition.We show in Chapter 3 how to reduce certain problems from a quotient term algebra to the free term algebra via the use of strongly complete sets of variants. We show that, when the quotient algebra is given by a convergent optimally reducing rewrite system, finite strongly complete sets of variants exist and are effectively computable.In Chapter 4, we show that static equivalence for (classes of) equational theories including subterm convergent equational theories, trapdoor commitment and blind signatures is decidable in polynomial time. We also provide an efficient implementation.In Chapter 5 we extend the previous decision procedure to handle trace equivalence. We use finite strongly complete sets of variants introduced in Chapter 3 to get rid of the equational theory and we model each protocol trace as a Horn theory which we solve using a refinement of resolution. Although we have not been able to prove that this procedure always terminates, we have implemented it and used it to provide the first automated proof of vote privacy of the FOO electronic voting protocol.In Chapter 6, we study composition of protocols. We show that two protocols that use arbitrary disjoint cryptographic primitives compose securely if they do not reveal or reuse any shared secret. We also show that a form of tagging is sufficient to provide disjointness in the case of a fixed set of cryptographic primitives.

À mesure que le nombre d’objets capables de communiquer croît, le besoin de sécuriser leurs interactions également. La conception des protocoles cryptographiques nécessaires pour cela est une tâche notoirement complexe et fréquemment sujette aux erreurs humaines. La vérification formelle de protocoles entend offrir des méthodes automatiques et exactes pour s’assurer de leur sécurité. Nous nous intéressons en particulier aux méthodes de vérification automatique des propriétés d’équivalence pour de tels protocoles dans le modèle symbolique et pour un nombre non borné de sessions. Les propriétés d’équivalences ont naturellement employées pour s’assurer, par exemple, de l’anonymat du vote électronique ou de la non-traçabilité des passeports électroniques. Parce que la vérification de propriétés d’équivalence est un problème complexe, nous proposons dans un premier temps deux méthodes pour en simplifier la vérification : tout d’abord une méthode pour supprimer l’utilisation des nonces dans un protocole tout en préservant la correction de la vérification automatique; puis nous démontrons un résultat de typage qui permet de restreindre l’espace de recherche d’attaques sans pour autant affecter le pouvoir de l’attaquant. Dans un second temps nous exposons trois classes de protocoles pour lesquelles la vérification de l’équivalence dans le modèle symbolique est décidable. Ces classes bénéficient des méthodes de simplification présentées plus tôt et permettent d’étudier automatiquement des protocoles taggués, avec ou sans nonces, ou encore des protocoles ping-pong. / As the number of devices able to communicate grows, so does the need to secure their interactions. The design of cryptographic protocols is a difficult task and prone to human errors. Formal verification of such protocols offers a way to automatically and exactly prove their security. In particular, we focus on automated verification methods to prove the equivalence of cryptographic protocols for a un-bounded number of sessions. This kind of property naturally arises when dealing with the anonymity of electronic votingor the untracability of electronic passports. Because the verification of equivalence properties is a complex issue, we first propose two methods to simplify it: first we design a transformation on protocols to delete any nonce while maintaining the soundness of equivalence checking; then we prove a typing result which decreases the search space for attacks without affecting the power of the attacker. Finally, we describe three classes of protocols for which equivalence is decidable in the symbolic model. These classes benefit from the simplification results stated earlier and enable us to automatically analyze tagged protocols with or without nonces, as well as ping-pong protocols.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Au Québec, le vieillissement de la population entraîne une augmentation importante des besoins de soins infirmiers, notamment dans la collectivité. En effet, les aînés vivant dans la communauté et dont l’état de santé est fragile voient régulièrement leurs besoins de soins se modifier, notamment parce qu’ils effectuent de nombreux séjours en centre hospitalier, lesquels contribuent à leur déclin fonctionnel. Cela est particulièrement vrai dans le contexte des résidences intermédiaires, où les personnes qui y vivent composent déjà avec des incapacités et la présence de problèmes de santé complexes. Le défaut d’apporter les soins infirmiers nécessaires peut entraîner une détérioration rapide du niveau d’autonomie de l’aîné et de son état de santé, ce qui compromet le maintien en communauté et entraîne une augmentation du recours à l’hébergement en soins de longue durée institutionnalisés. Il est donc impératif de faciliter, par une offre de soins infirmiers adaptés, la délicate période de transition que vivent les aînés suite à une hospitalisation. En effet, la présence de soins transitionnels adaptés permet de diminuer significativement les réadmissions hospitalières et les visites aux urgences, en plus d’engendrer un effet positif sur l’état de santé global des aînés ainsi que sur leur qualité de vie. Ce projet de recherche avait donc pour objectifs d’élaborer un protocole d’interventions infirmières visant à faciliter la transition des aînés faisant un retour en résidence intermédiaire après un séjour hospitalier, au Québec, puis d’évaluer la faisabilité et l’acceptabilité de ce dernier dans le cadre d’un projet-pilote en contexte clinique. La définition des soins infirmiers préconisée pour ce projet de recherche est celle proposée par le modèle de McGill. Cette définition sous-tend l’intervention de l’infirmière, et implique de mobiliser les forces, les ressources et la motivation des aînés et leurs familles, pour qu’ils parviennent à améliorer leur santé ou se rétablir, grâce à leurs capacités à composer avec les situations et à se développer, ici dans le contexte de la transition post-hospitalisation. D’autre part, la théorie de l’autodétermination (Deci & Ryan, 1985; Ryan & Deci, 2017f), la mini-théorie des besoins psychologiques fondamentaux (Ryan & Deci, 2017a), la théorie de l’autosoin de la maladie chronique (Riegel, Jaarsma, & Strömberg, 2012) et la théorie de l’incertitude (Mishel, 1988, 1990) procurent aussi un éclairage théorique considérable dans ce projet. La méthode de recherche interventionnelle retenue est celle de Sidani et Braden (2011). Cette méthode implique à la fois une approche déductive, par l’usage de théories intermédiaires et la consultation de données empiriques, et une approche inductive, par la collecte de données expérientielles. Dans ce projet en trois phases, une approche qualitative descriptive a été utilisée pour les données expérientielles recueillies auprès de onze (n=11) participants aînés et professionnels de la santé. Une triangulation des données expérientielles, empiriques et théoriques a permis ensuite de comprendre en profondeur la transition vécue par les aînés faisant un retour en résidence intermédiaire suite à une hospitalisation, et d’en tirer une liste de besoins de soins non comblés (phase 1, étape 1). Les données expérientielles recueillies ont à nouveau été utilisées pour y cerner des pistes d’interventions puis celles-ci ont été triangulées avec des données théoriques et empiriques pour concevoir les interventions infirmières nécessaires pour répondre adéquatement aux besoins identifiés (phase 1, étape 2), puis théoriser ces interventions (phase 1, étape 3). La phase 2 du projet consistait ensuite à opérationnaliser les résultats obtenus dans la phase 1 en protocole d’interventions écrit. Finalement, en phase 3, un projet-pilote a été réalisé auprès de trois aînés (n=3). Ces aînés ont reçu le protocole d'interventions, puis l’acceptabilité et la faisabilité de ce dernier ont alors été étudiées, de même que ses effets immédiats. Les résultats obtenus suggèrent l’acceptabilité et la faisabilité du protocole élaboré en plus d’illustrer des effets positifs liés au soutien à l’autonomie des personnes, à l’amélioration de leurs capacités d’autosoins ainsi qu’à la réduction de l’incertitude vécue pendant la transition. Enfin, en plus de dévoiler comment précisément les infirmières peuvent intervenir pour faciliter cette transition, l’explication des mécanismes sous-jacents à l’efficacité des interventions infirmières proposées permet d’illustrer pourquoi ces interventions sont bénéfiques pour les personnes et comment elles produisent leurs effets, ce qui n'est actuellement pas présent dans la littérature sur les modèles de soins transitionnels infirmiers. / In Quebec, the aging of the population is leading to a significant increase in nursing needs, particularly in the community. Indeed, seniors living in the community and whose health status is fragile regularly see their care needs change, particularly because they spend many hours in hospital, which contributes to their functional decline. This is particularly true in the context of intermediate resources, where people living in them already deal with disabilities and complex health problems. Failure to provide the necessary nursing care can lead to a rapid deterioration in the senior's level of autonomy and health status, which compromises community maintenance and leads to an increase in the use of institutionalized long-term care housing. It is therefore imperative to facilitate, through the provision of appropriate nursing care, the delicate transition period experienced by seniors following hospitalization. Indeed, the presence of adapted transitional care significantly reduces hospital readmissions and emergency room visits, in addition to having a positive effect on the overall health status of seniors and their quality of life. The objectives of this research project were therefore to develop a nursing intervention protocol to facilitate the transition of seniors returning to intermediate resources after a hospital stay in Quebec, and to assess the feasibility and acceptability of the latter as part of a pilot project in a clinical setting. The definition of nursing care recommended for this research project is that proposed by the McGill model. This definition underlies the nurse's intervention, and involves mobilizing the strengths, resources and motivation of seniors and their families to improve their health or recovery through their ability to cope and develop, here in the context of the post-hospital transition. On the other hand, the theory of self-determination (Deci & Ryan, 1985; Ryan & Deci, 2017f), the mini-theory of basic psychological needs (Ryan & Deci, 2017a), the middle-range theory of self-care of chronic illness (Riegel, Jaarsma, & Strömberg, 2012) and the theory of uncertainty (Mishel, 1988, 1990) also provide a very significant theoretical perspective in this project. The intervention research method used is that of Sidani and Braden (2011). This method involves both a deductive approach, through the use of middle-range theories and the consultation of empirical data, and an inductive approach, through the collection of experiential data. In this three-phase project, a descriptive qualitative approach was used for the experiential data collected from eleven (n=11) senior participants and health professionals. A triangulation of experiential, empirical and theoretical data then provided an in-depth understanding of the transition experienced by seniors returning to intermediate resources following hospitalization, and a list of unmet care needs (Phase 1, Step 1). The experiential data collected were again used to identify possible interventions and then triangulated with theoretical and empirical data to design the nursing interventions needed to adequately address the identified needs (Phase 1, Step 2) and then theorize these interventions (Phase 1, Step 3). Phase 2 of the project then consisted of operationalizing the results obtained in Phase 1 into a written intervention protocol. Finally, in Phase 3, a pilot project was conducted with three seniors (n=3). These seniors were provided with the intervention protocol, and its acceptability and feasibility were then studied, as well as its immediate effects. The results obtained suggest the acceptability and feasibility of the protocol developed and illustrate positive effects related to supporting people's autonomy, improving their self-care capacities and reducing the uncertainty experienced during the transition. Finally, in addition to revealing precisely how nurses can intervene to facilitate this transition, explaining the mechanisms underlying the effectiveness of proposed nursing interventions helps to illustrate why these interventions are beneficial to individuals and how they produce their effects, which is not currently available in the literature on nursing transitional care models.

Thèse ou mémoire avec insertion d'articles / Dans un contexte de présence de plus en plus proéminente d'unités électroniques ou Electronic Control Units (ECU) dans les véhicules [3, 127], la cybersécurité dans le domaine automobile joue un rôle de plus en plus critique [3, 20, 94, 127]. Les systèmes de tests avec matériel dans la boucle (ou Hardware-in-the-Loop (HIL)) sont un bon moyen d'évaluer la résilience des composants d'un véhicule à une attaque de type cyber [28, 29, 74]. Les systèmes de tests HIL sont généralement composés d'un châssis, dans lequel viennent se loger des cartes d'interface et de calcul. Cette architecture a l'avantage d'être très modulaire, une caractéristique nécessaire lorsque la configuration et la complexité des montages varient énormément d'un test à un autre. Ce travail présente un système de test HIL pour les applications automobiles, utilisant Ethernet comme technologie de communication de base. Bien entendu, son coût d'équipement inférieur en fait une alternative intéressante à des systèmes basés sur le PCI eXtention for Intrumentation (PXI) et VME eXtention for Instrumentation (VXI), qui sont les protocoles plus traditionnellement utilisés dans ces applications. Ainsi, on évaluera la viabilité de l'Ethernet dans une telle application, avant de définir le Small Payload Ethernet for HIL (SPEHIL), un protocole spécialement optimisé pour les tests HIL enchâssis. En effet, l'adoption d'Ethernet n'est pas sans défis. Ces derniers sont causés principalement par son taux d'encapsulation très élevé. C'est pourquoi le SPEHIL vient se placer au niveau des couches réseau, transport et application afin de mitiger cette tendance du protocole. Le SPEHIL définit également une couche applicative offrant ainsi la standardisation du contrôle des modules à travers une série de séquences de messages prédéfinis. On définit ensuite le premier prototype de système SPEHIL intégré, dans le but d'en évaluer les performances. Ce dernier se base sur une carte de développement Field Programmable Gate Array (FPGA) Zynq et offre l'interface nécessaire à l'usager pour interagir avec ce dernier. On termine par l'analyse des performances du protocole en place comparé à l'Ethernet tout comme à ses principaux rivaux dans le domaine du HIL. / In a context of an increasingly prominent presence of electronic units or ECU in vehicles [3, 127], cybersecurity in the automotive field plays an increasingly important role [3, 20, 94, 127]. Hardware-in-the-Loop (or HIL) test systems are a good way to assess the resilience of vehicle components to a cyberattack [28, 29, 74]. HIL test systems generally consist of a chassis, in which interface and calculation cards are housed. This architecture has the advantage of being very modular, a necessary characteristic when the configuration and the complexity of the test's setup vary enormously from one ECU to another. This work presents a HIL test system for automotive applications, using Ethernet as the core communication technology. Of course, its lower equipment cost makes it an interesting alternative to systems based on PXI and VXI, which are the protocols more traditionally used in these applications. Thus, we will evaluate the viability of Ethernet in such an application, before defining the SPEHIL, a protocol specially optimized for HIL tests in a chassis. Indeed, Ethernet adoption is not without its challenges. These are mainly caused by its very high encapsulation ratio. This is why the SPEHIL's implementation targets the network and transport layers in order to mitigate this tendency of the protocol. SPEHIL also defines an application layer, thus providing standardization of module's control messages through a series of predefined sequences. We then define the first prototype of an integrated SPEHIL system, in order to evaluate its performance. The latter is based on a Zynq FPGA development board and provides the necessary interface for the user to interact with it. We conclude with the analysis of the performance of the protocol in place compared to Ethernet, and its main rivals in the field of HIL.

Les protocoles cryptographiques constituent le coeur de la sécurité dans les communications de tous genres. Ils assurent l’authentification des agents, la confidentialité des données, leur intégrité, l’atomicité des biens et de l’argent, la non-répudiation, etc. Ils sont utilisés dans tous les domaines : le commerce électronique, le domaine militaire, le vote électronique, etc. L’utilisation de la cryptographie est essentielle pour assurer la sécurité d’un protocole, mais elle n’est pas suffisante. En effet, on rapporte un nombre important de protocoles qui ont été longtemps considérés sécuritaires, mais qui se sont avérés défaillants avec le l’usage. Dire qu’un protocole est correct ou non est un problème nondécidable en général. Cependant, plusieurs méthodes (basées sur les logiques, sur le Model-Checking ou sur le typage, etc.) ont vu le jour pour répondre à cette question sous des hypothèses restrictives et ont abouti à des résultats variables. Dans cette thèse, nous suggérons une méthode semi-décidable d’analyse des protocoles cryptographiques pour la propriété de confidentialité. Elle se base sur une intuition : "Un protocole croissant est correct". Nous validons cette intuition et nous proposons le théorème fondamental de correction des protocoles croissants sous des conditions minimales. Ensuite nous proposons une famille de fonctions témoins ayant les propriétés requises pour certifier qu’un protocole est correct. Nous validons enfin notre méthode sur des protocoles communs. / Cryptographic protocols are the fundament of security in all communications. They allow agents’ authentication, data confidentiality, data integrity, atomicity of goods, atomicity of money, nonrepudiation, etc. They are used in all areas: e-commerce, military fields, electronic voting, etc. The use of cryptography is essential to ensure the protocol security, but it is not sufficient. Indeed, we report a significant number of cryptographic protocols that had long been considered safe, but have been proven faulty with usage. Saying that a protocol is correct or not is an undecidable problem in general. However, several methods (logic-based methods, Model-Checking-based methods, typing-based methods, etc.) have emerged to address this question under restrictive assumptions and led to varying results. In this thesis, we suggest a semi-decidable method for analyzing cryptographic protocols for secrecy. It is based on an intuition: "An increasing protocol is correct". We formally validate this intuition, and we state the fundamental theorem of correctness of increasing protocols under few conditions. Then, we propose a safe way to build a family of reliable functions that we call the witness-functions, to certify protocol’s correctness. Finally, we validate our method on common protocols.

On ne s’en inquiète peut-être pas assez, mais toute communication confidentielle sur Internet, dont on prend désormais la sécurité pour acquise, pourrait du jour au lendemain devenir très facile à espionner. Nous savons en effet qu’un ordinateur quantique, s’il en existe un de suffisante envergure, pourra –ou peut déjà, qui sait ?– rendre obsolète les protocoles cryptographiques qui nous permettent de gérer nos comptes utilisateurs, faire des transactions bancaires et simplement d’avoir des conversations privées. Heureusement, une communauté de chercheurs se penche déjà sur des protocoles alternatifs ; cependant chacune des propositions est isolée dans son propre sous-domaine de recherche et il est difficile de faire la lumière sur laquelle est la plus prometteuse. À travers trois horizons, explorant respectivement pourquoi la cryptographie actuelle est considérée sécuritaire, comment l’arrivée d’un seul ordinateur quantique sur la planète changera toute la cryptographie, et que faire pour communiquer confidentiellement dans un monde où l’informatique quantique est omniprésente, nous développons un cadre uniforme pour analyser lesquels de ces nouveaux protocoles cryptographiques sont assis sur les bases théoriques présageant la plus grande sécurité.

Dans cette thèse, nous proposons un cadre unifié pour la pragmatique et la sémantique de la communication entre agents logiciels. La pragmatique traite la façon dont les agents utilisent les actes communicatifs lorsqu’ils participent aux conversations. Elle est liée à la dynamique des interactions entre agents et à la manière avec laquelle les actes individuels sont reliés pour construire des conversations complètes. La sémantique, quant à elle, est intéressée par la signification de ces actes. Elle établit la base pour une signification concise et non ambiguë des messages échangés entre les agents. Ce cadre unifié vise à résoudre trois problèmes majeurs dans le domaine de communication entre agents : 1- L’absence d’un lien entre la pragmatique et la sémantique. 2- L’inflexibilité des protocoles actuels de communication entre agents. 3- La vérification des mécanismes de communication entre agents. Les contributions principales de cette thèse sont : 1- Une approche pragmatique formelle basée sur les engagements sociaux et les arguments. 2- Un nouveau formalisme pour la communication entre agents appelé Réseau d’Engagements et d’Arguments. 3- Un modèle logique définissant la sémantique des éléments utilisés dans l’approche pragmatique. 4- Une technique de vérification de modèles basée sur une sémantique à tableaux pour vérifier une famille de protocoles flexibles de communication entre agents appelée protocoles à base de jeux de dialogue. 5- Un nouveau protocole de persuasion à base de jeux de dialogue. L'idée principale de notre approche pragmatique est que la communication entre agents est modélisée comme des actions que les agents accomplissent sur des engagements sociaux et des arguments. La dynamique de la conversation entre agents est représentée par cette notion d’actions et par l’évolution de ces engagements et arguments. Notre formalisme (Réseau d’Engagements et d’Arguments) basé sur cette approche fournit une représentation externe de la dynamique de communication entre agents. Ce formalisme peut être utilisé par les agents comme moyen pour participer à des conversations d’une manière flexible parce qu’ils peuvent raisonner sur leurs actes communicatifs en utilisant leurs systèmes d’argumentation et l’état actuel de la conversation. Notre modèle logique est une sémantique, à base d’un modèle théorique, pour l’approche pragmatique. Il définit la signification des différents actes de communication que nous utilisons dans notre approche pragmatique. Il exprime également la signification de quelques actes de discours importants dans le contexte de communication multi-agents et il capture la sémantique des arguments annulables. Ce modèle logique permet d’établir le lien entre la sémantique et la pragmatique de communication entre agents. Nous traitons le problème de vérification des protocoles à base de jeux de dialogue en utilisant une technique de vérification de modèles basée sur une sémantique à tableaux. Ces protocoles sont spécifiés sur la base de notre modèle logique. Nous montrons que notre algorithme de vérification offre une technique, non seulement pour vérifier si le protocole à base de jeux de dialogue (le modèle) satisfait une propriété donnée, mais également si ce protocole respecte la sémantique des actes communicatifs. Notre protocole de persuasion à base de jeux de dialogue est spécifié dans le contexte de notre cadre unifié en utilisant un langage logique. Il est implémenté en utilisant une programmation logique et un paradigme orienté-agent. Dans ce protocole, le processus décisionnel des agents est basé sur les systèmes d’argumentation et sur la notion de crédibilité des agents. / In this thesis, we propose a unified framework for the pragmatics and the semantics of agent communication. Pragmatics deals with the way agents use communicative acts when conversing. It is related to the dynamics of agent interactions and to the way of connecting individual acts while building complete conversations. Semantics is interested in the meaning of these acts. It lays down the foundation for a concise and unambiguous meaning of agent messages. This framework aims at solving three main problems of agent communication: 1- The absence of a link between the pragmatics and the semantics. 2- The inflexibility of current agent communication protocols. 3- The verification of agent communication mechanisms. The main contributions of this thesis are: 1- A formal pragmatic approach based on social commitments and arguments. 2- A new agent communication formalism called Commitment and Argument Network. 3- A logical model defining the semantics of the elements used in the pragmatic approach. 4- A tableau-based model checking technique for the verification of a kind of flexible protocols called dialogue game protocols. 5- A new persuasion dialogue game protocol. The main idea of our pragmatic approach is that agent communication is considered as actions that agents perform on social commitments and arguments. The dynamics of agent conversation is represented by this notion of actions and by the evolution of these commitments and arguments. Our Commitment and Argument Network formalism based on this approach provides an external representation of agent communication dynamics. We argue that this formalism helps agents to participate in conversations in a flexible way because they can reason about their communicative acts using their argumentation systems and the current state of the conversation. Our logical model is a model-theoretic semantics for the pragmatic approach. It defines the meaning of the different communicative acts that we use in our pragmatic approach. It also expresses the meaning of some important speech acts and it captures the semantics of defeasible arguments. This logical model allows us to establish the link between the semantics and the pragmatics of agent communication. We address the problem of verifying dialogue game protocols using a tableau-based model checking technique. These protocols are specified in terms of our logical model. We argue that our model checking algorithm provides a technique, not only to verify if the dialogue game protocol satisfies a given property, but also if this protocol respects the underlying semantics of the communicative acts. Our persuasion dialogue game protocol is specified in our framework using a logical language, and implemented using a logic programming and agent-oriented programming paradigm. In this protocol, the agents’ decision making process is based on the agents’ argumentation systems and the notion of agents’ trustworthiness.