可证明安全

Provable Security

在密码学中，当我们已经设计出一个密码系统或协议时，我们不能直接说它是安全的，因为这样很缺乏信服力。可证明安全通常是用来确定一个密码系统或协议是安全的。

针对确定的安全目标，构造一个形式化的敌手模型及思维实验，利用概率论和计算复杂性理论，把敌手对密码算法或密码协议的攻击归约到对已知困难问题（大数分解，离散对数）的攻击。

目前对于安全性有两种角度的理解。

第一种称为“real vs random”，也就是如果加密所得的真实密文的概率分布，看起来和随机（均匀）选取一个密文一样，那么偷听者将无法从密文中获取信息。下面是形式化定义：

一个密码算法$\Sigma$有一次性的均匀分布的密文（one-time uniform ciphertexts），当且仅当

$k\larr \Sigma KeyGen\\ c\larr \Sigma Enc(k,m)\\ return\ c\\ = c\larr \Sigma C\\ return\ c$

第二种安全性的定义称为“left vs right”，也就是对于任意的两个明文，他们所得的密文的概率分布是一样的，因此无法区分。下面是形式化定义：

一个密码算法$\Sigma$有一次性安全性（one-time secrecy），当且仅当：

$k\larr \Sigma KeyGen\\ c\larr \Sigma Enc(k,m_L)\\ return\ c\\ = k\larr \Sigma KeyGen\\ c\larr \Sigma Enc(k,m_R)\\ return\ c\\$

两种安全性定义的关系

满足定义1,一定满足定义2，$L_{ots-real}^{\Sigma}=L_{ots-rand}^{\Sigma}=>L_{ots-L}^{\Sigma}=L_{ots-R}^{\Sigma}=$

证明：第1步将其拆成了库的调用，主要是因为已知部分的输入只有一个参数。然后第2步是使用了条件（real和rand等价）。第三步是因为rand算法的结果与输入参数无关，因此可以换参数。第4步再次使用条件，最后得证。

满足定义2,不一定满足定义1

只要给出一个反例即可。比如下面这个密码算法，它是在一次性密码本的基础上，密文末尾加了两个0。由于一次性密码本是满足定义2的，因此对于任意两个明文，末尾加0后，两者的密文的概率分布仍然相同，因此满足定义2。但是在当前的密文空间上，一个明文加密所得的密文必然以00结尾，不满足均匀分布，故不满足定义1。

如何证明不安全

无论是哪种安全性的定义，我们只需要找到一个程序A，使得安全性定义中的两个库的执行结果（概率）不一样，就能证明该密码算法是不安全的。

要证明如下两个库等价。显然，根据按位与的性质，对于real部分，如果输入的是全0，那么输出的密文一定是全0，这显然与右边的随机算法的输出的概率分布不同。

因此，可以找到如下的一个程序，这个程序将证明 $Pr[A\ L_{ots-real}^{\Sigma}=> true] =1,Pr[A\ L_{ots_rand}^{\Sigma}=>true]=\frac{1}{2^\lambda}$，因此两个库不等价

使用Hybrid方法证明安全性

根据安全性的定义，证明需要计算概率，如果密码算法十分复杂，那么可能难以计算。因此Hybrid方法是希望通过一些等价转换（中间的库就称为hybrids），将待证明安全的密码算法转化为已证明安全的密码算法，从而简化安全性的证明。在给出具体示例之前，先介绍一些引理。

引理1 $(A\ L_1)\ L_2=A\ (L_1\ L_2)$,前者可以理解为，程序A将一些L1的函数内联，生成一个只调用L2的程序，后者可以理解为是链接了一个复合库，即L1可以调用L2

引理2 $L_{left}=L_{right},\ L^*\ L_{left}=L^*\ L_{right}$

下面，给出一个简单的使用Hybrid方法证明安全性的例子：证明如下密码算法的安全性（定义1）。该密码算法是在一次性密码本（OTP）的基础上，多进行了一次加密（两次异或）。

这里的思路是希望转化为已证明过安全性的一次性密码本

因此第一步是转化为一次性密码本。第二步则利用了一次性密码本的安全性（等价），根据第二个引理进行替换。第三步是将库进行内联。最后简化无用代码。