Description
Nous présentons une méthode pour automatiser l'analyse des protocoles cryptographiques à partir de leurs descriptions sous forme de règles d'envoi de messages. Le problème de la détection d'attaque dans un environnement hostile se ramène à la résolution de contraintes sur un espace de messages. La résolution de ces contraintes implantée dans le logiciel issu du projet européen AVISPA est relativement efficace en pratique. Elle a permis de découvrir de nouvelles failles dans des protocoles en cours de standardisation; Nous décrivons une procédure de décision dans le cas d'un nombre fini de sessions avec des clés composées. L'approche s'étend au cas d'un intrus muni de règles de déduction pour prendre en compte des propriétés des primitives cryptographiques : comme le XOR ou l'exponentielle modulaire ...
Prochains exposés
-
Computational assumptions in the quantum world
Orateur : Alex Bredariol Grilo - LIP6 (CNRS / Sorbonne Université)
QKD is a landmark of how quantum resources allow us to implement cryptographicfunctionalities with a level of security that is not achievable only with classical resources.However, key agreement is not sufficient to implement all functionalities of interest, and it iswell-known that they cannot be implemented with perfect security, even if we have accessto quantum resources. Thus, computational[…]-
Cryptographie
-
-
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