Les robots à vocation sociale ou robotique sociale, au départ très limités dans leur mécanique et leurs capacités intellectuelles, avaient la plupart du temps pour buts la distraction et l'amusement de personnes. De nos jours, les scientifiques s'intéressent aux relations psychologiques qu'il est possible d'entretenir avec ce type de nouveau média de communication. La Robothérapie, qui reprend les règles de la robotique sociale, a pour but d'améliorer l'état psychologique et physiologique de personnes malades, marginalisées ou atteintes de handicaps physiques ou mentaux. Il apparait que les robots peuvent jouer un rôle d'accompagnement et d'éveil. Il faut pour cela les doter de capacités de communications. Le nouveau défi du domaine des robots compagnons consiste à offrir un enrichissement du comportement par leur interaction avec les humains. Quelques études existent déjà dans le domaine de la RAA : " Robot Assisted Activity " et, plus précisément, dans le domaine du RAT : Le " Robot Assisted Therapy ". Les premières expérimentations dans ce domaine de la robotique ont prouvé que les robots compagnons peuvent donner un certain confort moral et psychologique aux personnes fragiles. Dans ce contexte, le projet MAPH (Média Actif Pour le Handicap) a pour objectif d'apporter un réconfort psychologique aux enfants fragilisés (ex. longue hospitalisation ou difficultés d'intégration sociale) à l'aide du robot compagnon. L'objectif de mon travail de recherche tend vers la réalisation d'un robot avec un contact agréable et qui sera doté de capacités d'expression corporelle, de perception et de compréhension du langage naturel de sorte qu'il puisse établir une représentation formelle de l'état émotif de son interlocuteur. Il s'agit de définir et concevoir un modèle des états émotifs du robot et de son évolution, afin que ses réactions semblent les plus naturelles possibles. Ce manuscrit présentera les méthodes utilisées et permettant d'atteindre l'objectif fixé. Nous présenterons les définitions utilisées pour la modélisation du processus émotionnel, la réalisation du modèle de calcul des émotions permettant de générer un état émotionnel ressenti, la construction du robot compagnon expressif et les expérimentations réalisées tentant de valider nos choix de conception et de développement.

Les échanges des informations confidentielles ou critiques dans un environnement public, et donc potentiellement hostile, nécessitent l'emploi de techniques cryptographiques (protocoles et primitives). Malheureusement, l'expérience montre qu'une mauvaise conception, ou une expression peu claire des propriétés et hypothèses de sécurité attendues conduisent à des attaques, et qu'il faut parfois des années avant que celles-ci soient découvertes et corrigées. D'où l'adoption croissante de la sécurité prouvable, où on donne une définition rigoureuse des objectifs de sécurité et des démonstrations mathématiques que ceux-ci sont remplis. Par ailleurs, la complexité et la diversité des systèmes cryptographiques croît également. Il est donc largement admis qu'il n'est plus viable d'écrire ou vérifier manuellement des démonstrations cryptographiques (Bellare& Rogaway 2004, Shoup 2004, Halevi 2005) et qu'il faut développer des méthodes de vérification des systèmes cryptographiques assistées par ordinateur. L'objectif de cette thèse est d'effectuer des progrès significatifs dans cette direction. Plus précisement on s'interesse à la preuve formelle de protocoles cryptographiques. Vérifier des protocoles cryptographiques requiert le développement d'un cadre théorique qui doit permettre: - une modélisation précise des protocoles cryptographiques et des propriétés de sécurité qu'on veut prouver dans le modèle calculatoire. - mise en place de stratégies d'automatisation de preuves. - prise en compte des modèles plus réalistes pour l'adversaire (canaux cachés, ressources de calcul). A la fin de la thèse on a obtenu un cadre formel et un ensemble de méthodes logicielles capable d'aider à la vérification des protocoles cryptographiques. / Critical and private information are exchanged on public environment. To protect it from dishonest users, we use cryptographic tools. Unfortunately, bad conception, poorly written security properties and required security hypothesis lead to attacks, and it may take years before one discover the attack and fix the security schemes involved. In this context, provable security provides formal definitions for security objectives and implied mathematical proofs that these objectives are fullfilled. On another hand, complexity and variety of cryptographic systems are increasing, and proofs by hand are too complicated to write and to verify (Bellare& Rogaway 2004, Shoup 2004, Halevi 2005). Thus, we need computer-assisted verification methods for cryptographic systems. The aim of this thesis is to progress in this direction. More precisely we want significant progress over formal proofs on cryptographic protocols. To verify cryptographic protocols we need to develop a theoritical framework providing: - a precise modelisation for cryptographic protocols and security properties we want to prove in the computationnal model, - designing tactics to automate proofs, - taking into account realistic models for adversary (side-channels...). By the end of the thesis we have enhanced a theoretical framework and computing tools helping verifying cryptographic protocols.