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
-
Encryption homomorphe sans bruit à l'aide de groupes
Orateur : Pierre Guillot - Ravel Technologies (dispo Université de Strasbourg, IRMA)
Je vais rappeler les travaux de Nuida et Ostrovski sur l'utilisation des groupes pour l'élaboration de schémas cryptographiques homomorphes. Je vais présenter nos travaux qui fournissent des encodages à la fois plus efficaces et plus généraux, et qui déterminent exactement quels groupes peuvent être utilisés. Puis je vais discuter GRAFHEN, un protocole qui utilise ces idées. Je dirai juste[…]-
Cryptography
-
-
MIKE: An efficient and compact NIKE Based on a Commutative Monoidal Action
Orateur : Jonathan Komada Eriksen - COSIC, KU Leuven
Robert recently described a powerful correspondence between certain (Hermitian) modules and (polarized) abelian varieties, which simultaneously generalizes both the class-group action underlying protocols such as CSIDH, and the Deuring correspondence, underlying protocols such as SQIsign. Using this correspondence, he also proposed how to construct a post-quantum NIKE, called MIKE, which, at a[…]-
Cryptography
-