EMVerify-PAN路由分析：Tamarin模型与EMV非接标准评估

简介：
本研究通过Tamarin证明辅助工具对EMV非接触式支付协议进行形式化验证和安全评估，运用PAN路由分析确保交易过程的安全性。 基于PAN路由的EMV模型该存储库包含EMV非接触式协议的模型。这是对我们USENIX Security 21论文《卡品牌混淆攻击：通过使用它们进行Visa交易绕过非Visa卡中的PIN》的补充材料。此扩展模型是我们先前工作的延续，允许终端根据卡片号（即PAN）确定卡的品牌，并据此选择路由网络处理交易。因此，该存储库中大部分内容是原始文档的副本。 与原版不同的是，在这个更新版本里，可以通过读取卡片编号来判断其所属品牌并决定使用哪个支付网络进行交易。若想查看我们先前模型和此扩展之间的代码差异，请直接对比相关文件即可。 资料夹布局是对EMV非接触式协议的一个（通用）建模框架。其中包含的GNU脚本用于生成目标模型，并对其进行Tamarin分析。*.oracle 文件为证明支持提供参考，而* .spthy 和 *.proof 则是自动生成的目标模型及其对应的证明文档。最后，还有几个有用的脚本以HTML格式展示分析结果。 该存储库中的文件结构和内容旨在帮助研究者更好地理解EMV非接触式协议的运作机制，并对其进行进一步的研究与探索。