Séminaire SoSySec : Not so AdHoc testing: formal methods in the standardization of the EDHOC protocol

Séminaire
Date de début
Date de fin
Lieu
IRISA Rennes
Salle
Salle Métivier
Orateur
Charlie JACOMME (INRIA Paris)
Département principal

SoSySec seminar Software and Systems Security
Inria - Rennes
Friday December 16, 11:00
Remotely via BBB: https://bbb.inria.fr/all-t0p-qjq-9em 
Access code: 192737

-------------------------------------------------------
Charlie Jacomme (INRIA Paris)
-------------------------------------------------------
======================================================================
Not so AdHoc testing: formal methods in the standardization of the EDHOC protocol
======================================================================

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.

 

To follow the presentation remotely, please connect to the followingURL with a modern web browser:
- URL: https://bbb.inria.fr/all-t0p-qjq-9em 
Access code: 192737
- Alternative audio access by phone will be possible but the parameters will be announced only a few minutes before the presentation.

Seminar taking place in person with mandatory registration at least 48h beforehand for *all* in-person participants by email to Nadia Derouault < nadia [*] derouaultatinria [*] fr >. Participants non-affiliated with Inria or IRISA will be asked to present an ID at the reception desk of the IRISA building.

To receive the SoSySec announcements, please subscribe to the SoSySec mailing list:
https://sympa.inria.fr/sympa/subscribe/sosysec 
All past and future SoSySec talks are listed at
https://seminaires-dga.inria.fr/en/seances-a-venir/ 
----------------------------------------------------------------------

Séminaire en présentiel ouvert à tous et toutes mais avec inscription obligatoire au moins 48h à l'avance pour *tous* les participants en présentiel auprès de Nadia Derouault <nadia [*] derouaultatinria [*] fr>.
Les participants externes devront se présenter à l'accueil avec une pièce d'identité.

Vous pouvez vous abonner à nos annonces de séminaires :
https://sympa.inria.fr/sympa/subscribe/sosysec
et consulter la liste des exposés passés et à venir :
https://seminaires-dga.inria.fr/seances-a-venir/