Cette thèse se propose de remédier à l'absence de formalisme dédié aux preuves de sécurité concrète à travers 3 contributions. Nous présentons d'abord la logique CIL (Computational Indistinguishability Logic), qui permet de raisonner sur les systèmes cryptographiques. Elle contient un petit nombre de règles qui correspondent aux raisonnements souvent utilisés dans les preuves. Leur formalisation est basée sur des outils classiques comme les contextes ou les bisimulations. Deuxièmement, pour plus d'automatisation des preuves, nous avons conçu une logique de Hoare dédiée aux chiffrement asymétrique dans le modèle de l'oracle aléatoire. Elle est appliquée avec succès sur des exemples de schémas existants. Enfin, nous proposons un théorème générique de réduction pour la preuve d'indifférentiabilité d'un oracle aléatoire de fonctions de hachage cryptographiques. La preuve du théorème, formalisée en CIL, en démontre l'applicabilité. Les exemples de Keccak et Chop-Merkle-Damgard illustrent ce résultat. / In this thesis, we address the lack of formalisms to carry out concrete security proofs. Our contributions are threefold. First, we present a logic, named Computational Indistinguishability Logic (CIL), for reasoning about cryptographic systems. It consists in a small set of rules capturing reasoning principles common to many proofs. Their formalization relies on classic tools such as bisimulation relations and contexts. Second, and in order to increase proof automation, it presents a Hoare logic dedicated to asymmetric encryption schemes in the Random Oracle Model that yields an automated and sound verification method. It has been successfully applied to existing encryption schemes. Third, it presents a general reduction theorem for proving indifferentiability of iterative hash constructions from a random oracle. The theorem is proven in CIL demonstrating the usefulness of the logic and has been applied to constructions such as the SHA-3 candidate Keccak and the Chop-MD construction.

La recherche sur les bases de données chiffrées vise à rendre efficace une tâche apparemment simple : déléguer le stockage de données à un serveur qui ne serait pas de confiance, tout en conservant des fonctionnalités de recherche. Avec le développement des services de stockage dans le Cloud, destinés aussi bien aux entreprises qu'aux individus, la mise au point de solutions efficaces à ce problème est essentielle pour permettre leur déploiement à large échelle. Le principal problème de la recherche sur bases de données chiffrées est qu'un schéma avec une sécurité ''parfaite'' implique un surcoût en termes de calcul et de communication qui serait inacceptable pour des fournisseurs de services sur le Cloud ou pour les utilisateurs - tout du moins avec les technologies actuelles. Cette thèse propose et étudie de nouvelles notions de sécurité et de nouvelles constructions de bases de données chiffrées permettant des recherches efficaces et sûres. En particulier, nous considérons la confidentialité persistante et la confidentialité future de ces bases de données, ce que ces notions impliquent en termes de sécurité et d'efficacité, et comment les réaliser. Ensuite, nous montrons comment protéger les utilisateurs de bases de données chiffrées contre des attaques actives de la part du serveur hébergeant la base, et que ces protections ont un coût inévitable. Enfin, nous étudions les attaques existantes contre ces bases de données chiffrées et comment les éviter. / Searchable encryption aims at making efficient a seemingly easy task: outsourcing the storage of a database to an untrusted server, while keeping search features. With the development of Cloud storage services, for both private individuals and businesses, efficiency of searchable encryption became crucial: inefficient constructions would not be deployed on a large scale because they would not be usable. The key problem with searchable encryption is that any construction achieving ''perfect security'' induces a computational or a communicational overhead that is unacceptable for the providers or for the users --- at least with current techniques and by today's standards. This thesis proposes and studies new security notions and new constructions of searchable encryption, aiming at making it more efficient and more secure. In particular, we start by considering the forward and backward privacy of searchable encryption schemes, what it implies in terms of security and efficiency, and how we can realize them. Then, we show how to protect an encrypted database user against active attacks by the Cloud provider, and that such protections have an inherent efficiency cost. Finally, we take a look at existing attacks against searchable encryption, and explain how we might thwart them.