安全协议形式化分析方法研究综述
2024-06-07缪祥华黄明巍张世奇张世杰王欣源
缪祥华 黄明巍 张世奇 张世杰 王欣源
作者简介：缪祥华（1972-），副教授，从事信息安全、网络安全和移动通信安全的研究。
通讯作者：黄明巍（1998-），硕士研究生，从事信息安全的研究，1104331869@qq.com。
引用本文：缪祥华，黄明巍，张世奇，等.安全协议形式化分析方法研究综述[J].化工自动化及仪表，2024，51（3）：367-378.
DOI：10.20030/j.cnki.1000?3932.202403001
摘 要 介绍了安全協议的基本概念和分类，然后对安全协议形式化分析方法进行了详细介绍，包括基于模态逻辑的方法、基于模型检测的方法、基于定理证明的方法和基于可证明安全性理论的方法。其中，基于模型检测的方法是目前应用最广泛的一种方法，因此详细介绍了一些常用的基于模型检测方法的工具。最后，总结了当前安全协议形式化分析方法的研究热点和未来的发展方向。
关键词 安全协议 形式化分析 模态逻辑 模型检测 定理证明 可证明安全性
中图分类号 TP309 文献标志码 A 文章编号 1000?3932（2024）03?0367?12
随着计算机技术的发展，其已应用到社会生活的方方面面，成为推动社会进步的主要力量。但是，信息安全问题也变得越来越突出，越来越复杂，已经上升到了国家安全层面，因此，解决信息安全问题显得刻不容缓。安全协议作为一种行之有效的安全保障手段，引起了越来越多研究人员的关注，使其成为了信息安全研究领域中的一个重要研究热点。
安全协议形式化分析可以有效地找出协议存在的漏洞并评估协议的安全性。安全协议形式化分析方法主要有四类，分别是模态逻辑、模型检测、定理证明和可证明安全性理论[1，2]。模态逻辑采用的方法通常以“A knows P”和“A believes P”为核心，即以知识为基础和以信仰为基础，模态逻辑方法可以深入探究安全协议执行过程中各实体的知识集合和信仰目标的变化。通过使用自动化工具，模型检测方法可以将安全协议看作分布式系统，并且定义安全属性或不变关系，以便对每个实体的状态进行推导，确定它们能够达到的全局状态，从而判断协议是否存在缺陷。定理证明则是通过将协议抽象为一个公理系统，并将其中的定理作为证明的依据，可以通过确保其定理的正确性，从而有效地检验安全协议的安全性。可证明安全性理论的方案是将协议安全性通过随机预言机模型归纳到某个困难的、难以攻破的难题上，通过难题的难以攻破性来确保协议的安全性。四种体系中对于安全分析的侧重点各有不同。笔者对此四者进行归纳总结概括，并分析比较各类方法的优缺点。
1 相关信息
1.1 安全协议的基本概念及分类
协议是一种由多个参与者（至少两个）共同协作行为的规则，协议旨在通过一系列的步骤来实现特定的目标。虽然有时单个参与者也可以完成这些步骤，但是仅仅依靠单个参与者是不能构成协议的，因为它们之间还需要其他的协作伙伴的参与才能构成完整的通信，从而达到协议所要完成的目标。然而在此过程中必然涉及到了信息的交换，因此协议的每一个参与者就会对消息的机密性、其他通信对象身份的真实性等安全属性有一定的要求。
通常，根据安全协议设计的不同目的，可将其分为以下几类：
a. 密钥交换协议。这种协议旨在在两个（或多个）相互依赖的个人（或组织）之间传输私有的数据，通常它们可以使用对称和非对称的加密技术来保护数据的安全性。
b. 认证协议。通常而言，在消息认证的过程中，协议往往会受到伪造、篡改及否认等攻击，为了解决此类攻击，则必然需要确定通信过程中的某些信息是否会被篡改，例如消息的轮次序号、通信双方的身份等安全属性。而认证协议就是用于解决这些攻击的。
c. 认证及密钥交换协议。这种协议既包含了传统的认证机制，也包含了一种新型的SK（密钥）交换机制，它能够在实体认证完成之后，利用密码算法生成的PSK（主密钥）来确定会话SK，从而提供更高效的安全保障。目前，这种协议在互联网中应用最为广泛，例如IKE协议、DASS协议等。
d. 电子商务协议。电子商务协议是一类特殊的协议，区别于上面三类协议的是，电子商务协议是为了保障交易双方的合法权益，即最大程度地保障公平性而存在的。它更多地关注在交易过程中主体双方的利益或者在目的不一致甚至是相互冲突的情况下以求保障双方不能通过损害对方利益来使得自己获利，从而保障商务交易的公平性。
1.2 安全协议形式化分析方法的发展
自1978年NEEDHAM R M和SCHROEDER M D提出安全协议形式化分析[3]的概念以来，已经45年有余，而他们所得到的研究成果也为安全协议形式化分析领域的发展做出了重大贡献，伴随着时间的推移，对于这一领域的深入探索也逐渐受到了重视。1983年，DOLEV D与YAO A C联手构建出一个被称作Dolev?Yao模型[4]的安全模型，该安全模型通常被用来评估安全协议的可靠性。该模型可以清晰地反映出网络攻击的特征、行动以及可能的威胁，但它仍有一些不足之处，比如无法检测到在迁移状态过程中加入用户，且只能查找部分漏洞，仅可以检测出部分缺陷等。随着时代的发展，许多研究人员都在尝试修正和改进Dolev?Yao模型存在的缺陷和漏洞，并将该研究的成果进行实际应用，从而得到了诸如Dolev?Even?Karp[5]以及基于状态空间的加密协议[6]等协议模型。
BAN逻辑是在DOLEV D与YAO A C之后，于1989年由Burrows、Abadi和Needham三位研究者提出的一个十分具有代表性的模态逻辑，BAN逻辑的出现意味着安全技术的形式化分析技术正式步入一个以信念逻辑为核心的新阶段。BAN逻辑通过将安全协议的过程和假设进行形式化，从而将安全协议的安全性证明转化为对于数学假设命题的成立与否的逻辑推理，使得其安全性依赖于假设命题的成立。尽管BAN逻辑存在一定的局限性，但它仍有其独特的优势，所以后来的研究人员以BAN逻辑为基础，相继开发出了GNY逻辑、AT逻辑、VO逻辑[7]及SVO逻辑等更加先进的类BAN逻辑。
1996年，Lowe利用通信顺序进程技术（CSP），成功地实现了对安全协议的形式化分析，此后，CSP的技术性应用时代也随之而来。随后，Schneider利用CSP语言，提供了一种有助于识别和核实认证属性的更加普遍的技术。
1999年Fabrega、Herzog和Guttman提出了Strand space（串空间）理论，Paulson提出了Paulson归纳方法，由此，定理证明方法进入了研究者们的视野。定理证明的方法有多种，例如Coq证明系统[8]、公理证明器HOL[9]及Isabelle定理证明系统[10]等。有的定理证明的验证过程可以通过模型检测工具或定理证明器来加以验证，例如Paulson归纳方法和串空间方法这两种与Petri
网[11]有着密切关系的方法就可以通过特定的定理证明器加以验证。
可证明安全性的概念是由Goldwasser、Micali及Rivest等在20世纪80年代初提出的，提出后该方法就快速地被运用到了加密、签名方案以及安全协议形式化分析上，但是这些方案通常只具有理论意义，因为其设计时大量地牺牲了效率来提高其安全性。直到“面向实际的可证明安全性（Practice?oriented Provable?security）”的概念和著名的随机预言机（Random Oracle，RO）模型被提出，该领域在实际运用上才取得了长足的发展。
笔者主要概括归纳了四大类方法，即基于模态逻辑的方法、基于模型检测的方法、基于定理证明的方法和可证明安全性的方法。
2 基于模态逻辑的安全协议形式化分析方法
基于模态的逻辑方法也称为基于推理的结构性方法。模态逻辑本身是逻辑学的一个分支，在形式化安全协议分析中常以演绎推理的形式存在。此类技术是从用户发送和接收的消息出发并根据演绎法的多个推理公理来进行演绎推理，从而判定安全协议是否可以达到预想的安全预期[12]。一般而言，该类逻辑系统可以分为两类：基于知识的（“A knows P”）和基于信仰的（“A believes P”）。这两类系统的主要区别在于：
a. 基于知识的一般表述为，如果实体知道P，则P是正确的。
b. 基于信仰的实体对于P的信仰不涉及P的正确性，即如果实体信仰P，则P一定正确，无论P本身是否正确。
根据基于信仰的逻辑系统，学者们提出了著名的BAN逻辑。
2.1 BAN逻辑
BAN逻辑[13]被誉为安全协议形式化分析方法研究的一个重要标志，它的提出者是Burrows、Abadi和Needham，他们的研究成果为后续的协议分析提供了重要的理论支撑，并且这些研究在许多方面都取得了重大的突破。BAN逻辑是一种以信仰为基础的形式化理论分析，它由7类共19条逻辑推理法则组成，可以根据信号的发送和接收情况来评估参与者的最终信仰是否符合预期的结果。
尽管BAN逻辑在长期的实践中取得了一定的成效，但它仍然存在一些明显的缺陷，比如理想化过程不够规范，初始化假设不够合理，缺乏完整性以及没有一个清晰明确的语义定义。BAN逻辑的发展为GNY逻辑的出现提供了坚实的基础，使得它对安全协议在模态逻辑分析中可以使用的范围得到了极大的拓展，从而大幅提升了其分析能力。
2.2 GNY逻辑
1990年，GONG L等学者以BAN逻辑为基石，提出了GNY逻辑[14]，它大幅拓宽了BAN逻輯的范围，GNY逻辑自身包含的逻辑推理公式相对于BAN逻辑增加到44条，并且GNY逻辑努力尝试消除主体诚实的假设、消息源假设和可识别假设。在“拥有”和“可识别”的基础上，GNY逻辑将“不是由此首发”的理论纳入到每轮的形式化协议中，并将其作为一个重要的组成部分。
GNY逻辑尝试在BAN逻辑的基础上进行改进，但是由于GNY逻辑的复杂性，它的效果未能达到预期，甚至被一些学者批评无法实现正确的分析，但这并未阻止它为模态逻辑的发展带来新的可能性。
2.3 AT逻辑
AT逻辑[15]源自ABADI M和TUTTLE M R的工作，它的基本理念是逻辑的结构必须符合逻辑的要求，而且这种结构必须不受逻辑的限制。这一概念是第1次被引入，极大地拓展了AT逻辑的范畴，有效地改进了它的表述效果。AT逻辑在BAN逻辑的基础上，大幅提升了其功能和性能：
a. 从语义的角度分析改进了BAN逻辑，并且剔除了语义与现实细节相混淆的部分;
b. 更加直观地定义了一部分逻辑定义;
c. 将全部的逻辑连接词引入系统，改写推理规则为公式，并且给出了形式化的语义;
d. 证明了推理系统的合理性。
然而AT逻辑仍然存在一定的缺陷，比如个别公理存在一定的漏洞等。
2.4 SVO逻辑
在对BAN逻辑、GNY逻辑、AT逻辑及VO逻辑进行了分析和总结后，SYVERSON P F和 VAN OORSCHOT P C提出了SVO逻辑[16]。SVO逻辑大幅改变了AT逻辑的表达方式，它以一种更加清晰的方法来表达概念，从而解决了传统模态逻辑存在的模糊性问题，同时SVO逻辑也具有良好的拓扑性，易于实际应用。该类逻辑的出现，意味着以BAN逻辑为基础的一大类逻辑的发展成熟。
2.5 Kailar逻辑
Kailar逻辑旨在解决BAN逻辑和类BAN逻辑在商业应用中存在的可追究性、不可否认性等问题，它能够帮助主体证明另一方对于某个行为的发起是有责任的，从而使得双方能够达成共识。
2.6 ZQZ逻辑
ZQZ逻辑是一种基于模态逻辑的形式化验证方法，用于对安全协议进行分析和验证，它由中国学者周典萃、卿斯汉和周展飞提出，因此被称为ZQZ逻辑[17]。ZQZ逻辑基于模态逻辑，是为了针对Kailar逻辑在电子商务协议分析方面存在不足而提出来的，该逻辑通过对收发双方的不可否认证据进行收集，然后用该证据来保证协议的公平性、可追究性等，ZQZ逻辑可以通过扩展的方式形成扩展ZQZ逻辑，从而分析更多的复杂协议，例如引入对时间的刻画来分析不可否认协议等[18]。
2.7 Bieber逻辑
尽管BAN和大部分的类BAN逻辑均建立在信仰的基础上，但并不意味着基于信仰的模态逻辑就是完美无缺的，即人们可能会盲目地相信某种信仰，这种信仰的正确性仍然需要进一步的讨论。于是Bieber利用CKT5技术构建一种全新的、基于知识的安全协议，它的核心思想就在于Bieber逻辑[19]，该思想有效地解决了基于信仰的模态逻辑分析方法中存在的问题，并且由Bieber逻辑构造的协议可以在不同的或者不确定的通信环境中保持稳定，且可以有效地保护参与者的隐私。
2.8 非单调逻辑
非单调逻辑[20]是由Rubin博士提出的，旨在解决因为主体获得信仰（知识）后长期信仰（认为）这些事件是正确的而导致问题产生的情况。此方案有4个特点：
a. 这是第1种能够有效地探索和分析复杂安全协议的技术;
b. 无理想化过程;
c. 分析过程紧密结合于形式化描述;
d. 形式化描述与协议具体实现过程接近。
3 基于模型检测的安全协议形式化分析方法
一般来说，基于模型检测的方法通常需要借助自动化的分析软件。模型检测的方法基本都是基于有限状态机原理，通过有限状态机原理，可以采用一些新的方法来构建一个能够有效检测、识别异常状态和特定状态的状态迁移函数，从而有效证明所要分析的安全协议的安全性。这种方法采用穷举的策略，能够有效地检测出不同状态之间的关联，并且能够有效地实现状态的迁移和识别。该方法的特性表现为极高的自动性，能够根据缺陷快速创建相应的案例，然而不容忽视的是模型检测方法存在着两个明显的缺陷：
a. 主体数目必须有限;
b. 穷举搜索会带来状态空间爆炸问题。
尽管如此，采用模型检测方法，研究者们也取得了十分显著的成果。
3.1 Dolev?Yao模型
Dolev?Yao模型被认为是模型检测方法的基石，它不仅提供了一种有效的安全协议形式化分析方法，同时还引入了一个强大的敌手模型，即假定这个敌手模型能够有效地识别出攻击者，并且能够有效地预测攻击者的行为，其特点如下：
a. 已经完全控制了网络;
b. 仅限于特定的加密原语和操作。
这两个特點被称为完美的密码学假设。当然，Dolev?Yao模型并不完美，仍然存在一些缺点，例如无法针对特定的安全漏洞来分析、攻击者模型过于强大使得分析困难等。
3.2 CSP方法
通信顺序进程（Communicating Sequential Processes，CSP）[21]是一种基于代数理论的方法，
它将参与者视为一组独立的进程，每一组进程都可以被视为一个事件，这样整个协议就可以被组织成一个完整的CSP，里面的每一个程序都可以并行运行，并且可以与外部环境进行交互。通过对协议说明的分析，CSP方法可以抽取出相关的模型，并利用故障发散提炼（Failures Divergence Refinement，FDR）技术，以证明协议的安全性。
3.3 NRL协议分析器
NRL协议分析器[22]是利用Dolev?Yao模型的术语重写模型而构建的。NRL模型采用了信仰集合的方式，通过不停地生产“词”“信仰”“时间”来模拟消息的生产和接收，从而达到信仰变化的目的。其中“消息”由“词”构成，而“时间”的迁移则可以表示“信仰”的修改和变化状态过程，从而对攻击者进行分析。
3.4 Mur?模型
通常Mur?模型[23]一般应用于工业的安全协议形式化分析方面，Mur?模型经过编译后产生C++文件，此模型用于描述有限异步并发系统，采用列举法来验证是否所有状态都可以达到规定下的安全属性，为了提高协议的分析效率，Mur?模型支持深度优先和广度优先两种算法。
3.5 Brutus模型
Brutus模型主要采用数学模型法将协议进行转化，将协议的安全属性通过一阶逻辑进行描述并辅以状态空间搜索和自然推理相结合的方法来对模型进行验证，并且Brutus模型采用偏序状态缩减技术和对称状态缩减技术来对状态空间进行缩减，从而降低状态空间爆炸的可能。
3.6 以攻击者为中心的安全协议验证机制（SSMCI）
SSMCI是一种新型的安全协议自动化验证方法[24]，它与传统的基于模型检测和定理证明的验证方法不同，它将攻击者视为协议的一部分，并且建立以“需求”为核心的知识集合，从而建立以“需求”为核心的攻击者模型。该模型采取了回溯机制来确保在协议迁移过程中，敌手的知识集合能够正常增长，从而考虑攻击者的能力和策略，进而更加准确地评估协议的安全性。此机制的实验验证总体表现优于Scyther?proof等工具。以攻击者为中心的安全协议验证机制具有很高的准确性和实用性，它能够更加真实地模拟攻击场景，考虑攻击者的能力和策略，从而更加准确地评估协议的安全性。不过，值得注意的是，攻击模型的定义和建模需要考虑到协议的复杂性和实际应用场景，同时需要对模型进行测试、验证等。
3.7 基于模型检测的常用分析工具
3.7.1 Scyther?proof工具
Scyther?proof工具是一种用于验证安全协议的工具，它使用Scyther工具来分析协议的安全性。Scyther是一种模型检测器，可以自动化地验证协议的安全性和正确性。Scyther?proof工具使用Scyther检测器来自动化地检查协议的安全性，并生成报告，指出可能存在的安全漏洞和风险。这种工具可以帮助保护网络和系统免受攻击并避免数据泄漏。Scyther?proof工具通过生成Isabelle/HOL定理证明器的证明脚本进行检测，对安全性的验证是通过对类似搜索树的检测来寻找协议存在的问题。但是其对代数运算支持较差，使用者需要将代数运算进行模拟才可以在工具中使用。
3.7.2 Tamarin工具
Tamarin工具是一种用于形式化分析协议的工具，可以检查协议的安全性和正确性。它使用基于Dolev?Yao模型的形式化语言来描述协议，并使用符号执行技术来自动化地分析协议的安全性。Tamarin工具可以检测协议中的安全漏洞和攻击，例如中间人攻击、重放攻击及欺骗攻击等。它还可以验证协议的正确性，例如保证协议的认证、保密、完整性及可用性等。Tamarin工具是一个开源工具，可以在Linux、Mac OS X及Windows等操作系统上运行。它提供了一个易于使用的图形用户界面，可以帮助用户快速创建和分析协议。Tamarin工具已经被广泛应用于许多领域的安全协议形式化分析上，包括网络安全、物联网、金融及医疗保健等。Tamarin工具是在Scyther工具的基础上进一步地完善了其功能，同时支持自动和交互验证，并且支持迹属性的规范，其通过对安全属性和安全引理的双重约束来寻找不安全状态的迹，从而找出协议漏洞。该工具支持Diffie?Hellman、双线性对等代数运算。
3.7.3 ProVerif工具
ProVerif是一种自动化的形式化验证工具，用于验证安全协议和分布式系统的安全性。它可以检查协议的保密性、完整性及可用性等方面的安全性，并且能够自动发现协议中的漏洞和攻击路径。ProVerif支持多种协议语言，包括CSP、pi演算、lambda演算及Dolev?Yao模型等，并且能够自动推理出协议的安全性。同时ProVerif分析器是一个高度抽象化的、注重敌手知识集的分析工具，这也导致了该工具不适合处理各种状态性协议的问题。该分析器将协议规范为Horn族，或者使用pi演算后再进行转化，然后进行分析。该工具试图找出与安全规范相悖的反例，从而构建出攻击的一个迹。当然该工具也支持代数运算。
3.7.4 Maude?NPA工具
Maude?NPA是一种基于Maude系统的形式化验证工具，用于验证分布式系统和协议的安全性。它使用一种被称为NPA（Non?deterministic Pushdown Automata）的形式化语言来表示协议的安全性，并且能够自动化地分析协议的安全性。Maude?NPA的工作原理是将协议转换为一个Maude模型，然后使用NPA语言来描述协议的安全性。该工具能够自动化地生成验证条件，并使用Maude模型检查器來验证这些条件。它还能够生成证明来证明协议的安全性。Maude?NPA支持多种协议语言，包括CSP、pi演算、lambda演算及Dolev?Yao模型等，并且能够自动推理出协议的安全性。它还提供了一些高级功能，如模型缩减和抽象，以便更快地验证大型协议。Maude?NPA是一种非常强大的验证工具，广泛应用于安全协议和分布式系统的设计和分析中。它的使用可以大幅地提高协议的安全性和可靠性，减少安全漏洞的出现。Maude?NPA分析器的前身是NRL协议分析器。该工具的优势在于特别针对方程式推理，并且支持异或和同态运算，其采用后向搜索策略，通过提出不安全状态而后从初始状态进行路径验证，是否可以从初始状态推导至该不安全状态，从而发现协议存在的漏洞问题。
3.7.5 CPN?Tools工具
由丹麦奥尔胡斯大学开发的有色Petri网（Colored Petri Net，CPN）工具软件CPN?Tools，是一种基于Petri网的建模和仿真工具，用于对分布式系统和协议进行建模、分析和验证。它支持多种Petri网模型，包括CPN、TPN（Timed Petri Nets）和HPN（Hierarchical Petri Nets）等，并提供了多种分析技术，如模型检查、符号执行和定理证明等，以便对系统的安全性进行验证。CPN?Tools的工作原理是使用Petri网模型来描述系统的行为和状态，然后使用模型检查技术对模型进行分析。它能够自动发现系统中的漏洞和攻击路径，并且能够生成证明来证明系统的安全性。该软件支持可视化建模并且提供自动生成状态空间搜索的报告，集成的SML（Standard Meta Language）辅助其对状态空间的可达路径进行搜索，也加强了对安全协议整体的评价辅助[25]。
3.7.6 AVANTSSAR工具
AVANTSSAR工具是一种基于形式化方法的安全协议分析工具，它能够自动化地分析协议的安全性，并发现其中的漏洞和攻击路径。该工具使用一种称为CASL（Common Algebraic Specification Language）的形式化语言来描述协议和安全性，并且提供了多种分析技术来验证协议的安全性。AVANTSSAR工具常用于工业协议的验证中，其期望在后端的验证中在有限的回合内找出协议存在的漏洞。该工具套本身已经使用在多个工业案例中。
3.7.7 SPIN工具
SPIN是一个基于模型检测方法的软件验证工具，由美国贝尔实验室开发[26]。它主要用于验证并发系统的正确性，包括进程间的同步和通信、共享资源的访问和分配等。SPIN支持多种模型，如有限状态机、Petri网和时序逻辑等，并提供多种验证技术，如模型检查、模拟仿真等。SPIN是一种用于检测有限状态系统是否满足PLTL公式和其他性质的工具，包括可达性、循环性等。它的建模方式是以进程为单位，将进程异步组合，并使用赋值语句、条件语句、通信语句、非确定性选择及循环语句等基本要素来描述进程。SPIN的基本方法是使用自动机表示每个进程和PLTL公式，并计算这些自动机的组合可接受的语言是否为空，以检测进程模型是否满足给定的性质从而验证协议的安全性。
4 基于定理证明的安全协议形式化分析方法
定理证明是一种安全协议形式化验证方法，它是指使用数学推理和描述，将访问控制策略模型使用严格的数学逻辑符号抽象转换成数学公式，进而采用逻辑演算来验证模型。通过综合运用模态逻辑的精准度、模型检测的全面性以及其他技术手段，从而让研究人员可以有效地消除模态逻辑的错误、缺陷以及模型检测过程中的漏洞，同时也可以把这些理论应用于一些恒定的等价关系。
4.1 Paulson归纳法
Paulson归纳法[27]旨在将协议的各种可能的“迹”进行归纳，以构建一个“迹”空间，以便更好地理解协议的安全性。然而，由于该模型空间涉及多种攻击手段，例如消息丢失、密码破解攻击及伪随机数攻击等，因此，在协议执行期间，发送者的身份很难被确认，而且可能会被中间人转发未被发现的消息。攻击者必须采取积极的行动，包括收集、伪造、加密及解密等，以便达到自身的目的，这时他们处于主动的状态。Paulson归纳法通过借助定理证明器Isabelle，通过对上述“迹”的归纳，证明安全协议的安全性，从而达到分析的目的。
4.2 Schneider秩函数
Schneider秩函数[28]是一种用于刻画密码分析攻击复杂度的函数，由密码学家SCHNEIDER S提出。它是一种基于信息熵的度量方法，用于衡量密码算法的安全性和抗攻击能力。Schneider秩函数的值越大，表示密码算法越难以被攻击。因为当输入比特串的熵较高时，攻击者需要更多的信息才能推断出密钥，从而增加了攻击破译密钥算法的复杂度，以此保障其安全性;而当输出比特串的熵较高时，表示数据接近完美的随机性，没有可利用的模式或结构，攻击者难以从密文本身分析出任何有用的信息，因此攻击者需要更多的尝试才能找到正确的密钥，从而增加了攻击的成本，保障了其安全性。
Schneider秩函数的核心思想是循环不变式技术。通过对消息空间中的每一条信息进行精确的加密，并将其转换成可重复使用的恒等不变式，从而保证该安全协议的安全性。此方法通常存在于合法主体与恶意攻击者并存的情况，合法主体与恶意攻击者会有潜在的不定期的交互行为。这种行为可能导致即使在最完美的密码学条件下，安全协议的安全性仍然无法得到有效的保障。
4.3 串空间
采用数学方法，可以把协议的运作情况抽象地表示出来，并且以一组集合和有向图的方式展示出来。通常可以把这些数据看作一种偏序关系，然后根据这些数据来确认它们之间的相互作用，并且以此来检测是否发生了攻击。这种方法就被称为串空间[29]。串空间模型被设计地十分简洁和巧妙，并且十分直观。串空间模型的优势体现为：
a. 给出了一些数据在协议操作中的清晰语义;
b. 将攻击者行为定理化，并且与所分析的协议相独立;
c. 提出多种不同的定义，以确保其准确性，并通过解释和论证来证实其可靠性;
d. 使用者可以更深入细致地了解协议正确的原因，证明十分简洁且可人工完成。
4.4 Rewriting逼近法
Rewriting逼近法[30]与传统的协议分析方法有着本质的不同，它旨在证明安全协议不受任何攻击的影响。然而，这种方法的复杂性远远超出了其他方法。Rewriting逼近法将协议结构化，将初始通信集描绘成一个树状的自动状态机，并以极大的精度接近可达集合，从而计算出消息集的超集。通过树状自动机模型，可以自动检测出逼近集合和违禁集合之间的交集，通过判断是否为空集，从而确保协议的安全性。该模型拥有无限的参与者、可扩展的交互对话以及一个强大的攻击者模型，因此可以有效地实现确保协议安全的目标。
4.5 不变式产生技术
随着归纳推理技术的发展，其在安全协议自动化验证领域中渐渐获得了十分重要的地位。研究者们最为关心的就是如何从无限消息集合推理归纳出安全协议的安全性[31，32]。通常，学者们会构造一个不受协议主体行为影响的不变式来实现这个目标。而利用这个方法也衍生出了前面所叙述的几种方案。
这些方案利用消息集合的形式来表达，它们的特征不受参与者或攻击者的行为影响，一般可以分为两类：
a. 攻击者不可知或在特定情况下可知的项;
b. 攻击者可知的项。
4.6 扩展串空间模型
扩展串空间理论（Extended String Space Theory）是一种形式化分析的方法，由Fabrege等提出，用于对安全协议进行建模、分析和验证。它是串空间理论（String Space Theory）的扩展，扩展串空间理论使用一种称为扩展串语言的形式化语言来描述协议和安全性，并提供了一种称为扩展串空间的模型来表示协议执行的过程。扩展串空间理论是为了解决串空间模型抽象密码学原语不足而提出的，为的是可以分析更加复杂的密码协议[33]。
扩展串空间模型是扩展串空间理论中的一种模型，用于表示协议的执行过程。它是串空间模型的扩展，采用了更加严格的语法和語义规则，使得协议的建模更加准确和完整。扩展串空间模型将协议执行的过程表示为一个有向图，其中每个节点表示一个协议执行状态，每条边表示协议执行过程中的转移。节点和边上都带有标签，用于表示协议执行过程中的信息和状态。例如，节点标签可以表示协议执行过程中的协议消息和密钥，边标签可以表示协议执行过程中的加密、解密操作等。扩展串空间模型能够全面而深入地表示协议执行过程中所有可能的路径，包括所有可能的攻击路径。它还能够自动化地分析协议的安全性，并生成证明来证明协议的安全性。同时，扩展串空间模型还具有很强的可扩展性和适应性，支持对多种协议安全性的分析。
4.7 事件逻辑理论
事件逻辑理论（Logic of Events Theory，LoET）是定理证明方法中常用于对分布式系统的安全性进行分析的方法。该理论由Joseph Sifakis等在20世纪80年代初提出，旨在解决并发系统的建模和验证问题。LoET使用事件来描述系统的行为和性质，可以准确地捕捉系统中不同事件之间的时间关系。LoET可以描述并发系统中不同进程之间的同步和通信，以及共享资源的访问和分配等问题。LoET支持多种逻辑，如时序逻辑、线性时序逻辑及计数时序逻辑等，可以根据不同的需求选择合适的逻辑进行归约。中国学者钟小妹等通过引入协议组合逻辑思想，对LoET理论进行了扩展[34]，扩展后的LoET理论可用于多领域得分安全协议形式化分析，例如对物理不可克隆函数（PUFs）协议的分析等。
5 基于可证明安全性的安全协议形式化分析方法
为了尝试解决传统协议存在周而复始地出现漏洞需要经常更新修补，而导致大众对于协议安全性的信心降低、成本开销大等问题，研究人员提出了安全协议的可证明方法[35]。对于安全协议分析而言，可证明安全性的方法更类似于密码学中对密码安全性的证明，即将安全性归约到已知的数学难题上，通过无法解决数学难题从而达到安全性的保证。通俗地说，就是把协议的安全性在适当的敌手模型下使用随机预言机进行安全归约，达到敌手无法攻破的目标，于是协议可以被证明是安全的。当然此方案也不是完美的，基于此类型的方案通常难以抵御物理攻击或者被证明的安全问题可能存在错误等。当然，如果选取的安全性假设本身就是容易被攻破的，那么其本身就没有意义再去假设，这也就说明在选取可证明安全性的问题时应当强调下限，也就是最弱安全应当达到的等级。
在安全协议可证明方法的应用中，会话密钥分配（SKD）协议是一个经典的应用方向。下面给出几种不同的可证明安全性理论模型。
5.1 随机预言机（RO）模型
RO模型被称为设计最成功的基于可证明安全性理论的模型方法[36]，在现代协议设计中，几乎所有的设计标准都需要提供在RO模型中可证明安全性的设计。RO模型是在实体和敌手双方都拥有同一个公开的随机预言机的情况下，证明协议实体在其中运行的正确性，然后选择适当的模拟函数取代该预言机，模拟函数的选取条件是在模拟环境和现实环境中，此函数在多项式时间内不能够被敌手区分。严格来说，以此为根据设计的协议与现实实用的协议效率、安全性相当。RO模型可以通过归约论断和形式化地定义协议的安全性来显式地得到协议的安全特征，从而归约证明协议的安全性。
5.2 BR安全模型
BR安全模型由BELLARE M和ROGAWAY P分别在1993年和1995年给出的两个可证明安全性的两方和三方的SKD协议中归纳出[37，38]，这也是首次建立了基于SKD协议的形式化的安全模型。它的基础安全理论依据是根据会话密钥与某随机数的计算不可区分性来保证安全。然而该模型归约过程十分复杂，可操作性较差，于是后来的研究者们根据该模型提出了更加简洁的BCK模型。
5.3 BCK模型
BCK模型类似于BR模型，但BCK模型的设计需要采用模块化[39]的方式，把要证明安全性的安全协议定义到理想化的模型中，同样也需要将安全性归约到计算不可区分性上。但是在归约过程中需要证明现实中的敌手强度与理想敌手是不可区分的。该模型通常用于研究认证通信问题，特别是密钥交换问题。
5.4 PSKD安全模型
BELLOVIN S M和MERRITT M提出了第1个PSKD协议[40]，该协议是基于口令来构建的，这也导致其容易受到离线字典攻击。通常基于此模型设计的协议多偏向于采用混合的方式来设计，即通信实体双方只有一方使用口令。其安全目标为任何PPT（概率多项式时间）敌手的成功破解密钥的概率上界为：
O（t/|D|）+μ（n）
其中，t为敌手会话产生的次数;μ（）为可忽略函数;D为字典且D∈{0，1}n;n为会话密钥长度。
5.5 Top?k元素求解
Top?k元素求解的方案多用于多方安全计算方面，其适用范围通常是在不泄漏隐私的情况下来求解某些特定的值或者特定的分布。在多方安全计算的情境下，越多的数据聚合使得样本越大，可以使其给出的结果越清晰。研究者们大都在尝试构建可行的Top?k求解协议，例如基于预估数值和安全比较的多方Top?k求解协议、两方和多方Top?k求解协议等。不过此类型的方案大多存在通信轮次对通信效率造成影响的问题[41]。
5.6 非交互式零知识证明技术
GOLDWASSER S等提出了零知识证明的方法[42]，这是一种特殊的密码协议，零知识证明方法运行在证明者和验证者之间，通过证明者单方面的消息发送就可以完成验证者的身份验证，该方案通常用于成员归属证明或者知识证明。零知识证明方案一般需要满足3个性质，分别是完备性、可靠性和零知识性。零知识证明方案应用十分广泛，例如数字签名、区块链及多方安全技术等。零知识证明根据难题假设来保证安全性，例如基于二次算术程序（Quadratic Arithmetic Program，QAP）/线性PCP（Linear?PCP）的系列证明，对于其安全性的保障是基于难题假设是不可证伪（non?falsifiable）的假设来保证的[43]。零知识证明的构造是一类值得研究的问题，经典的零知识证明协议有∑-协议，这类协议存在一定的提升空间，是一类十分热门的研究方向。
6 总结与展望
隨着信息安全技术的不断发展，安全协议在信息系统中的应用越来越广泛。然而，在安全协议的设计和实现过程中常存在漏洞，这些漏洞可能会被攻击者利用，导致信息泄漏、数据损坏等安全问题。因此，对安全协议进行形式化分析已成为确保其安全性的重要手段。在过去的几十年中，安全协议形式化分析方法得到了广泛研究和应用。基于模态逻辑的方法、基于模型检测的方法、基于定理证明的方法及基于可证明安全性理论的方法等都取得了一定的成果。其中，基于模型检测的方法是目前应用最广泛的一种方法，它可以自动化地检测安全协议的漏洞。同时，也有一些新的方法被提出，如基于信息流的方法、基于程序分析的方法[44～46]等，这些方法在某些场景下具有一定的优势。然而，当前安全协议形式化分析方法仍然存在问题和挑战，所以未来可以在以下3个方向来开展研究。
第一，安全协议的安全属性运用统一的框架进行分析。将安全协议的安全属性运用统一的框架进行分析是一种通用的安全协议形式化分析方法。这种方法可以将安全协议的安全属性抽象为一些基本的安全属性，然后通过定义这些安全属性之间的关系构建一个统一的框架，对安全协议进行形式化分析。例如下面由4个安全属性构成的简易框架：机密性、完整性、认证性和不可否认性。基于这个安全属性框架，可以对安全协议进行形式化分析。例如，可以通过定义机密性、完整性、认证性和不可否认性之间的关系，来描述安全协议的安全性。同时，可以使用Tamarin等工具对安全协议进行模型化，并使用模型检测技术对协议的安全性进行自动化分析。
此外，还可以将其他安全属性，如可用性、匿名性及抗重放攻击等，加入到安全属性框架中，构建一个更加全面的安全属性框架。这样可以更加准确地描述安全协议的安全性，并提高安全协议形式化分析的效率和准确性。然而将各类安全协议进行建模，归约到同一个框架下是有一定困难的，因此对于该方向的研究需要不断地去完善所建构的安全协议的安全属性模型框架。
第二，提出新的安全协议分析方法。安全协议研究的发展越来越关注新兴技术的应用，例如基于区块链的认证与密钥协商协议分析研究，通过区块链的去中心化技术可以用来研究安全协议的匿名性问题，也可以通过分析改进协议从而解决例如医療使用协议中出现的单点失效等问题[47]。又如量子协议的分析，量子协议的分析需要针对量子协议自身的特殊物理性质来考虑，也就是说量子协议是依赖量子本身可构建的数理方程和量子操作来构建的[48，49]，而对于这些特征来进行分析或者开发针对量子协议的特殊分析方法是十分有意义的。还有在传统的串空间模型下引入同态加密技术来构造高效的多方安全计算协议、基于同态密码的安全协议设计和分析、基于同态加密的多方安全计算协议等[50，51]方向的特殊协议的分析方法的开发也具有十分重要的意义。近年来，基于符号执行的自动分析方法的研究也是一个热门的方向。符号执行是一种新兴的安全协议自动分析方法，可以通过对协议的符号执行路径进行分析，发现协议中的漏洞和安全问题[52]。近年来，符号执行技术已经得到了广泛的应用，例如使用KLEE等工具对安全协议进行分析，发现协议中的漏洞和安全问题。
还有对于跨协议攻击（多协议攻击）的分析显然也是一个重要且值得研究的方向[53]。跨协议攻击是指利用不同协议之间的互操作性漏洞，将一个协议中的攻击流量伪装成另一个协议的合法流量，从而实现对目标系统的攻击。这种攻击方式可以绕过一些安全防护措施，对目标系统造成极大的威胁。在跨协议攻击中，攻击者通常会利用协议之间的相互依赖性和交互性，从而实现攻击的目的。跨协议攻击的危害非常大，因为它能够绕过单个协议的安全措施，从而实现对整个系统的攻击。然而跨协议攻击涉及的对象较多，通信信息量较大，采用自动化的分析方式常常会使状态空间出现爆炸问题，因此较难分析，但提出对于跨协议攻击的针对性的分析方法也是一个值得研究的方向。
第三，安全协议的自动化生成[54]。安全协议的自动分析和设计是近年来安全协议研究中的热门领域，其目的是通过自动化技术来提高协议的安全性和可靠性。安全协议的自动化生成依赖于安全协议的自动化分析，这就要求不断更新改进分析方法并应用于自动化分析软件中，安全协议的自动化生成可以大幅提高协议的安全性和可靠性，减少人工设计协议时可能出现的错误和漏洞。同时，它也可以加快协议的设计和开发，提高工作效率。不过，安全协议的自动化生成也存在一些挑战和限制，例如在设计模型时需要考虑协议的复杂性和实际应用场景，同时需要对生成的代码进行测试、验证等。现有的技术基本上都是针对协议的自动化分析而没有自动化生成，如果能够采用自动化的方式，将分析的漏洞等问题进行自动化改进与修正，显然也是一个十分实用的方向。
参 考 文 献
[1] 冯登国，范红.安全协议形式化分析理论与方法研究综述[J].中国科学院研究生院学报，2003，20（4）：389-406.
[2] 高尚，胡爱群，石乐，等.安全协议形式化分析研究[J].密码学报，2014，1（5）：504-512.
[3] NEEDHAM R M，SCHROEDER M D.Using encryption for authentication in large networks of computers[J].Communications of the ACM，1978，21（12）：993-999.
[4] DOLEV D，YAO A C. On the security of public key protocols[J].IEEE Transactions on Information Theory，1983，29（2）：198-208.
[5] DOLEV D， EVEN S， KARP R M. On the security of ping?pong protocols[J].Information and Control，1982，55（1?3）：57-68.
[6] NIEH B B，TAVARES S E.Modelling and analyzing cryptographic protocols using Petri nets[C]//Advances in Cryptology—AUSCRYPT′92.Berlin Heidelberg：Springer，1993：275-295.
[7] VAN OORSCHOT P.Extending cryptographic logics of belief to key agreement protocols[C]//Proceedings of the 1st ACM Conference on Computer and Communications Security.ACM，1993：232-243.
[8] DUTERTRE B，SCHNEIDER S.Using a PVS embedding of CSP to verify authentication protocols[M]//BOULTON R J.Theorem Proving in Higher Order Logics.Berlin Heidelberg：Springer，1997：121-136.
[9] BRACKIN S H. A HOL formalization of CAPSL semantics[C]//Proceedings of the 21st National Conference on Information Systems Security.Piscataway，NJ：IEEE，1998.
[10] BELLA G， PAULSON L C.Using Isabelle to prove properties of the Kerberos authentication system[J].Recent Advances in Environmentally Compatible Polymers，1997，394（2）：73-78.
[11] 趙玉兰，冀超，蒋凤仙，等.基于着色Petri网的IS?IS路由协议互操作性测试的研究[J].计算机工程与科学，2013，35（12）：90-95.
[12] 李建华，张爱新，薛质，等.网络安全协议的形式化分析与验证[M].北京：机械工业出版社，2010.
[13] BURROWS M， ABADI M， NEEDHAM R M.A logic of authentication[J].Proceedings of the Royal Society A，1989，426（1871）：1-13.
[14] GONG L，NEEDHAM R，YAHALOM R.Reasoning about belief in cryptographic protocols[C]//Proceedings of 1990 IEEE Computer Society Symposium on Research in Security and Privacy.Piscataway，NJ：IEEE，1990：234-248.
[15] ABADI M，TUTTLE M R. A semantics for a logic of authentication[C]//Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing.ACM，1991：201-216.
[16] SYVERSON P F，VAN OORSCHOT P C.A unified cryptographic protocol logic[R].Washington D. C.：Naval Research Lab，1996.
[17] 周典萃，卿斯汉，周展飞.一种分析电子商务协议的新工具[J].软件学报，2001，12（9）：1318-1328.
[18] 韩志耕，石青山，杨鹏，等.不可否认协议分析的扩展ZQZ逻辑方法[J].Journal of Cryptologic Research，2022，9（1）：60-75.
[19] CLARKE E M，GRUMBERG O，PELED D.Model Checking[M].Cambridge，MA：MIT Press，1999.
[20] MOORE R C.Semantical considerations on nonmonotonic logic[J].Artificial Intelligence，1985，25（1）：75-94.
[21] LOWE G，ROSCOE B.Using CSP to detect errors in the TMN protocol[J].IEEE Transactions on Software Engineering，1997，23（10）：659-669.
[22] 刘怡文，李伟琴.安全协议的形式化需求及验证[J].计算机工程与应用，2002（17）：125-128.
[23] 张磊.安全协议设计及验证研究[D].北京：清华大学，2004.
[24] 谷文，韩继红，袁霖.SSMCI：以攻击者为中心的安全协议验证机制[J].通信学报，2017，38（10）：175-188.
[25] 龚翔，冯涛，杜谨泽.基于CPN的安全协议形式化建模及安全分析方法[J].通信学报，2021，42（9）：240-253.
[26] 王西忠，肖美华，杨科，等.基于SPIN的MIXCOIN协议形式化分析与验证[J].广西大学学报（自然科学版），2020，45（6）：1404-1412.
[27] PAULSON L C. The inductive approach to verifying cryptographic protocols[J].Journal of Computer Security，1998，6（1）：85-128.
[28] SCHNEIDER S.Using CSP for Protocol Analysis：The Needham?Schroeder Public?key Protocol[R].England：University of London，Royal Holloway，Department of Computer Science，1996.
[29] THAYER F J，HERZOG J C，GUTTMAN J D.Strand spaces：Why is a security protocol correct？[C]//Proceedings of 1998 IEEE Symposium on Security and Privacy.Piscataway，NJ：IEEE，1998：160-171.
[30] BOICHUT Y，GENET T，JENSEN T，et al.Rewriting approximations for fast prototyping of static analyzers[M]//BAADER F.Term Rewriting and Applications.Berlin Heidelberg：Springer，2007：48-62.
[31] 潘建东，陈立前，黄达明，等.含有析取语义循环的不变式生成改进方法[J].软件学报，2016，27（7）：1741-1756.
[32] 陈志慧.基于Event?B的软件需求形式化建模技术的研究[D].成都：电子科技大学，2013.
[33] 沈海峰，薛锐，黄河燕，等.串空间理论扩展[J].软件学报，2005（10）：1784-1789.
[34] 钟小妹，肖美华，杨科，等.基于事件逻辑的PUFs认证协议形式化分析[J].华中科技大学学报（自然科学版），2024，52（2）：69-76.
[35] 冯登国.可证明安全性理论与方法研究[J].软件学报，2005（10）：1743-1756.
[36] BELLARE M， ROGAWAY P. Random oracles are practical：A paradigm for designing efficient protocols[C]//Proc of the 1st ACM Conference on Computer and Communications Security.New York：ACM Press，1993：62-67.
[37] BELLARE M，ROGAWAY P.Entity authentication and key exchange[C]//STINSON D R.Proc of the Advances in Cryptology—Crypto93.Berlin Heidelberg：Springer?Verlag，1993：232-249.
[38] BELLARE M.Provably secure session key distribution—The three party case[C]//Proc of the 27th ACM Symposium on the Theory of Computing.New York：ACM Press，1995：57-66.
[39] BELLARE M，CANETTI R，KRAWCZYK H.A modular approach to the design and analysis of authentication and key exchange protocols[C]//Proc of the 30th Annual Symposium on the Theory of Computing.New York：ACM，1998：419-428.
[40] BELLOVIN S M，MERRITT M.Encrypted key exchange：Password?Based protocols secure against dictionary attacks[C]//Proc of the IEEE Symposium on Research in Security and Privacy.Piscataway，NJ：IEEE，1992：72-84.
[41] 栾明学，张秉晟，杨国正，等.通用可重组安全的多方求解Top?k协议设计[J].密码学报，2023，10（1）：195-208.
[42] GOLDWASSER S，MICALI S，RACKOFF C.The kno?
wledge complexity of interactive proof?systems （extended abstract）[C]//Proceedings of the Seventeenth Annual ACM Symposium on Theory of Computing （STOC1985）.New York：ACM，1985：291-304.
[43] 李威翰，张宗洋，周子博，等.简洁非交互零知识证明综述[J].密码学报，2022，9（3）：379-447.
[44] 张焕国，吴福生，王后珍，等.密码协议代码执行的安全验证分析综述[J].计算机学报，2018，41（2）：288-308.
[45] 葛艺，黄文超，熊焰.基于安全协议代码的形式化辅助建模研究[J].计算机应用研究，2023，40（4）：1189-1193;1202.
[46] 田昊瑋.基于ECC的RFID安全协议研究[D].秦皇岛：燕山大学，2022.
[47] 邵晓伟，郭亚军.基于区块链的远程医疗认证协议[J]. 密码学报，2023，10（2）：397-414.
[48] 林崧，王宁，刘晓芬.一个高效的量子安全多方计算协议[J].中国科学：物理学 力学 天文学，2023，53（4）：30-40.
[49] 闫晨红，李志慧，刘璐，等.具有少量参与者的分层量子密钥分发协议[J].软件学报，2023，34（6）：2878-2891.
[50] 张爱娈.基于同态密码安全协议的研究与设计[D].北京：北京印刷学院，2022.
[51] 朱宗武，黄汝维.基于高效全同态加密的安全多方计算协议[J].计算机科学，2022，49（11）：345-350.
[52] 张协力，祝跃飞，顾纯祥，等.模型学习与符号执行结合的安全协议代码分析技术[J].网络与信息安全学报，2021，7（5）：93-104.
[53] PATERSON K G，SCARLATA M，TRUONG K T.Three lessons from threema：Analysis of a secure messenger[C]//32nd USENIX Security Symposium （USENIX Security 23）.2023：1289-1306.
[54] METERE R，ARNABOLDI L.Automating cryptographic protocol language generation from structured specifications[C]//Proceedings of the IEEE/ACM 10th International Conference on Formal Methods in Software Engineering.Piscataway，NJ：IEEE，2022：91-101.
（收稿日期：2023-03-13，修回日期：2024-04-28）
A Review of Formal Analysis Methods for Security Protocols
MIAO Xiang?hua1，2， HUANG Ming?wei1， ZHANG Shi?qi1，
ZHANG Shi?jie1， WANG Xin?yuan1
（1. Faculty of Information Engineering and Automation， Kunming University of Science and Technology;
2. Yunnan Key Laboratory of Computer Technology Applications ）
Abstract The basic concepts and classifications of security protocols were introduced and then， the formal analysis methods for security protocols were described， including methods based on modal logic and those based on model detection， theorem proving and provable security theory， of them，that based on model detection is the most widely used method. In addition， some commonly?used tools based on model detection methods were introduced in detail and both research hotspots and future development directions of formal analysis methods for security protocols were summarized.
Key words security protocol， formal analysis， modal logic， model detection， theorem proof， provable security
