Abstracts
- Speaker: Elaine Li (New York University)
- Title: Multiparty Session Type Projection and Subtyping with Automata
- Abstract: Multiparty session types (MSTs) are a type-based approach to verifying communication protocols. Central to MSTs is a projection operator: a partial function that maps protocols represented as global types to correct-by-construction implementations for each participant, represented as a communicating state machine (CSM). Existing projection operators are syntactic in nature, and trade efficiency for completeness. In the first part of the talk, I will present the first projection operator that is sound and complete. I will highlight the automata-theoretic nature of our projection operator, which separates synthesis from checking implementability, and can be computed in PSPACE.
While our projection operator always computes a candidate implementation if one exists, it may not always compute the best candidate. In the second part of the talk, I motivate the subtyping problem for MSTs through a series of examples. I then demonstrate how we can use our previous solution to implementability to obtain subtyping algorithms for MSTs, with unrestricted CSMs as implementation model.
- Speaker: Ralf Sasse (ETH Zurich)
- Title: The EMV Standard: Break, Fix, Verify & Card Brand Mixup Attacks
- Abstract: EMV is the international protocol standard for smartcard payment and is used in over 9 billion cards worldwide. Despite the standard's advertised security, various issues have been previously uncovered, deriving from logical flaws that are hard to spot in EMV's lengthy and complex specification, running over 2,000 pages.
We formalize a comprehensive symbolic model of EMV in Tamarin, a state-of-the-art protocol verifier. We use our model to automatically identify flaws that lead to critical attacks. Criminals can use a victim's Visa contactless card to make payments for amounts that require cardholder verification, without knowledge of the card's PIN. We built a proof-of-concept Android application and successfully demonstrated this attack on real-world payment terminals.
Most EMV transactions require online authorization by the card issuer. In this paper we show that it is possible to induce a mismatch between the card brand and the payment network, from the terminal's perspective. The resulting card brand mixup attack has serious security consequences. In particular, it enables criminals to use a victim's Mastercard contactless card to pay for expensive goods without knowing the card's PIN. We extended the Android application and successfully used it to carry out this attack for transactions with both Mastercard debit and credit cards, including a transaction for over 400 USD with a Maestro debit card.
- Speaker: Sasa Radomirovic (University of Surrey)
- Title: Managing the integrity and availability of our online accounts
- Abstract: Account access graphs model relationships between user devices, credentials, online accounts, and methods of access. They capture both single and multi-factor access routes as well as alternative access routes (e.g., for account recovery).
This talk will provide an overview of our past and present work on account access graphs. I will first show how we used them to discover users' online security strategies. I will then present our recent and ongoing work towards the use of account access graphs as a tool to model attacker techniques and resilience strategies in order to analyse the security of our evolving online account ecosystems.
- Speaker: Rolando Trujillo Rasua (Rovira i Virgili University)
- Title: Automated generation of attack trees with optimal shape and labelling
- Abstract: This talk presents a solution approach to the following problem: given a formal specification of a system, produce an attack tree that correctly and clearly describes the ways the system can be attacked. Correctness means that the attacks displayed by the attack tree are indeed attacks in the system; clarity means that the tree is efficient in communicating the attack scenario.
Back to SRM presentations.
Contact
For questions and comments contact
Sergiu
.
