Description
We believe that formal methods in security should be leveraged in all the standardisation’s of security protocols in order to strengthen their guarantees. To be effective, such analyses should be:* maintainable: the security analysis should be performed on every step of the way, i.e. each iteration of the draft;* pessimistic: all possible threat models, notably all sort of compromise should be considered;* precise: the analysis should notably include as many real life weaknesses of the concrete cryptographic primitives specified.In this talk, we illustrate how such a goal may be approached by detailing our analysis of the current IETF draft standard of the EDHOC protocol, as well as our subsequent interactions with its LAKE working group. We will proceed in three steps, first introducing the Sapic+ platform that allows from a single modeling of a protocol to benefit from all the capabilities of multiple automated verification tools (ProVerif, Tamarin, DeepSec). We will then introduce multiple recent advances on how to better model the cryptographic primitives and their real life weaknesses. We will finally show how we leveraged Sapic+ along with the advanced primitive models to analyze the EDHOC protocol and provide feedback to the LAKE working group that has been integrated in latter drafts.
Prochains exposés
-
Vers l’émergence d’un droit européen pour la Blockchain : Une approche sous l’angle de la Privacy et de l’encadrement des crypto-actifs
Orateur : Damien Franchi - Univ Rennes, IODE
La Blockchain, technologie derrière Bitcoin, fait l’objet d’un encadrement juridique de plusen plus important, en particulier de la part de l’Union européenne. Curieusement, le mot« Blockchain » n’apparaît pas dans les textes l’encadrant. Les expressions « technologie deregistres distribués » (Distributed ledger technology, DLT), ou, parfois, « registreélectronique » lui sont plutôt privilégiées.[…]-
SoSysec
-
Law
-
-
Blockchain and digital currencies: between European regulation and technological challenges
Orateur : Loïc Miller - CentraleSupélec
As the European Union develops a legal framework for crypto-assets and data protection, the technological question underlying the emergence of a genuine digital currency remains open. Blockchain today stands as an interdisciplinary field of study at the crossroads of computer science, economics, and law. This presentation will place the ongoing regulatory framework in perspective with the[…]-
SoSysec
-
Distributed systems
-
-
Hardware-Software Co-Designs for Microarchitectural Security
Orateur : Lesly-Ann Daniel - EURECOM
Microarchitectural optimizations, such as caches and speculative out-of-order execution, are essential for achieving high performance. However, these same mechanisms also open the door to attacks that can undermine software-enforced security policies. The current gold standard for defending against such attacks is the constant-time programming discipline, which prohibits secret-dependent control[…]-
SoSysec
-
Hardware/software co-design
-
Micro-architectural vulnerabilities
-