文件名称：EMVerify:Tamarin模型和EMV分析
文件大小：1.08MB
文件格式：ZIP
更新时间：2024-06-12 01:07:31
security emv formal-verification HTML
EM验证 这是EMV标准的模型，是我们IEEE S＆P 2021论文EMV标准：Break，Fix，Verify的补充材料。 有关这项工作的详细信息，请访问 。 资料夹布局 ：包含自动生成的目标模型及其证明（ .proof ），位于以下两个文件夹中： ：包含从Contact.spthy派生的文件。 ：包含从Contactless.spthy派生的文件。 ：包含有用的脚本： ：Python脚本，用于在人类可读HTML文件中总结证明。 它还会生成汇总表的LaTeX代码。 ：Python脚本，它将输入模型的所有事实打印到输出HTML文件中。 它有助于检测不匹配的事实，错误等。 ：Python脚本，可打印输入模型的无注释副本。 ：EMV联系人的通用模型。 ：EMV非接触通用模型。 ：GNU脚本，用于生成目标模型并对其进行Tamarin分析。 *.oracle
【文件预览】：
EMVerify-master
----Contact.oracle(2KB)
----.gitignore(10B)
----Makefile(6KB)
----Mastercard.oracle(1KB)
----tools()
--------columns.txt(258B)
--------collect(14KB)
--------parse_facts(5KB)
--------tex-add.txt(4KB)
--------decomment(964B)
----models-n-proofs()
--------contactless()
--------contact()
----README.md(12KB)
----results-contact.html(37KB)
----Visa.oracle(1KB)
----results-contactless.html(26KB)
----Contactless.spthy(38KB)
----Contact.spthy(33KB)