EMV标准：断开、修复、验证
The EMV Standard: Break, Fix, Verify
摘要：
EMV是电子货币支付的国际协议标准，在全球范围内使用超过90亿张卡。尽管该标准宣传了安全性，但之前已经发现了各种问题，这些问题源于EMV冗长而复杂的规范中难以发现的逻辑缺陷，超过2,000页。我们正式的EMV在Tamarin，一个国家的最先进的协议验证器的综合符号模型。我们的模型是第一个支持对EMV旨在提供的所有相关安全保证进行细粒度分析的模型。我们使用我们的模型来自动识别导致两种关键攻击的缺陷：一种是欺骗持卡人，另一种是欺骗商家。首先，犯罪分子可以使用受害者的Visa非接触式卡支付需要持卡人验证的金额，而不知道卡的PIN。我们构建了一个概念验证的Android应用程序，并成功地在现实世界的支付终端上演示了这种攻击。第二，犯罪分子可以欺骗终端接受不真实的离线交易，在犯罪分子带走货物后，发卡银行应该会拒绝。这种攻击对于遵循标准的实现是可能的，尽管出于道德原因，我们没有在实际终端上进行测试。最后，我们提出并验证改进的标准，防止这些攻击，以及任何其他攻击，违反了考虑的安全属性。建议的改善措施可轻易在终端机实施，而不会影响流通的卡。
英文摘要：
EMV is the international protocol standard for smartcard payment and is used in over 9 billion cards worldwide. Despite the standard's advertised security, various issues have been previously uncovered, deriving from logical flaws that are hard to spot in EMV's lengthy and complex specification, running over 2,000 pages. We formalize a comprehensive symbolic model of EMV in Tamarin, a state-of-the-art protocol verifier. Our model is the first that supports a fine-grained analysis of all relevant security guarantees that EMV is intended to offer. We use our model to automatically identify flaws that lead to two critical attacks: one that defrauds the cardholder and a second that defrauds the merchant. First, criminals can use a victim's Visa contactless card to make payments for amounts that require cardholder verification, without knowledge of the card's PIN. We built a proof-of-concept Android application and successfully demonstrated this attack on real-world payment terminals. Second, criminals can trick the terminal into accepting an unauthentic offline transaction, which the issuing bank should later decline, after the criminal has walked away with the goods. This attack is possible for implementations following the standard, although we did not test it on actual terminals for ethical reasons. Finally, we propose and verify improvements to the standard that prevent these attacks, as well as any other attacks that violate the considered security properties. The proposed improvements can be easily implemented in the terminals and do not affect the cards in circulation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
