可证明安全理论的发展

张曼君

（西安邮电大学 通信与信息工程学院 陕西 710000）

1 可证明安全含义

可证明安全是指密码协议可以从数学上被规约证明是安全的，能抵抗某些攻击。最早在这一领域做出贡献的是C.E.Shannon，他在信息论中首先提到了信息量的完善保密（Perfectly secret）概念。完善是指密码协议能抵抗所有的唯密文攻击，而不会透露密文所对应的任何明文消息。

对密码系统的有效攻击绝大多数是由于密码方案或协议存在很大的漏洞。假设好的密码原语存在，如何设计密码方案正是可证明安全性要解决的问题，它是一种将好的密码原语转化为好的密码方案的方法。

可证明安全的一般性方法如下：

确定密码协议的安全目标；

给出密码协议的形式化安全定义；

将攻击者完成攻击目标的方法归约为破译或者解决极微本原，从而达到证明协议安全的目的。

这一过程并没有直接证明密码方案或协议的安全性，如果发现了方案或协议的漏洞，就相当于发现了其中困难问题的解。如果我们相信后者是安全的，那么不用分析该方案或协议我们就证明了其安全性。有时也将“可证明安全”称为“归约安全”。

冯登国在可证明安全理论与方法研究一文中指出了目前多数安全协议的设计现状：

（1）传统方式：一种安全协议被提出后，在某种假定之下做出其安全性判断。如果在很长一段时间内都不能被破译，就接受其安全性；如果一段时间后发现该协议可能存在安全漏洞，于是对协议进行必要改动，再继续使用；这一过程可能周而复始。

（2）可证明安全：是一种归约方法。首先，确定协议的安全方案和安全目标，其次，构建攻击模型，再次，将攻击者的目标归约到解决某类密码学上的难题，最后，推翻原始假设，证明协议的安全性。

设计安全协议是非常容易出错的，因此有必要对协议进行安全性分析。传统上通过试错法来分析协议，但是该方法仅仅对于已知攻击具有检测能力，却无法检测未知攻击，因此经该方法检测为正确的协议，在一段时间后往往被发现存在安全漏洞。因此，学者们提出了多种安全协议的证明技术，以提供安全性准确可信的分析。目前，协议安全性证明方法基本分为两大类：形式化证明方法和可证安全法。

2 形式化方法

形式化方法又称作计算机安全方法。该方法源于计算机安全团体，强调对安全协议的自动化分析和描述。形式化方法最初来自Delov和Yao的安全威胁模型，在模型中，安全协议被划分成两个层面：协议技术层面和密码算法层面，密码算法被当作黑盒处理，模型将协议的运行用形式化方法进行分析。形式化方法根据设计思想可分为三类：逻辑推导法、模型检测法和定理证明法。

（1）逻辑推导法

牛奶燕麦粥。先把牛奶放微波炉里加热半分钟，然后把即食燕麦片倒进去搅拌，让它泡十几分钟就可以吃了。配鸡蛋、榨菜吃咸的，还是配葡萄干吃甜的，大家可以根据个人口味选择。

在逻辑推导法中定义一个逻辑公理集，通过可操作的抽像符号来表述协议的安全特性，并利用逻辑公理对协议各方的知识信仰进行推理，以期推出新的关于协议安全性的知识信仰。最著名的逻辑推导法是Burrows、Abadi和Needham提出的BAN逻辑。BAN逻辑的优点是概念清晰、简单，对于协议中的潜在安全漏洞能够有效地发现。但是，BAN逻辑中的假设以及理想化过程具有非形式化的特点，在推理的过程中可能会导致协议信息的丢失或不严格的重构，影响协议的安全性和可信度。随着BAN逻辑的推广，在此基础上出现了多种扩展协议，其中有GNY逻辑、AT逻辑、VO逻辑和SVO逻辑，他们被称作类BAN逻辑。除此之外，还有用于协议非否认性证明的Kailar逻辑。

（2）模型检测方法

模型检测方法主要考察协议状态之间的转换，将其以路径形式表达，从初始状态开始，搜索协议参与方或攻击者的可能路径。主要包括一般目的验证语言、单一代数理论模型以及特别目的专家系统。典型的一般目的验证语言包括MurÁ描述语言和通信顺序进程语言，这类语言把安全协议当作一般性的描述目标，遍历所有状态，对协议进行验证。单一代数理论模型包括Meadows模型和Woo-Lam模型等，这类方法对于安全协议的分析更有针对性，通过将协议转换为代数系统来描述参与方的状态，证明某一状态式不可达。特别目的专家系统为了证明协议的漏洞，从不安全状态出发，以证明初始状态到此不安全状态是有效路径。其中有代表性的方法包括NRL分析器和Interrogator询问器。

（3）定理证明方法

定理证明法先对协议进行形式化，在此基础上对其进行模型化和归约，为了证明协议满足某种安全属性，需要证明归约在模型中成立。主要包括Paulson归纳法、Schneider秩函数、串空间模型和Spi-演算等。定理证明与模型检测的区别在于，前者是从协议的正面入手，而后者试图针对反面，寻找各种可能的攻击。定理证明无需检测工具，且过程简单明了。

形式化方法是对于人类智慧和经验模型化了的专家系统，该方法在论证协议不安全方面是有效的，它能够查找协议中的安全漏洞。但是该方法对于攻击者的模型定义不够全面，主要考虑被动攻击；而且该方法将密码算法作为黑盒处理，因此无法发现因为密码算法的不合理带来的安全漏洞。

3 可证明安全方法

可证明安全方法起源于密码学团体，最初来自Goldwasser和Micali的研究。在公钥签名体制的可证明安全的发展过程中，Goldwasser等人在80年代中期提出了最重要的成果，攻击者获得适应性所选择消息的签名后，仍然不能以不可忽略优势伪造一个新消息的签名。该方法应用计算复杂性理论，通过对敌手攻击成功概率和计算代价的评估来判断协议的安全性。

可证明安全方法包括以下三个方面：

困难问题：公认在多项式时间内得到解决的概率是可忽略的问题。

安全性定义：是可证明安全方法的关键。其中定义了攻击者的行为和目的。对攻击者的行为，即可能的攻击方法进行形式化描述；攻击者的目的即攻击协议要达到的目标。当协议中的攻击者具有最强的攻击行为且目的最简单，就称协议具有最好的安全性。其中包括BR模型、基于BR的扩展模型BR95、WJM97，和基于组合以及模块思想的模型，例如CK模型、UC模型等。

归约方法：归约方法是可证安全理论中最常用到的工具，可证安全的主要技巧在于从攻击能力到困难问题的归约。对协议进行证明时，首先要构建安全模型，为攻击者提供一种虚拟环境，使其发挥攻击能力；还要建立挑战算法，将安全问题归约为数学难题，并且在模拟过程中将数学难题暗中嵌入，引导攻击者解决该难题。目前的主流方法包括标准模型和随机预言机模型。

4 随机预言机模型下的可证明安全

在随机预言机模型(Random Oracle Model：ROM)中，允许协议各方对其进行问询，证明者首先完成在这个模型中方案的安全性证明，利用哈希函数模拟随机预言机，在哈西函数没有缺点的安全论断下，随机预言机的证明保证了协议的安全性。

在随机预言机模型中，归约论断如下进行：首先对方案满足的安全性进行形式化定义，假设在概率多项式算法中，攻击者能够以不可忽略概率成功攻击方案；其次，为攻击者提供其所需的模拟环境，即随机预言机，对攻击者的询问予以回答；最后，将数学上的困难问题嵌入模型中，利用攻击结果解决数学难题。在模型证明过程中，用哈希函数模拟随机预言机，协议参与者都能对其进行访问，通过利用攻击者的攻击行为来求解困难问题。利用上述证明过程得到的模型即随机预言机模型。

1993年，Bellare和Rogaway两位学者正式提出了ROM方法论，自此，可证明安全方法从理论研究走向实际应用，随之产生了多个安全方案，同时，具体安全性的概念得以提出，安全性的渐进度已经满足不了人们对于安全性的衡量，取而代之是得到确切的安全性度量。

5 标准模型下的可证明安全

标准模型将密码学原语视为基础部件，通过某种方式利用这些基础部件构造更强大的原语。在ROM中证明了的方案安全并不能保障该方案在现实生活中的安全性。目前有许多安全方案可在ROM中证明安全，但是在实际应用中却不能构造出与方案对应的实例。与之相比较，可证安全性在标准模型中更具现实意义。标准模型虽然也是通过预言机对于询问进行应答，但与ROM不同，预言机内部映射要符合方案中的具体函数关系，因此，增加了设计难度。

虽然随机预言机模型不能成为方案安全性的绝对证明，但是，作为方案安全性的一种必要测试工具，ROM可以排除多项安全隐患。在ROM下设计简单有效的可证明安全协议，能够抵抗多种未知攻击。但是仍有一些学者坚持使用标准模型来证明协议的安全性，他们认为，在ROM中将哈希函数当做理想的随机模型是强假设，而且，ROM中证明的协议安全性和通过哈希函数获得的安全性没有必然的因果关系。事实上，所有标准模型下的可证安全协议在设计上都过于复杂，ROM设计上较为简单，实用性更强。因此，客观上来说，目前的安全方案至少要能够达到ROM下证明的安全性。而设计安全协议的目标应放在具有标准模型下可证明的安全性，以及ROM下的简单高效性。