安全协议的形式化分析技术方法研究

付浩

摘要：安全协议是解决网络安全问题最有效的手段之一。然而，由于互联网的开放性和协议的并发性，安全协议的设计和分析一直是一个复杂而困难的问题。实践证明，借助形式化的方法或工具分析安全协议是非常必要而且行之有效的。安全协议的形式化分析已有三十多年的历史，一直存在两类不同的方法：计算方法和符号方法。符号方法用形式化语言和符号推理对协议进行分析和验证，更容易实现自动化分析。但是由于对密码学原语和攻击者能力的理想建模，使得这类分析方法的肯定性结论往往并不直接具有现实意义，被认为没有真正建立起密码学的可靠性。

关键词：安全协议；符号方法；计算方法

随着信息技术和网络技术的飞速发展，互联网的广泛应用已成为社会进步和发展的重要标志之一。然而，由于网络的开放性，它给人们的生活带来极大方便的同时也带来了许多安全隐患。安全协议是解决网络安全问题最有效的手段之一，安全协议的正确实施对于保障网络虚拟世界中各种组织和系统、各种商务和交易的安全运行起着十分关键的作用。安全协议”（也称密码协议）是建立在密码体制基础上的一种通信協议，它运行在计算机网络或分布式系统中，借助于密码算法为实现密钥分配、身份认证、电子商务交易等任务的各方约定一系列执行步骤和执行规则。

由于安全协议中各消息之间存在着复杂的相互作用和制约关系，许多设计并投入实际应用的安全协议在运行时不一定能够真正实现它所声明的安全性质。据英国学者Gavin Lowet估计，在已公开发表的安全协议中，有超过一半的安全协议实际上不能实现它所声明的安全性质。造成安全协议失败的原因主要在于：1）协议设计者对安全陸需求（目标）的定义和刻画不完全、或理解上有偏差；2）协议分析者对设计出来的安全协议是否满足安全性需求缺乏足够的、全面的安全性分析。

自20世纪70年代末以来，安全协议的分析已经成为一个研究热点。但是，由于安全协议设计与分析的复杂性，使得该研究变得十分困难并具有挑战性。安全协议的分析方法主要有两大类：攻击检验方法和形式化分析方法。攻击检验方法根据已知的各种攻击方法对协议进行攻击测试，以攻击是否有效来检验协议是否安全。

自上世纪八十年代开始使用形式化方法对安全协议进行分析以来，安全协议的形式化分析就存在两类截然不同的方法：计算方法和符号方法。这两类方法都是通过对安全协议的执行过程和攻击者能力建立数学模型，以及对安全协议的安全性需求给出形式化定义，实现对协议安全陸的严格证明。

计算方法（也称可证明安全方法）一般是在计算复杂性理论框架下的一种“归约”方法，将对安全方案或者协议的攻击有效变换到对大整数分解和离散对数等困难问题的求解，其结果更具密码学可靠性。在计算方法的协议建模中，安全协议执行时产生的消息是二进制位串，各种密码学原语是一个多项式时间算法，而攻击者（也称敌手）是一个关于安全参数多项式时间计算的图灵机。协议的安全性通过概率和计算复杂度表示，即攻击者不能经常且轻易地做一些坏事情。计算方法以其复杂的定义和定理强化了密码学基础，对设计和研究某些协议起了很重要的作用。但是，也正由于这些特点使得其证明较复杂，不容易验证。对具体协议的分析与论证往往需要发现较特殊的证明途径，很多细节难以很好把握，基本上都是手工证明，导致即使分析中等规模的安全协议，其证明也耗时较长且容易出错。

符号方法（也称Dolev-Yao方法）用形式化语言和符号推理进行协议分析和验证，更便于对协议的自动化分析。在符号方法的协议建模中，消息都是形式化的符号表达式，各种密码学原语的理想安全属性通过对这些表达式应用各种符号操作得到，这些符号操作像一个黑盒，而不是基于二进制位串的具体密码学算法。符号方法通常以Dolev-Yao模型或扩充的Dolev-Yao模型作为安全协议攻击者模型，攻击者只能对符号表达式施行一些给定的符号操作，但没有计算时间限制。符号方法具有自然而强有力的密码学直觉，近年已用于许多协议的设计和分析，并肯定一些现有协议的安全性以及发现很多协议的攻击。但是，基于高度抽象的符号形式特征往往不能准确地表达协议的安全性质，因此这类分析方法的肯定性结论未必具有现实意义（即使符号分析方法断言一个协议是“安全”的，其未必在现实中是安全的）或密码学可靠性。

综上所述，表1给出了计算方法和符号方法的比较。现在普遍的认识是：基于计算复杂性的计算方法是（密码学）可靠的，但是证明过程是高度创造性的手工数学式证明，这对于目前越来越复杂的安全协议，不仅证明本身越来越复杂，而且证明的正确性也越来越不容易；而大多数建立于Dolve-Yao模型之上的符号方法借助于符号演绎体系的演算机制，证明过程容易实现自动化，但是由于对密码学原语和攻击者能力的理想建模，使得某些类型的肯定性结论往往并不直接具有现实意义，被认为没有真正建立起密码学的可靠性。

通过为安全协议的符号方法建立更精确的计算密码学语义，对密码学原语的实现提出明确要求，还可以证实或改善协议的形式化证明与该协议具体实例之间的关联。

计算方法，也称可证明安全方法，本质上是一种“归约”方法：首先形式化的定义安全方案或协议的安全目标；然后根据攻击者的能力构建一个形式化的攻击者模型，严格定义攻击者所掌握的攻击手段和资源；最后通过安全性证明指出，如果存在攻破某个安全方案或协议的攻击者，那么我们可以使用这个攻击者作为子程序来构造解决某个已知计算难题的有效算法。由于我们相信某些计算难题的有效算法是不存在的，因此我们得到结论：不存在攻击者能够以不可忽略的概率攻破该安全方案或协议。