EMV 标准：破解、修复、验证

EMV 是智能卡支付的国际协议标准，全球超过 90 亿张卡在使用。尽管该标准宣称安全，此前已发现各种问题，源于 EMV 长达 2000 多页、冗长复杂的规范中难以察觉的逻辑缺陷。我们在最先进的协议验证器 Tamarin 中形式化了 EMV 的综合符号模型。我们的模型是首个支持对 EMV 旨在提供的所有相关安全保证进行细粒度分析的模型。我们利用模型自动识别导致两次关键攻击的缺陷：一个欺诈持卡人，第二个欺诈商户。首先，犯罪分子可使用受害者的 Visa 非接触式卡进行需要持卡人验证金额的支付，而无需知晓卡的 PIN。我们构建了一个概念验证 Android 应用，并在真实支付终端上成功演示了该攻击。其次，犯罪分子可诱骗终端接受一笔不应被认证的离线交易，发卡行应在犯罪分子拿走商品后拒绝该交易。此攻击对遵循标准的实现是可能的，尽管出于道德原因我们未在真实终端上测试。最后，我们提出并验证了该标准的改进，以防止这些攻击以及任何违反所考虑安全属性的其他攻击。所提改进可轻易在终端中实现，且不影响流通中的卡片。