我们对协议验证者的信任程度如何？

Question

我读过很多关于认证密钥交换协议的论文，大多数的安全证明都是由作者完成的。在这种方法中，可以想象效率很低。此外，即使您已经在某个模型(例如eCK)下证明了AKE协议的安全性，您仍然无法确保所有其他模型下的安全性，包括现实生活中的安全性。

这让我不禁要问:可以用一些自动化工具来验证协议，例如塔马林吗？这毕竟是非常有效的。我最初担心的是，这种做法是否会被人们接受，并与传统方式一样令人信服？

Answer 1

我们知道，传统的数学证明可以包含错误，而且这些错误可能多年未被发现。有时，即使证据不正确，该方案也是安全的，例如RSA-OAEP。有时，这个方案有轻微的缺陷，由于证明中的错误而未被发现的缺陷，例如HMQV。有时候，一个计划根本就是不安全的。

我们知道，正规系统可能无法描述现实世界，因此证明了不正确的结果，例如班逻辑，但现在的正式系统似乎更完整。

正规系统通常适用于理想化的密码学。有时可以证明某种理想化是合理的，但总的来说，这是困难的。这意味着，原则上，可以设计在正式系统中安全的方案，但无论使用什么加密技术来实例化形式对象，这些方案都是不安全的。对于随机oracle模型和泛型组模型也有类似的结果，但是随机oracle模型仍然被认为是现实世界中的一种很好的安全启发式方法(泛型群模型不那么理想)。

许多系统将注意力限制在各种形式的加密和数字签名上。这在某种意义上是好的，因为理想化很可能是正确的。另一方面，你甚至不能在正式系统中表达Diffie-Hellman，这意味着它没有那么有用。在可以表达Diffie-Hellman的情况下，组模型通常是非常有限的，这意味着正规系统可能无法表达涉及到组的微妙特性的各种攻击，因此，理想化的声音就不那么清晰了。

最终的结果是，具有良好工具支持并能够对您感兴趣的方案建模的正式系统是有用的，而且通常非常容易使用。传统的数学证明是有用的，但很难用。

Answer 2

答案肯定会在某种程度上是基于意见的，因为没有人能真正地说，人工检查是否比自动检查更有说服力。毕竟，如果成功地传达/出售给第三方，两者都是令人信服的。

从我个人的角度来看，最好的方法是手动验证自动验证的结果。因此，首先是自动验证，然后手动检查/验证自动验证工具(S)产生的正负结果。这样更彻底，你就能从这两个世界中得到最好的结果。

除此之外，请记住，没有"100%安全“这样的东西。

我们可以接近，但我们很可能永远无法达到完美的安全。