本论文针对 EMV 非接触式支付系统中存在的中继攻击（relay attack）问题展开研究。中继攻击允许攻击者在持卡人与读卡器之间转发消息，从而在用户不知情的情况下完成支付，例如通过无线方式窃取资金。论文首先评估了现有的防护措施：Apple Pay 要求用户指纹或 Face ID 授权；Mastercard 和 Visa 则提出了基于时间或加密的协议来阻止中继。作者发现，在交通支付模式下，可以利用中继绕过 Apple Pay 的锁屏，从已锁定的 iPhone 向任意 EMV 读卡器非法支付任意金额，无需用户授权。此外，Visa 提出的中继对抗措施可被 root 后的智能手机绕过。对于 Mastercard 的防护，作者指出其时间限制在 ISO 14443 协议层实施比在 EMV 协议层更可靠。基于这些发现，论文提出了一种新的中继抵抗协议 L1RP（Layer 1 Relay Protection），并利用 Tamarin 证明器对手机支付（含或不含用户认证）的不同模式进行建模，形式化验证了 Apple 和 Visa 建议（Samsung 采用）的解决方案，并证明 L1RP 能够有效抵御中继攻击。该研究为改进非接触式支付安全提供了重要理论和实践依据。

本文研究了针对EMV非接触支付应用（如Apple Pay、Google Pay等）的秘密状态泄漏攻击。EMV协议在非接触支付中使用动态数据认证和交易计数器等秘密状态来保证安全性，但研究发现攻击者可以通过侧信道或协议实现漏洞，窃取或推测这些秘密状态，从而实施欺诈交易。论文分析了攻击对支付应用安全性的影响，提出了可能的安全增强方法。实验表明，多种主流支付应用存在潜在风险，攻击者可绕过交易限制或伪造支付凭证。

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