形式化分析方法

《形式化分析方法》由会员分享，可在线阅读，更多相关《形式化分析方法（8页珍藏版）》请在装配图网上搜索。

1、安全协议的形式化分析方法安全协议是采用密码技术来保障通信各方之间安全交换信息的一个规则序 列。其目的是在通信各方之间提供认证或为新的会话分配会话密钥。尽管现有的 安全协议是安全专家精心设计和详细审核过的 但仍然可能存在一些不易发现的 安全缺陷 有些甚至数年后才被发现。长期以来，形式化方法被公认为分析安全 协议的有力武器。目前分析安全协议的形式化方法主要有：（1）推理构造法，该方法基于知识和信念推理的模态逻辑，如 K3P 逻辑等， 但 K3P 逻辑只能分析协议的认证性质而不能分析协议的保密性质；（2）攻击构造法，该方法从协议的初始状态开始，对合法主体和一个攻击者 所有可能的执行路径进行穷尽搜索，

2、以期找到协议可能存在的错误。这种方法主 要有基于模型检测技术的模型检测器 QRS（ 验证语言 、代数简化理论模型以及 特定专家系统（如特殊目的NRL分析器和Interrogator）,但这种方法无法解决状 态空间爆炸问题；（3）证明构造法，该方法集成了以上两类方法的思想及多种技术，主要有Bolignano 证明方法和 Paulson 方法等。以上形式化分析方法的主要缺点是无法解 决状态空间爆炸问题在很大程度上被限制在规模很小的协议分析中 这显然不适 应网络通信规模日益增大等发展的需要。安全协议是建造网络安全环境的重要基石，是保证网络安全的核心技术。设 计和证明安全协议自身的正确性和安全性，成为

3、网络安全的基础。形式化分析方 法已被证明是用于分析、设计和验证安全协议的重要方法，对安全协议的形式化 分析、设计和验证已经成为当今形式化分析研究领域的一个热点问题。虽然人们使用形式化分析方法已成功发现了许多现存安全协议存在的缺陷 和针对她们的攻击，但是这些分析方法还存在许多缺陷。有些形式化分析方法自 身不太完善，存在一定的局限性，不能分析和验证某些类型安全协议的安全性； 有些只能分析安全协议的不安全性，不能给出协议安全性的精确证明。在总结安全协议现存各种缺陷的基础上，根据缺陷产生各种原因将缺陷分为 过小保护缺陷、消息可重放缺陷、消息不可达性缺陷、并行会话缺陷和其他类型 缺陷等五类。同时把针对安

4、全协议的各种攻击方法可分为：重放消息型攻击、猜 测口令型攻击、分析密码型攻击、并行会话型攻击、格式缺陷型攻击和身份绑定 型攻击等六类。其中，Burrows, Abadi和Needham提出的BAN逻辑开创了用逻辑化方法 分析安全协议安全性的新纪元。由于该方法是对现实协议分析方法的抽象，逻辑 处理的符号集是对现实具体协议的抽象；其初始假设、断言集合等均是从现实世 界中抽象出来的要素。因此，其狭窄的符号集合定义也就决定了该方法存在不能 分析某些类型协议安全性的缺陷，如：不能发现由于时间同步问题而导致的协议 缺陷。另外使用BAN逻辑对安全协议分析时，很多初始假设是不合理的，如消 息不可伪造假设就非常

5、不合理，这些假设的不合理，妨碍了该分析方法的正确应 用。 BAN 逻辑还存在非严谨的理想化步骤缺陷；语义不清晰缺陷；非严密的环 境模型缺陷和无法有效预测对协议存在的攻击等缺陷。本文讨论基于知识与信念推理的模态逻辑方法,对 BAN 逻辑及其重要的增 强与扩展GNY逻辑、AT逻辑、VO逻辑进行详尽的研究，比较它们的 特点和优缺点讨论了 BAN类逻辑中的佼佼者SVO逻辑，并研究安全协议 的逻辑分析方法和串空间模型相结合的问题.然后讨论安全协议的设计原则.设 计时必须充分考虑Dolev-Yao攻击者模型,不低估攻击者的能力.安全协议必须能 够抵抗常见攻击，特别是重放攻击然后，通过串空间模型的实例，说明

6、形式化方法 如何指导安全协议的正确设计.模态逻辑方法是分析安全协议的最为重要的方法之一，它们分析并验证了许 多重要的安全协议 ， 其中包括分析经典的 Needham-Schroeder 私钥协议、 Lowe-Needham-Schroeder 公钥协议、 Nessett 协议等.模态逻辑分析方法与分布式系统中分析知识和信念演化的逻辑相似.这些逻 辑系统由一些命题和推理规则组成，命题表示主体对消息的知识或信念，应用推 理规则可以从已知的知识和信念推导出新的知识和信念 . Syverson 在文献中阐 述了在安全协议的分析中，知识、信念和语义之间关系的相互作用。在这类方法 中，最著名的是BAN类逻

7、辑。其他相近的工作还包括：Bieber逻辑CKT5、 Syverson 逻辑KPL、Rangan 逻辑、Moser 逻辑以及 Yahalom,Klein,Beth 的YHK逻辑等.1999年Kindred在他的博士论文中提出的密码协议的生成理论一 RV 逻辑是这方面的又一个新成果。Syverson 逻辑将攻击者具有的知识分为两类:一类是攻击者收到一条消息后 所具有的知识(在看见一个比特串的含义下);另一类是攻击者可以识别消息时所 具有的知识.然后,Syverson逻辑可以对此进行推理.类似于Syverson逻 辑,Bieber逻辑也区别看见一条消息和理解一条消息，并能对安全协议中知识的 演化进

8、行推理.Rangan逻辑的特点是研究可信(trust),对由“可信”至“信念”(belief) 的演化过程进行推理.YKB逻辑则从另一个角度讨论“可信” 在上述逻辑中，知 识和信念的演化都是单调的,亦即知识和信念的演化只增不减 Moser逻辑是惟 一的例外,它的信念演化是非单调的.例如,在推理过程中如果知道一个密钥已被 泄露, 则其信念集合可以减小。BAN 逻辑之所以著名,不仅由于它开创了安全协议形式化分析的先河,是一 项开拓性的工作 , 而且由于它提供的形式化分析方法特别直观与简单 . 有人 说,BAN逻辑成功的秘诀是“简单加实用”，这话有一定的道理。BAN逻辑虽然简 单，但仍然可以成功地揭

9、示安全协议中的设计缺陷例如，通过BAN逻辑分析，发 现了 CCITT X.509标准推荐草案中的安全漏洞.BAN 逻辑的直观性与简单性主要表现在以下几个方面:第 1，BAN 逻辑不区 分看见一条消息和理解一条消息；第 2，BAN 逻辑的信念演化过程是单调递增 的；第3,BAN逻辑不讨论“可信”；第4, BAN逻辑不讨论知识；第5, BAN逻 辑假设参加协议的主体是诚实的 ， 他们都忠实地根据协议的规则执行协议 ; 第 6,BAN逻辑假设加密系统是完善的(perfect)等等。但是,BAN逻辑不追求完美而追求简洁、实用的设计思想，也为BAN逻辑分 析方法带来了局限性,使 BAN 方法的抽象级别过

10、高,分析范围过窄.例如,由于 BAN逻辑不能对知识进行推理，因此,BAN逻辑只能分析协议的认证性质,而不能 分析协议的保密性质.然而在现实中,通常的密钥分配协议要同时实现保密性和 认证性两个重要目标.BAN逻辑是一种多类型模态逻辑(many-sorted modal logic),它包含以下3 种处理对象:主体、密钥和公式.其中的公式，也称作语句或命题.BAN逻辑仅包含 合取这一命题联接词，用逗号表示.BAN逻辑共有19条推理规则.在推理规则中， 卜是元语言符号HC表示可以由前提集推导出结论C.应用BAN逻辑形 式化分析安全协议的步骤是:1. 对安全协议进行理想化,亦即,将协议消息转换为 BA

11、N 逻辑所能理解的 公式；2. 对安全协议进行解释 ,亦即,将形如 的消息转换成形如 Q 的逻辑语言. 解释过程中遵循以下规则:X Q P : f X received(1) 若命题X在消息前成立，则在其后,X和都成立；Y Q P : f Y Qreceived(2) 若根据推理规则可以由命题 X 推导出命题 Y， 则命题 X 成立时， 命题 Y 亦成立；3. 应用 BAN 逻辑语言对系统的初始状态进行描述， 给出初始化假设集；4. 应用 BAN 推理规则对协议进行形式化分析， 得出相应的结论。关于BAN逻辑的其他内容，例如BAN逻辑构件的语法和语义、BAN逻辑 的推理规则、 BAN 逻辑分析

12、认证协议的实例等，读者可参见其他文献。1990 年， Nessett 引入一个简单的例子 ， 试图说明 BAN 逻辑本身存在一个重 要的安全问题：在消息1中,A用其秘密密钥加密A与B之间的会话密钥和临时值，然后发送 给B.B用A的公开密钥解密出，然后用加密临时值 后发送给A,显然，不是A 和B之间通信的“良好”的会话密钥，因为任何主体都可以从消息1中获得会话 密钥 . 但是， 用 BAN 逻辑分析 Nessett 协议， 却得出 是良好的会话密钥的结论.据此,Nessett认为，BAN逻辑本身存在一个重要缺陷，该缺陷源于BAN逻辑 的分析范围.因为 BAN 逻辑只考虑分配密钥和身份认证的问题，

13、但未考虑哪个主 体不应当获得密钥，亦即，未考虑机密性的问题.BAN对Nessett的批评答复如下： 在BAN逻辑的文献中，已经清楚地说明,BAN逻辑只讨论诚实主体的认证问题，并 不关心检测非授权地暴露秘密的问题.在Nessett协议中,A在消息1中公开了， 故Nessett的假定：不符合BAN的基本假定.因此,Nessett从不合理的初 始假定推导出了不合理的结论，而 BAN 逻辑本身并不能防止建立不合理的初始 假定集合.虽然我们不能通过 Nessett 协议说明 BAN 逻辑本身存在着缺陷， 但 Nessett 的 反例启示我们，BAN逻辑的推理分析依赖于我们所作的基本假设和初始假设如 果非

14、形式化的初始假设错了,则通过形式化分析之后常常得出错误的结论。在对 BAN逻辑进行增强和扩充的过程中,GNY逻辑、AT逻辑、VO逻辑和SVO逻辑最 为著名，习惯上统称它们为BAN类逻辑其中，SVO逻辑是在总结BAN逻辑、GNY 逻辑、 AT 逻辑和 VO 逻辑的基础上发展起来的, 我们将在下一节加以讨论.(1) GNY 逻辑BAN逻辑问世以后，第一个对它进行增强的是GNY逻辑.GNY的逻辑公设有 44个之多此外，在GNY逻辑中，如果C是逻辑公设,则对任何主体P,也是逻 辑公设.具体地说，在GNY逻辑中，有接收法则6个(T1T6);拥有法则8个 (P1P8);新鲜性法则11个(F1F11 );识

15、别法则6个(R1R6);消息解释法则7 个(1117);管辖法则3个J1J3); “不在这里产生”法则3个.GNY逻辑对 BAN 逻辑的重要改进与推广有以下几个方面:(1)通过新增加的逻辑构件与法则， 推广了 BAN逻辑的应用范围.例如,GNY逻辑不局限于分析认证协议，还可以分 析某些应用单向函数的密码协议;(2)增加了“拥有密钥”的表达式， 增强了 GNY 逻辑本身的表达能力因此,A相信C拥有A和B之间的共享密钥可以表示 为 ， 并能进行相应的推理 ;(3) 在 GNY 逻辑中， 区分一个主体收到的消息和一 个主体可用的消息;(4) 在 GNY 逻辑中， 进一步区分一个主体自己生成的消息和

16、其他消息；(5) 在 GNY 逻辑分析中， 在理想化协议中保留明文. 而在 BAN 逻辑 分析中， 明文在认证过程中不起作用。AB K C A has believes类似于 BAN 逻辑， 为了简化分析过程， 在 GNY 逻辑中不包含否定形式 ， 也 没有粒度更细的时序概念此外,GNY逻辑的语义也与BAN逻辑相似。尽管 GNY 逻辑具有上述特点， 但它本身过于复杂. 在它的 44 个法则中， 有 许多法则使 GNY 逻辑本身不必要地复杂 因此许多学者认为 ， 应用 GNY 逻辑 分析安全协议在实际上是行不通的.尽管如此， 我们认为， GNY 逻辑在历史的长河中发挥了它应有的作用 ， 使我 们

17、对认证协议及BAN逻辑分析有了更加深刻的认识.在 BAN 逻辑之后不久出现的 AT 逻辑为 BAN 逻辑构造了一个简单的语义 模型，是对BAN逻辑的一种重要改进.类似于GNY逻辑,AT逻辑对BAN逻辑 的本质与局限性进行了深入的分析,并获得了相近的结论但是,GNY得到的是一 个更加复杂的逻辑,其原因是 GNY 逻辑和 BAN 逻辑一样,缺乏一个适当的语 义基础.AT逻辑比BAN逻辑更接近传统的模态逻辑：它包含一个详细的计算模 型,增加了模型论语义,表达能力更强,因而将 BAN 逻辑向前推进了一大步.AT 逻辑对 BAN 逻辑的改进还包括：(1)对 BAN 逻辑中的定义和推理法 则进行整理,抛弃

18、其中语义和实现细节的混和部分；(2)对某些逻辑构件引入更直 接的定义,免除对诚实性进行隐含假设；(3)简化了推理法则,所有的概念都独立 定义,不与其他概念相混淆;(4)整个逻辑只有两条基本推理规则 ,亦即： (a) MP 规则(modus ponens):由 0 和 0 屮 可以推导出屮；(b) Nec 规则(necessi tati on): 由0可以推导出P believes 0。例如,BAN逻辑有P said X的逻辑构件，说明P发送过X,但没有P最近 发送 X 的构件.在 AT 逻辑中引入了新的逻辑构件 P says X, 表示 P 最近发 送X,因此更加接近新鲜性的本质.AT逻辑的公

19、理A20:，说明若X是新鲜的且 P 发送过 X, 则 P 最近发送了 X. 这条公理更加深刻地描述了新鲜性的本质。在AT逻辑中有一条比BAN逻辑更加直接的管辖公理A15: 000-A says controls P P ,说明若P管辖0且P最近说过0，则0是真实的.这个更自然 的管辖内涵,使 AT 逻辑不必进行隐含的诚实性假设。VO 逻辑的贡献是扩展了 BAN 逻辑的应用范围 .Diffie-Hellman 协议是许 多近代密钥分配协议的基础,VO逻辑的设计目标就是增加分析Diffie-Hellman 协议的能力，进而可以分析IETF标准因特网密钥交换协议IKE和SSL等。VO 逻辑的另一个重

20、要特点是,细化了认证协议的认证目标,给出了 6 种不 同形式的认证目标。SVO逻辑吸取了 BAN逻辑、GNY逻辑、AT逻辑和V0逻辑的优点，将 它们集成在一个逻辑系统中 . 在形式化语义方面 ,SVO 逻辑对一些概念重新进行 定义(有别于 AT 逻辑),从而取消了 AT 逻辑系统中的一些限制。 SVO 逻辑所用 的记号与 BAN 类逻辑相似, 其中特有的 12 个符号。与AT逻辑相似，SVO逻辑也将语言划分为集合T上的消息语言MT和公 式语言 FT. 其中 T 为原子术语集, 由主体、共享密钥、公开密钥、私有密钥及一 些常量符号构成. 应用 SVO 逻辑对安全协议进行形式化分析可以分为以下 3

21、 个步骤:(1) 给出协议的初始化假设集Q ,即用SVO逻辑语言表示出各主体的初始 信念、接收到的消息、对所收到消息的理解和解释；(2) 给出协议可能或应该达到的目标集 , 即用 SVO 逻辑语言表示的一个 公式集；(3) 在SVO逻辑中证明结论Q是否成立.若成立，则说明该协议达到了预期 的设计目标, 协议的设计是成功的. 因此, 正确理解安全协议中消息的含义和协 议的设计目标， 是应用 SVO 逻辑进行协议分析的基础。SVO 逻辑是 BAN 类逻辑中的佼佼者. 它的理论基础更加坚实， 在实用上保 持了 BAN 逻辑简单易用的特点， 因此被广泛接受. 应用 SVO 逻辑不仅成功地 分析了各种认

22、证协议， 也成功地分析了在电子商务中应用日益广泛的非否认协议 在设计协议时， 如何保证安全协议能够满足保密性、无冗余、认证身份等设计目 标呢?经过总结， 我们提出了以下安全协议的设计原则:(1) 设计目标明确 ， 无二义性；(2) 最好应用描述协议的形式语言， 对安全协议本身进行形式化描述；(3) 通过形式化分析方法证明安全协议实现了设计目标；(4) 安全性与具体采用的密码算法无关；(5) 保证临时值和会话密钥等重要消息的新鲜性， 防止重放攻击；(6) 尽量采用异步认证方式， 避免采用同步时钟(时戳)的认证方式；(7) 具有抵抗常见攻击， 特别是防止重放攻击的能力；(8) 进行运行环境的风险分

23、析， 作尽可能少的初始安全假设；(9) 实用性强， 可用于各种网络的不同协议层；(10) 尽可能减少密码运算， 降低成本， 扩大应用范围。其中，第 条十分重要oDolev和Yao于1983年提出了 Dolev-Yao攻击者 模型. 它是对攻击者的知识和能力进行概括的最早的模型 ， 此后关于安全协议的 形式化分析或多或少都受到他们的工作的影响 . “永远不低估攻击者的能力”， 这是设计安全协议时应当时刻牢记的一条重要原则。形式化分析方法， 包括简单直接的 BAN 类逻辑分析方法， 不但是分析安全协 议的重要工具， 也是指导安全协议设计的理论基础. 我们预期， 今后这一领域的 热点研究方向包括:(1)减少对协议所作的基本假设， 例如， 加密体制的“完善”(perfect)假设、自由加密(free encryption)假设等，使理论研究尽量接近实际.扩 大协议的分析范围.例如,分析安全电子商务协议;分析协议的公平性等.(3)增加 分析“协议组合”的能力， 这是目前的研究热点与难点之一.(4)综合不同分析方 法的特点，例如,CSP模型、串空间模型、模型校验器(model checker)方法、线性 逻辑方法等的相互比较与结合的研究 . (5)安全协议的自动生成与校验研究. (6) 参加协议的主体数目可以无限增加时的研究等等。