Description
Providing security proofs instead of arguing lack of existing relevant attacks is a quite new approach when it comes to cryptography. In the last thirty years, a lot of work has been done to formalize security of systems and prove of the achievement of security criteria. It has resulted in the design of a great number of proofs under various hypotheses. Though a step in the right direction, these pencil-and-paper proofs are so numerous, involved and technical that the community has difficulty to carefully check them. The well-known example of the encryption scheme OAEP whose security proof, apparently correct, was corrected seven years after its publication illustrates that security-dedicated verification tools need to be designed. Our work takes place in the so-called computational model, where messages are considered to be bitstrings, and system adversaries are probabilistic Turing machines. A proof of security is then a complexity-theoretic reduction argument: the probability of success of an adversary in solving a security challenge is reduced to its ability to solve a known difficult problem (given a fixed amount of resources). Firstly, we provide some intuition on usual security requirements, and common sketches of security proofs. Then, we present a semantics and a logic to formalize security proofs. One could say there are several levels in automatic proving: computer-aided verification of proofs, computer-aided design of proofs, and automatic generation of proofs. We show how our inference rules can be used to derive proofs and verify them automatically, or sometimes perform a proof search using some additional inputs.
Prochains exposés
-
Schéma de signature à clé publique : Frobénius-UOV
Orateur : Gilles Macario-Rat - Orange
L'exposé présente un schéma de signature à clé publique post-quantique inspiré du schéma UOV et introduisant un nouvel outil : les formes de Frobénius. L'accent est mis sur le rôle et les propriétés des formes de Frobénius dans ce nouveau schéma : la simplicité de description, la facilité de mise en oeuvre et le gain inédit sur les tailles de signature et de clé qui bat RSA-2048 au niveau de[…] -
Yoyo tricks with a BEANIE
Orateur : Xavier Bonnetain - Inria
TBD-
Cryptography
-
Symmetrical primitive
-