为什么密码模型不被认为是形式化的方法？
我刚刚开始研究分析密码协议安全性的不同方法。根据我的理解，在这方面有两种主要的方法。第一种方法是所谓的Dolev-姚(或形式)模型，其中密码信息被表示为术语代数中的符号术语。第二个方案更接近于密码协议的实际实现，其中原语被看作概率算法，攻击者是一个多项式时间概率图灵机。在后一种方法中，密码的安全性通常被定义为安全博弈。
我的困惑是，前一种方法在文献中被称为正式方法，而不是第二种。看看维基百科中形式化方法的定义，它说：“形式化方法是一种特殊的基于数学的技术，用于软硬件系统的规范、开发和验证”。根据这个定义，我不明白为什么第二种方法不能被视为正式的方法。实际上，第一个级别比第二个抽象级别高一个抽象级别，并且提供了较弱的安全保证。因此，据我所知，它们都是安全协议的正式验证技术，因此都应该被看作是正式的方法。有人能帮我澄清一下吗？
回答 1
Cryptography用户
发布于 2016-10-23 12:51:08
免责声明:我目前正在做正式方法和密码学方面的PhD，我不太确定我的答案。
形式化方法的第一个应用是应用于软件的各个部分。目的是证明它们的安全属性。这些通常是安全关键软件(那些你在飞机，火车，核设施.)这个字段称为软件验证。
我主要认为形式方法是一种争论的方式，一种思考或证明的方式。在这种情况下，正式手段没有歧义。因此，在正式方法领域中，您可以考虑任何具有这种思维方式的方法。
为了回答您的问题，在我看来，两种方法都符合正式方法的条件(我不明白为什么它们不应该)。
例如，Easycrypt，一个在基于游戏的模型和概率模型中进行证明的工具，是基于Why3的。我很肯定，Why3是形式方法的一部分，它使用定理证明器和SMT求解器，如阿尔戈或Z3。
https://crypto.stackexchange.com/questions/40894
复制相似问题
腾讯云开发者
