Loading Seminars

« All Seminars

  • This seminar has passed.

Not so AdHoc testing: formal methods in the standardization of the EDHOC protocol

July 20 (2022) @ 3:00 pm - 4:00 pm

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.

passcode: 095565

Live Stream:


July 20 (2022)
3:00 pm - 4:00 pm
Seminar Tags:
, ,


Charlie Jacomme (CISPA)

Charlie Jacomme (charlie.jacomme.fr) is a post-doctoral researcher at CISPA (Germany) in Cas Cremers group, after a PhD thesis at ENS Paris-Saclay (France) under Hubert Comon and Steve Kremer for which he got PhD thesis awards both from the French security community and the French computer science community. He works on formal methods applied to security, with publications at top conferences (S&P, CCS, USENIX, CSF) covering both practical security analysis and more theoretical contributions. He is notably one of the main developers and designers of the Squirrel Prover, an interactive prover for protocols that provides computational guarantees even in the post-quantum setting.

Leave a Reply

Your email address will not be published. Required fields are marked *