该论文对EMV（Europay, Mastercard, Visa）支付协议标准进行了系统性的形式化安全分析。EMV是国际智能卡支付协议标准，全球超过90亿张卡片使用该标准。尽管标准宣称安全，但此前已发现多种由逻辑缺陷导致的安全问题，这些缺陷在长达2000多页的规范中难以察觉。作者使用Tamarin——一种先进的协议验证器——构建了EMV的全面符号化模型，该模型首次支持对EMV旨在提供的所有相关安全保证进行细粒度分析。通过自动分析，模型发现了两个关键攻击：第一，攻击者可以利用用户的Visa非接触式卡片进行需要持卡人验证的支付，而无需知道卡片PIN码。作者开发了概念验证Android应用，并在真实支付终端上成功演示了该攻击。第二，攻击者可以欺骗终端接受未经认证的离线交易，发卡银行后续应拒绝该交易，但此时攻击者已携商品离开。出于道德原因，作者未在实际终端测试该攻击，但确认符合标准的实现可能受到该攻击影响。最后，作者提出并验证了对标准的改进措施，这些改进可防止上述攻击以及任何其他违反所考虑安全属性的攻击。改进措施易于在终端实现，且不影响已在流通的卡片。该研究揭示了形式化验证在发现复杂协议安全漏洞中的重要作用，并为改进支付安全提供了可操作的方案。