Université de Rennes 1 Provable security of real world protocols Sécurité prouvée pour les protocoles de la vie réelle cryptographiesécurité prouvéesignature assainissablepare-feux inversésmessagerie sécurisée cryptographyprovable securitysanitizable signaturesreverse firewallssecure messaging Cryptographie La sécurité prouvée est un outil cryptographique particulièrement utile pour évaluer la sécurité d'un protocole. Pour construire une preuve, il faut d'abord définir les propriétés de sécurité à atteindre, c'est-à-dire le modèle de sécurité, ainsi que le type d'adversaire auquel nous sommes confrontés. Ces deux éléments représentent le contexte de la preuve, qui sera calculée après avoir « formaté » le protocole dans le modèle. Dans cette thèse, nous introduisons (ou adaptons) des modèles dans lesquels nous donnons des preuves de sécurité pour trois types de protocoles ayant des applications pratiques : un protocole de messagerie sécurisé, une signature assainissable, et un pare-feu inversé. Pour le premier, nous proposons quelques corrections aux faiblesses du protocole Signal et de son analyse de sécurité précédente. Ensuite, pour le second, nous étendons la signature assainissable pour inclure une nouvelle fonctionnalité, et donc nous étendons les propriétés de sécurité pré-existantes pour la prendre en compte. Enfin, pour la troisième, nous proposons un modèle plus réaliste et plus inclusif que ce qui avait été fait auparavant. Dans les trois cas, nous construisons un protocole que nous prouvons sécurisé dans le modèle défini. Provable security is a very useful cryptographic tool that helps in the evaluation of the security of a protocol. In order to construct a proof, one must first define the security properties that are to be achieved, i.e., the security model, as well as what kind of adversary we are facing. These two components represent the context of the proof, which we can compute after fitting the protocol to the model. In this thesis, we introduce (or adapt) models in which we give security proofs for three kinds of protocols with real-life applications: a secure messaging protocol, a sanitizable signature, and a reverse firewall. For the first, we propose some corrections to the weaknesses of the Signal protocol and its previous security analysis. Then, for the second, we extend sanitizable signature to include a new feature, and thus extend the previous security properties to take this feature into account. Finally, for the third, we propose a more realistic and inclusive model than what had been done before. In all three, we build a protocol that we show is secure in the model we defined. Electronic Thesis or DissertationText en application/pdf1 : 1943 Kohttps://ged.univ-rennes1.fr/nuxeo/site/esupversions/64fee5a1-f0f1-4fe1-ad79-5e0a3a769ea3 Bossuat Angèle 1993-10-13 XX 256026386 angele.bossuat@gmail.com 2020REN1S101 http://www.theses.fr/2020REN1S101 2020-10-06 Informatique Universite de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiFouquePierre-Alainintervenant_1085216380 MATHSTICecoleDoctorale_1 204770424 IRISA partenaireRecherche_1 026386909 ddc:004 FouquePierre-AlainUniversite de Rennes 1Sciences et technologie, medecine, pharmacie, odontologie, droit, economie, gestion, philosophieMATHSTICÉcole doctorale Mathématiques et sciences et technologies de l'information et de la communication (Rennes) IRISA ASCII PDF 1989652