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.
Next sessions
-
Endomorphisms via Splittings
Speaker : Min-Yi Shen - No Affiliation
One of the fundamental hardness assumptions underlying isogeny-based cryptography is the problem of finding a non-trivial endomorphism of a given supersingular elliptic curve. In this talk, we show that the problem is related to the problem of finding a splitting of a principally polarised superspecial abelian surface. In particular, we provide formal security reductions and a proof-of-concept[…]-
Cryptography
-