形式化分析方法.doc

《形式化分析方法.doc》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

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

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

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

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

5、不合理，这些假设的不合理，妨碍了该分析方法的正确应用。BAN逻辑还存在非严谨的理想化步骤缺陷；语义不淸晰缺陷；非严密的坏境模型缺陷和无法有效预测对协议存在的攻击等缺陷。模态逻辑方法是分析安全协议的最为重要的方法么一,它们分析并验证了许多重要的安全协议，其屮包括分析经典的Needham・Schroeder私钥协议、Lowe-Needham-Schroeder公钥协议、Nessett协议等.模态逻辑分析方法与分布式系统屮分析知识和信念演化的逻辑相似.这些逻辑系统由一些命题和推理规则组成，命题表示主体对消息的知识或信念，应用推理规则可以从己知的知识和信念推导出新的知识和信念.Syve

6、rson在文献屮阐述了在安全协议的分析屮,知识、信念和语义Z间关系的相互作用。在这类方法屮，最著名的是BAN类逻辑。其他相近的工作还包括:Bieber逻辑KT5>Syverson逻辑KPL>Rangan逻辑、Moser逻辑以及Yahalom,Klein,Beth的YHK逻辑等.1999年,Kindred在他的博士论文屮提出的密码协议的生成理论——RV逻辑是这方面的又一个新成果。Syverson逻辑将攻击者具有的知识分为两类:一类是攻击者收到一条消息后所具有的知识(在看见一个比特串的含义卜J;另一类是攻击者可以识别消息时所具有的知识.然后,Syverson逻辑可以对此进行推理.类

7、似于Syverson逻辑,Bieber逻辑也区别看见一条消息和理解一条消息，并能对安全协议屮知识的演化进行推理.Rangan逻辑的特点是研究可信(trust),对由“可信”到“信念"(belief)的演化过程进行推理.YKB逻辑则从另一个角度讨论“可信，在上述逻辑屮，知识和信念的演化都是单调的，亦即知识和信念的演化只增不减.Moser逻辑是惟一的例外，它的信念演化是非单调的.例如，在推理过程屮如果知道一个密钥已被汕露,则其信念集合可以减小。BAN逻辑Z所以著名，不仅由于它开创了安全协议形式化