该论文对国际智能卡支付协议标准 EMV（全球超过90亿张卡片在使用）进行了系统性安全分析。研究背景是EMV标准长达2000多页的规范中存在难以发现的逻辑缺陷，此前已有若干安全问题被披露。核心方法是对EMV协议进行全面的符号化建模，使用先进协议验证工具Tamarin，首次实现对EMV旨在提供的所有相关安全保证的细粒度分析。通过自动化验证，论文发现了两类关键攻击：第一类攻击允许犯罪分子使用受害者的Visa非接触式卡片进行需要持卡人验证（如输入PIN）的高额支付，而无需知道PIN；研究者开发了概念验证安卓应用并在真实支付终端上成功演示。第二类攻击允许犯罪分子诱骗终端接受未经认证的离线交易，随后发卡行应拒绝该交易，但犯罪分子已携带商品离开（由于伦理限制，未在实际终端测试）。针对上述攻击，论文提出了改进方案，并利用模型验证了这些方案能阻止攻击且不影响已发行的卡片；改进只需在终端侧实施，无需更新卡片。该工作的主要贡献包括：首个支持EMV完整安全属性细粒度分析的符号化模型；自动化发现并验证两个关键攻击；提出并验证可落地的修复措施。适合协议安全研究者、支付系统开发者和标准制定者阅读。