安全协议的形式化分析方法
安全协议是采用密码技术来保障通信各方之间安全交换信息的一个规则序列。其目的是在通信各方之间提供认证或为新的会话分配会话密钥。尽管现有的安全协议是安全专家精心设计和详细审核过的 但仍然可能存在一些不易发现的安全缺陷 有些甚至数年后才被发现。长期以来，形式化方法被公认为分析安全协议的有力武器。
目前分析安全协议的形式化方法主要有：
（1）推理构造法，该方法基于知识和信念推理的模态逻辑，如K3P逻辑等，但K3P逻辑只能分析协议的认证性质而不能分析协议的保密性质；
（2）攻击构造法，该方法从协议的初始状态开始，对合法主体和一个攻击者所有可能的执行路径进行穷尽搜索，以期到协议可能存在的错误。这种方法主要有基于模型检测技术的模型检测器QRS( 验证语言 、代数简化理论模型以及特定专家系统（如特殊目的NRL分析器和Interrogator），但这种方法无法解决状态空间爆炸问题；
（3）证明构造法，该方法集成了以上两类方法的思想及多种技术，主要有Bolignano证明方法
和Paulson方法等。以上形式化分析方法的主要缺点是无法解决状态空间爆炸问题在很大程度上被限制在规模很小的协议分析中 这显然不适应网络通信规模日益增大等发展的需要。
安全协议是建造网络安全环境的重要基石，是保证网络安全的核心技术。设计和证明安全协议自身的正确性和安全性，成为网络安全的基础。形式化分析方法已被证明是用于分析、设计和验证安全协议的重要方法，对安全协议的形式化分析、设计和验证已经成为当今形式化分析研究领域的一个热点问题。
虽然人们使用形式化分析方法已成功发现了许多现存安全协议存在的缺陷和针对她们的攻击，但是这些分析方法还存在许多缺陷。有些形式化分析方法自身不太完善，存在一定的局限性，不能分析和验证某些类型安全协议的安全性；有些只能分析安全协议的不安全性，不能给出协议安全性的精确证明。
在总结安全协议现存各种缺陷的基础上，根据缺陷产生各种原因将缺陷分为：过小保护缺陷、消息可重放缺陷、消息不可达性缺陷、并行会话缺陷和其他类型缺陷等五类。同时把针对安全协议的各种攻击方法可分为：重放消息型攻击、猜测口令型攻击、分析密码型攻击、并行会话型攻击、格式缺陷型攻击和身份绑定型攻击等六类。
其中，Burrows，Abadi 和 Needham 提出的 BAN 逻辑开创了用逻辑化方法分析安全协议安全性的新纪元。由于该方法是对现实协议分析方法的抽象，逻辑处理的符号集是对现实具体协议的抽象；其初始假设、断言集合等均是从现实世界中抽象出来的要素。因此，其狭窄的符号集合定义也就决定了该方法存在不能分析某些类型协议安全性的缺陷，如：不能发现由于时间同步问题而导致的协议缺陷。另外使用BAN逻辑对安全协议分析时，很多初始假设是不合理的，如消息不可伪设就非常不合理，这些假设的不合理，妨碍了该分析方法的正确应用。BAN逻辑还存在非严谨的理想化步骤缺陷；语义不清晰缺陷；非严密的环境模型缺陷和无法有效预测对协议存在的攻击等缺陷。
本文讨论基于知识与信念推理的模态逻辑方法,对 BAN 逻辑及其重要的增强与扩展——GNY 逻辑、AT 逻辑、VO 逻辑——进行详尽的研究,比较它们的特点和优缺点.讨论了BAN 类逻辑中的佼佼者——SVO逻辑,并研究安全协议的逻辑分析方法和串空间模型相结合的问题.然后讨论安全协议的设计原则.设计时必须充分考虑 Dolev-Yao攻击者模型,不低估攻击者的能力.安全协议必须能够抵抗常见攻击,特别是重放攻击然后,通过串空间模型的实例,说明形式化方法如何指导安全协议的正确设计.
模态逻辑方法是分析安全协议的最为重要的方法之一,它们分析并验证了许多重要的安全协议 ,其中包括分析经典的 Needham-Schroeder 私钥协议、Lowe-Needham-Schroeder 公钥协议、Nessett 协议等.
模态逻辑分析方法与分布式系统中分析知识和信念演化的逻辑相似.这些逻辑系统由一些命题和推理规则组成,命题表示主体对消息的知识或信念,应用推理规则可以从已知的知识和信念推导出新的知识和信念.Syverson 在文献中阐述了在安全协议的分析中,知识、信念和语义之间关系的相互作用。在这类方法中,最著名的是 BAN 类逻辑。其他相近的工作还包括:Bieber 逻辑——CKT5、Syverson逻辑——KPL、Rangan 逻辑、Moser 逻辑以及 Yahalom,Klein,Beth 的 YHK 逻辑等.1999 年,Kindred在他的博士论文中提出的密码协议的生成理论——RV 逻辑是这方面的又一个新成果。
Syverson 逻辑将攻击者具有的知识分为两类:一类是攻击者收到一条消息后所具有的知识(在看见一个比特串的含义下);另一类是攻击者可以识别消息时所具有的知识.然后,Syverson 逻辑可以对此进行推理.类似于Syverson 逻辑,Bieber 逻辑也区别看见一条消息和理解一条消息,并能对安全协议中知识的演化进行推理.Rangan 逻辑的特点是研究可信(trust),对由“可信”
到“信念”(belief)的演化过程进行推理.YKB 逻辑则从另一个角度讨论“可信”.在上述逻辑中,知识和信念的演化都是单调的,亦即知识和信念的演化只增不减.Moser 逻辑是惟一的例外,它的信念演化是非单调的.例如,在推理过程中如果知道一个密钥已被泄露,则其信念集合可以减小。
BAN逻辑之所以著名,不仅由于它开创了安全协议形式化分析的先河,是一项开拓性的工作,而且由于它提供的形式化分析方法特别直观与简单.有人说,BAN 逻辑成功的秘诀是“简单加实用”,这话有一定的道理。BAN逻辑虽然简单,但仍然可以成功地揭示安全协议中的设计缺陷.例如,通过 BAN 逻辑分析,发现了 CCITT X.509标准推荐草案中的安全漏洞.
BAN 逻辑的直观性与简单性主要表现在以下几个方面:第 1,BAN 逻辑不区分看见一条消息和理解一条消息；第 2,BAN 逻辑的信念演化过程是单调递增的；第 3,BAN 逻辑不讨论“可信”;第4,BAN 逻辑不讨论知识；第5,BAN 逻辑假设参加协议的主体是诚实的,他们都忠实地根据协议的规则执行协议;第 6,BAN 逻辑假设加密系统是完善的(perfect)等等。
但是,BAN 逻辑不追求完美而追求简洁、实用的设计思想,也为 BAN 逻辑分析方法带来了局限性,使 BAN方法的抽象级别过高,分析范围过窄.例如,由于BAN逻辑不能对知识进行推理,因
此,BAN逻辑只能分析协议的认证性质,而不能分析协议的保密性质.然而在现实中,通常的密钥分配协议要同时实现保密性和认证性两个重要目标.
BAN 逻辑是一种多类型模态逻辑(many-sorted modal  logic),它包含以下 3 种处理对象:主体、密钥和公式.其中的公式,也称作语句或命题.BAN逻辑仅包含合取这一命题联接词,用逗号表示.BAN逻辑共有19条推理规则.在推理规则中,⊦是元语言符号. Γ ⊦C 表示可以由前提集Γ 推导出结论 C.应用 BAN 逻辑形式化分析安全协议的步骤是:
1.  对安全协议进行理想化,亦即,将协议消息转换为BAN 逻辑所能理解的公式；
2.  对安全协议进行解释,亦即,将形如 的消息转换成形如Q 的逻辑语言.解释过程中遵循以下规则:
X Q P : → X received
(1)  若命题 X 在消息 前成立,则在其后,X 和 都成立;  Y Q P : → Y Qreceived
(2)  若根据推理规则可以由命题 X 推导出命题 Y,则命题 X 成立时,命题 Y 亦成立；
3.  应用 BAN 逻辑语言对系统的初始状态进行描述,给出初始化假设集；
4.  应用 BAN 推理规则对协议进行形式化分析,得出相应的结论。
关于 BAN 逻辑的其他内容,例如 BAN 逻辑构件的语法和语义、BAN 逻辑的推理规则、BAN 逻辑分析认证协议的实例等,读者可参见其他文献。
1990 年,Nessett引入一个简单的例子,试图说明 BAN 逻辑本身存在一个重要的安全问题：
在消息1中,A用其秘密密钥加密A与B之间的会话密钥和临时值 ,然后发送给B.B用A的公开密钥解密出 ,然后用 加密临时值 后发送给A,显然, 不是A和B之间通信的“良好”的会话密钥,因为任何主体都可以从消息 1 中获得会话密钥 .但是,用 BAN 逻辑分析 Nessett 协议,却得出 是良好的会话密钥的结论.
据此,Nessett 认为,BAN 逻辑本身存在一个重要缺陷,该缺陷源于 BAN 逻辑的分析范围.因为 BAN 逻辑只考虑分配密钥和身份认证的问题,但未考虑哪个主体不应当获得密钥,亦即,未考虑机密性的问题. BAN对Nessett的批评答复如下:在BAN逻辑的文献中,已经清楚地说明,BAN逻辑只讨论诚实主体的认证问题,并不关心检测非授权地暴露秘密的问题.在 Nessett 协议中,A
在消息 1 中公开了 ,故 Nessett 的假定: 不符合 BAN 的基本假定.因此,Nessett 从不合理的初始假定推导出了不合理的结论,而BAN 逻辑本身并不能防止建立不合理的初始假定集合.
虽然我们不能通过Nessett协议说明BAN逻辑本身存在着缺陷,但Nessett的反例启示我们,BAN逻辑的推理分析依赖于我们所作的基本假设和初始假设.如果非形式化的初始假设错了,则通过形式化分析之后常常得出错误的结论。在对 BAN 逻辑进行增强和扩充的过程中,GNY 逻辑、AT 逻辑、VO 逻辑和 SVO 逻辑最为著名,习惯上统称它们为 BAN 类逻辑.其中,SVO 逻辑是在总结 BAN 逻辑、GNY 逻辑、AT 逻辑和 VO 逻辑的基础上发展起来的,我们将在下一节加以讨论.
(1) GNY 逻辑
BAN 逻辑问世以后,第一个对它进行增强的是 GNY 逻辑.GNY 的逻辑公设有 44 个之多.此外,在 GNY 逻辑中,如果C 是逻辑公设,则对任何主体 P ,也是逻辑公设. 具体地说,在 GNY 逻辑中,有接收法则 6 个(T1~T6);拥有法则 8 个(P1~P8);新鲜性法则 11 个(F1~F11);识别法则 6 个(R1~R6);消息解释法则 7 个(I1~I7);管辖法则 3 个(J1~J3);“不在这里产生”法则 3 个. GNY 逻辑对 BAN 逻辑的重要改进与推广有以下几个方面:(1)通过新增加的逻辑构件与法则,推广了B
正则化是结构风险最小化策略的实现AN 逻辑的应用范围.例如,GNY 逻辑不局限于分析认证协议,还可以分析某些应用单向函数的密码协议;(2)增加了“拥有密钥”的表达式,增强了 GNY 逻辑本身的表达能力.因此,A 相信 C 拥有 A 和 B 之间的共享密钥可以表示为 ,并能进行相应的推理;(3)在 GNY 逻辑中,区分一个主体收到的消息和一个主体可用的消息;(4)在 GNY 逻辑中,进一步区分一个主体自己生成的消息和其他消息；(5)在 GNY 逻辑分析中,在理想化协议中保留明文.而在 BAN 逻辑分析中,明文在认证过程中不起作用。
AB K C A has believes
类似于 BAN 逻辑,为了简化分析过程,在 GNY 逻辑中不包含否定形式,也没有粒度更细的时序概念.此外,GNY 逻辑的语义也与 BAN 逻辑相似。

版权声明：本站内容均来自互联网，仅供演示用，请勿用于商业和其他非法用途。如果侵犯了您的权益请与我们联系QQ:729038198，我们将在24小时内删除。