Abstract: 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.
Password-authenticated key exchange (PAKE) is an interesting example that shows the magic of mathematics. It allows two remote users to establish a “high-entropy” key from a “low-entropy” shared secret without involving any trusted third party. Following Bellovin and Merrit’s 1992 Encrypted Key Exchange (EKE), many PAKE protocols have been proposed in the next 30 years. Today, some have been adopted in large-scale applications, e.g., secure messenger, Wi-Fi, iCloud, browser sync and Thread. On the other hand, designing a robust PAKE protocol has proved extremely delicate and error-prone. In this talk, I will provide a review of the three decades research in this field, a summary of the state-of-the-art, and a taxonomy to categorize existing protocols. A comparative analysis of protocol performance is provided, using representative examples from taxonomy categories. Finally, I will review the recent IETF selection of PAKE protocols for standardisation and summarise lessons as well as open problems.…