Description
Les méthodes formelles (ou encore logiques) sont désormais capables d'analyser automatiquement la plupart des protocoles cryptographiques. Néanmoins les modèles d'attaquant utilisés reposent tous --sauf rares exceptions-- sur le modèle Needham-Schroeder, qui énumère un nombre fini d'actions possibles pour l'intrus. Les modèles cryptographiques au contraire reposent sur un modèle d'attaquant très général, au prix de preuves difficilement automatisables. Une question naturelle est alors de savoir si les modèles logiques, ou au moins certains d'entre eux, peuvent être justifiés du point de vue de la cryptographie: autrement dit si la sécurité au niveau logique implique la sécurité au niveau cryptographique. Le bénéfice serait de pouvoir tirer profit des deux approches et obtenir de manière automatique des preuves de sécurité cryptographiques.<br/> Dans cet exposé, nous présenterons un panorama des travaux existants sur ce sujet. Nous montrerons que si la plupart des résultats sont positifs, certaines limitations sont inévitables dans l'état actuel des connaissance en cryptographie. Nous présenterons enfin certaines directions de recherche visant à étendre les résultats actuels.
Prochains exposés
-
Polytopes in the Fiat-Shamir with Aborts Paradigm
Orateur : Hugo Beguinet - ENS Paris / Thales
The Fiat-Shamir with Aborts paradigm (FSwA) uses rejection sampling to remove a secret’s dependency on a given source distribution. Recent results revealed that unlike the uniform distribution in the hypercube, both the continuous Gaussian and the uniform distribution within the hypersphere minimise the rejection rate and the size of the proof of knowledge. However, in practice both these[…]-
Cryptographie
-
Primitive asymétrique
-
Mode et protocole
-
-
Post-quantum Group-based Cryptography
Orateur : Delaram Kahrobaei - The City University of New York