Compositional Analysis of Protocol Equivalence in the Applied π-Calculus Using Quasi-open Bisimilarity. - Ross Horne; Sjouke Mauw; Semen Yurkov (ICTAC, 2021)

Breaking and Fixing Unlinkability of the Key Agreement Protocol for 2nd Gen EMV Payments. - Ross Horne; Sjouke Mauw; Semen Yurkov (CoRR, 2021)

Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments. - Ross Horne; Sjouke Mauw; Semen Yurkov (CSF, 2022)

Provably Unlinkable Smart Card-based Payments. - Sergiu Bursuc; Ross Horne; Sjouke Mauw; Semen Yurkov (CCS, 2023)

Analysis of Smartcard-based Payment Protocols in the Applied Pi-calculus using Quasi-Open Bisimilarity. - Semen Yurkov (2023)

When privacy fails, a formula describes an attack: A complete and compositional verification method for the applied π-calculus. - Ross Horne; Sjouke Mauw; Semen Yurkov (Theor. Comput. Sci., 2023)