Latest Past Seminars
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.
ProVerif is a popular tool for the fully automatic analysis of security protocols, offering very good support to detect flaws or prove security. One exception is the case of protocols with global states such as counters, tables, or more generally, memory cells. ProVerif fails to analyse such protocols, due to its internal abstraction.
In the original paper of GSVerif, our key idea was to devise a generic transformation of the security properties queried to ProVerif. We proved the soundness of our transformation and implemented it into a front-end GSVerif. Our experiments showed that our front-end (combined with ProVerif) outperforms the few existing tools, both in terms of efficiency and protocol coverage. We successfully applied our tool to a dozen of protocols of the literature, yielding the first fully automatic proof of a security API and a payment protocol of the literature.
In the newest version of ProVerif, the generic transformations of GSVerif can be fully described in term of axioms, thus taking advantage of this new ProVerif feature.
The number of online services, accounts, apps, and devices that we use is constantly increasing and so is the complexity of the interconnections between them. These interconnections have been exploited in targeted attacks that range from account takeovers to cryptocurrency theft. Protecting users from such attacks is difficult because each user's account ecosystem is individual.
In this talk I will introduce account access graphs which are a formal model to represent a user's account ecosystem, i.e., the collection of accounts, apps, and devices, as well as their interconnections. I will show examples of account access graphs from our user studies and present some of the insights we have gained from them. I will then discuss some of the challenges we must overcome in order to build an account management tool aimed at empowering users to better protect their individual account ecosystem.
This talk is based on joint work published at CCS 2019, CHI 2022 and carried out at ETH Zurich, the University of Dundee and Heriot-Watt University.