Proverif学习

ProVerif可以用来自动分析密码协议的Security性质，功能涵盖对称和非对称加密、数字签名、哈希函数、比特承诺、非交互式零知识证明。ProVerif可以证明可达性(reachability)，对应断言(correspondence assertion)，和可观察的等价性(observational equivalence)。这个能力使得它能对计算机安全领域中的机密性和认证性质进行分析，也可以考虑一些新兴的性质，如隐私性(privacy)、可追溯性(traceability)、可验证性(verifiability)。它还具有攻击重构的功能，如果某个性质不能被证明，ProVerif就会尝试构造一个反例trace。

Proverif

Proverif用来验证密码协议，密码协议是利用互联网等公共通信渠道进行交互以实现一些与安全相关的目标的并发程序。Proverif是在Dolev-Yao模型下进行密码协议验证的。在Dolev-Yao模型下，攻击者可以完全控制通信信道，可以读取、修改、删除以及注入消息，攻击者还可以操纵数据，例如：计算元组的莫个参数，使用密钥解密信息。Proverif还将检测不诚实的参与者行为，只有诚实的参与者会被建模。

Proverif允许密码术语和相关安全性目标以形式化的方式输入，允许自动验证声明的安全性目标。假设密码是完美的，只有攻击者拥有所需的密钥才能执行密码操作。运用对等原理或者重写规则来获取密码术语之间的关系。

使用Proverif语言，需要分三步，第一步声明；第二步进程宏；第三步主进程。

缺陷

ProVerif依赖于符号化的Dolev-Yao密码学模型，所以结果不能应用于计算模型，如果要用计算模型可以考虑CryptoVerif等其它工具。

ProVerif使用符号执行技术和Dolev-Yao模型对协议进行分析和验证。由于这种模型的抽象性质，ProVerif的结果在某些情况下可能无法直接应用于具体的计算模型。

Dolev-Yao模型假设通信网络是可信的，并且攻击者无法干扰、篡改或拦截通信。这种理想化的假设在现实世界中并不成立，因为真实的网络环境中存在各种攻击和安全威胁。

因此，尽管ProVerif可以对协议在Dolev-Yao模型下的安全性进行形式化验证，但在实际应用中，需要将结果与具体的计算模型和网络环境结合起来进行综合评估。这意味着ProVerif的结果可能需要在实际环境中进行进一步的验证和测试，以确保协议在现实的计算模型下的安全性。

另外，ProVerif的符号执行技术也存在一定的局限性，例如对于复杂的协议和大规模系统的分析可能效率较低。因此，在使用ProVerif时，需要谨慎考虑其适用性和局限性，并结合其他验证方法和实验结果进行综合评估和决策。