Sécurité prouvée pour les protocoles de la vie réelle

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