Privacy properties of systems are usually expressed as certain equivalence problems in applied Pi-calculus. In this talk, I discuss the importance of the chosen equivalence notion and argue that Quasi-open bisimilarity is the optimal equivalnce choice to analyse the privacy of real-world protocols. The corresponding paper, "Compositional Analysis of Protocol Equivalence in the Applied Pi-calculus using Quasi-Open Bisimilarity" is to appear in the proceedings of the ICTAC 2021 conference.
Unlinkable key agreement suitable for EMV payments
As of June 2022 the most prevalent smart card-based payment method, EMV, offers no privacy to its users. Transaction details and the card number are sent in clear text, enabling cardholders’ profiling and tracking. To address this issue EMVCo has proposed a Blinded Diffie-Hellman authenticated key establishment protocol, which is intended to satisfy unlinkability property, i.e. the inability to link protocol sessions made with the same card. In the paper to appear in the proceedings of the CSF 2022 conference we point out that the proposed protocol is not unlinkable in the presence of active attackers, and demonstrate that an active attacker can compromise unlinkability within a distance of 100cm. We adopt a strong definition of unlinkability that does account for active attackers and propose an enhancement of the protocol proposed by EMVCo, and prove that our protocol does satisfy strong unlinkability while preserving authentication.
