EasyCrypt in anger — Proofs for Primitives, Constructions and Protocols
The EasyCrypt proof assistant offers—in a single tool—the ability to reason about cryptographic security at various scales from primitives to protocols. However, this flexibility comes at a huge cost in usability. This talk will discuss insights gained through the recent formalisation of primitives (SHA-3, XMSS), constructions (KMS, crypto_box) and protocols (distance-bounding, AKE) and explore plans for improvements to the tool that would enable its use on larger protocols, and for the creation of beginner-friendly tutorial material that would enable it to be used more broadly.
1 0
A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif
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.
1 0
Practical and Formal Analysis Security of Contactless Mobile Payments
In this talk, we will look at the (in)security of contactless payments made via mobile apps. These systems are a composition of the mobile app (e.g., Samsung Pay, Apple Pay) and their underlying payment protocols provided via the card registered within (e.g., Visa, Mastercard, etc.). One added complexity comes also from the various “modes” in which the apps operate; for instance, there is a standard mode as well as transit/travel mode, in which the user authentication (via fingerprint or Face-ID) on the mobile device is foregone in order to provide better usability when paying at a metro/train ticketing gate. Primarily, we show that we can abuse this usability feature of Apple Pay in Travel Mode when set up with a Visa card. The abuse results in a fraudulent payment without user-authentication, of any value, to any point-of-sale including points-of-sales what are not linked to transport companies. Also, we show that the same attack does not apply to Apple Pay with a Mastercard registered with it, or to Samsung Pay. We will explain the practical aspects of the attack, as well as some elements of formal security verification.
1 0