密码学中的形式验证

#1 楼

免责声明：我每天使用Coq ...




在某些地方，我发现人们使用正式验证和/或计算机辅助验证来进行加密。


据我所知，没有很多地方可以做这样的事情。


首先，让我们定义一下概念：

形式验证：使用形式化的数学方法证明某种形式规范或属性的算法正确性的行为。

计算机辅助证明：一种已经存在的证明

一些示例（在密码学中）：



密码原语的验证：SHA-256（纸质）

基于游戏的加密证明（PHD）的正式认证

和一些阅读材料：



关于通过抽象解释对计算机系统进行正式验证（论文）

加密的基础证明框架raphy（PHD）

密码学中的计算机验证（纸）

加密实现的概率关系验证（纸）



如何

在正式方法（无论是哪个领域）中，有两种方法：


规范$ \ rightarrow $软件
规范$ \ wedge $ Software $ \ rightarrow $证明软件的正确性。

在大多数情况下，第一种方法是所用的方法。为什么？因为从正式的规范开始比较容易，然后逐步通过经过验证的步骤，最终可以使用该软件（因此被证明）。例如，该经过认证的编译器：


例如在方法B中，过程如下：
$$ DEFINE \ / \ SPECIFY \ rightarrow PROVE \ rightarrow REFINE \ rightarrow证明\ rightarrow \ ldots \ rightarrow IMPLEMENT $$

形式验证使用Hoare逻辑，Hoare逻辑是一组允许我们推理程序的规则。它基于演算和自然演绎。它依赖于Hoare三元组：
$$ \ {P \} \ C \ \ {Q \} $$
当满足前提条件$ \ {P \} $时，命令的执行$ C $建立后置条件$ \ {Q \} $。如果命令$ C $从状态$ s $变为状态$ s'$。
$$ C：s \ rightarrow s'$$
那么您将必须证明：
$$ \ forall \ s \ s'，P [s] \表示C：s \ rightarrow s'\表示Q [s'] $$
，但我们更喜欢Hoare三元符号（更轻）。

例如，这是$ SKIP $的规则（也称为不执行任何操作）：
$$ \ frac {} {\ {P \} \ SKIP \ \ {P \}} $ $

这是序列的规则：
$$ \ frac {\ {P \} \ C_1 \ \ {Q \} \ \ \ \ \ \ \ \ {Q \} \ C_2 \ \ {R \}} {\ {P \} \ C_1; C_2 \ \ {R \}} $$
该符号表示为：
“如果$ \ {P \} \ C_1 \ \ {Q \} $（是$ \ text {True} $ ），如果$ \ {Q \} \ C_2 \ \ {R \} $，则可以推断$ \ {P \} \ C_1; C_2 \ \ {R \} $。

证明因此是从下到上构建的：如果要证明$ \ {P \} \ C_1; C_2 \ \ {R \} $，则需要​​证明其中有$ Q $，例如$ \ {P \} \ C_1 \ \ {Q \} $和$ \ {Q \} \ C_2 \ \ {R \} $。

有关Hoare逻辑的一些读物：



关于Hoare逻辑（课程）的背景阅读

讲义C2：关于代码（Hoare Logic）的推理（课程）

Software Foundation（自学课程，高度学习）如果想进入该领域，则建议使用。）


工具

在正式方法中，有两种工具：


全自动证明者
证明助手

第一个主要基于Atelier B和Alt-Ergo等SMT（可满足性模理论）。 >
第二个基于纯逻辑。您为其提供引理（帮助定理），这将确保您在证明中所做的每一步都是正确的。这是一个非常彻底的过程，非常缓慢。但是最后，您知道您的证明是如何工作的，并且它是正确的，因为您没有错过任何假设。该过程可能令人沮丧，将确保证明有效。
主要的证明助手如下：Coq，
Isabelle，Agda，Fstar和HOL。

您提到的工具（ProVerif，CryptoVerif）并非专用于加密原语，而是协议验证。我不认识他们，所以我不会发表评论。确实存在关于同一主题的其他工具。例如：


CertiCrypt

EasyCrypt（教程）

是的，它们基于Coq。

在C语言中，为了能够验证您的代码是否符合规范（例如对$ \ text {SHA-} 256 $所做的工作），需要从代码中提取语义。这可以使用可验证工具链或Why3来完成。第一个将为您提供一个Coq文件，您可以从中开始打样。在给定的C ASCL工具代码的情况下，第二个代码将使用frama-c并尝试使用上述SMT证明来证明其属性。在失败时，它会产生目标，并要求您通过Coq进行证明。


在密码学（和数学）中

我已经提到了证明协议的想法（ cf EasyCrypt等人），对于密码证明，想法基本相同。使用逻辑属性进行指定。

Coq示例（对于本科生来说很容易用手证明）：
$$ \ forall \ fg，f \ text {是内射性} \ implies g \ text {是内射} \暗示g \ circ f \ text {是内射} $$

Require Import Coq.Sets.Image.

Theorem injective_trans:
forall A B C (f: A -> B) (g:B -> C) (h:A -> C),
(forall x, h x = g (f x)) -> injective A B f -> injective B C g -> injective A C h.
Proof.
intros A B C f g h H_h_equal_g_f H_f_injective H_g_injective.
unfold injective in *.
intros x y H_h_x_y.
apply H_f_injective.
apply H_g_injective.
rewrite <- H_h_equal_g_f.
rewrite <- H_h_equal_g_f.
apply H_h_x_y.
Qed.

以下是Coq中著名的证明定理的列表。


最后一个单词

Keccak的安全范围已通过计算机得到证明。但是他们的过程不同：他们详尽地生成了线索并显示了属性。因此，它是计算机辅助的，但未经验证。

最后，来自FSE 2016的最新论文：加密实现的可验证侧通道安全性：恒定时间MEE-CBC


正如SEJPM所指出的那样，本文也是另一种方法（更多基于游戏）。他们创建了一个分析器，该分析器生成了满足AE方案的密码方案。但是，我不知道他们是手动证明自己的属性还是使用了证明助手（考虑到他们使用Ocaml对分析仪进行编码，可能会实现）。


您可能也对Gilles Barthe（EasyCrypt团队）在这里所做的课程感兴趣。

我不知道我的回答是否有帮助。我知道它并不主要针对密码学，但我希望它能使您对事物的工作方式有所了解。

#2 楼

形式验证用于验证算法或协议的安全服务。它使用特定的高级建模规范来指定您的安全解决方案，并使用后端正式验证工具来查看是否存在安全漏洞。正式验证的结果将告诉您协议是安全还是不安全。我建议您看看AVISPA，这是最常用的用于验证Internet协议安全性的内容之一。