Description
Le problème SAT est un des piliers de l'informatique théorique et de la NP-Complétude. Sa résolution pratique a connu un réel essor ces dernières années. Les contributions en ce sens sont multiples et touchent un certain nombre de champs d'application. Les tentatives d'affaiblissements des primitives cryptographiques en font partie. Cet exposé rappellera les fondements du problème SAT, les limitations actuelles de sa résolution pratique (séquentielle et parallèle) et décrira les différentes approches qu'il est possible d'envisager pour modéliser une cryptanalyse par ce biais. Nous illustrerons ces principes avec une attaque pratique sur la seconde préimage d'une fonction de hachage cryptographique et sur un nombre de tours restreint, l'approche SAT constituant à ce jour et à notre connaissance la meilleure inversion pratique connue. Nous conclurons en donnant quelques pistes de recherche.
Prochains exposés
-
CryptoVerif: a computationally-sound security protocol verifier
Orateur : Bruno Blanchet - Inria
CryptoVerif is a security protocol verifier sound in the computational model of cryptography. It produces proofs by sequences of games, like those done manually by cryptographers. It has an automatic proof strategy and can also be guided by the user. It provides a generic method for specifying security assumptions on many cryptographic primitives, and can prove secrecy, authentication, and[…]-
Cryptography
-