论文部分内容阅读
随着计算机网络通信的迅猛发展,安全协议的重要性越来越得到重视。安全协议负责密钥分发和身份认证,一旦其自身出现漏洞,那么将会对通信的安全造成威胁。基于这种迫在眉睫的需求,本文分别用基于BAN逻辑和基于符号化模型检测的方法对安全协议进行形式化分析。本文的主要工作有：(1)使用BAN逻辑对YAHALOM协议进行协议理想化以及关于密钥Kas、 Kab、Kbs的有效性、服务器S的权威性、随机数Na和Nb的新鲜性等初始状态假设以及在BAN逻辑规定的六条规则的基础上进行推理证明,来验证协议能否达到文中提出的协议一级目标和二级目标。同时对逻辑推理结果进行分析,如果协议满足部分安全目标那就说明协议存在安全漏洞,那么我们就在分析结果的基础上对YAHALOM协议的改进提出建设性的意见；(2)SMV是安全协议形式化进行自动化验证的工具。文中在阐述符号化模型检测软件SMV的语法语义并在小系统模型的基础上,对YAHALOM协议中的三个通信实体建立有限状态机模型,同时在分析协议消息的基础上创建初始者A、响应者B和服务器S三个诚实通信实体的状态转换图,当然我们也会给出入侵者I冒充初始者、响应者或者是服务器的状态转换图。接着根据创建的状态转换图给出三个诚实通信实体的状态转换的自然语言描述,并在此基础上对YAHALOM协议进行详细的建模。然后根据SMV语法语义给出协议要验证的关于认证性、保密性、安全性和完整性等性质。最后用SMV执行文中建立的模型,以此来验证YAHALOM协议是否符合文中提出的R1～R6等六个CTL属性。同时系统给出验证结果true或者false,若为false则系统会自动给出反例,那么我们就可以在分析系统给出的反例的基础上对YAHALOM协议的改进提出可行性的建议；(3)从时间复杂度、空间复杂度等角度对文中的两种验证方法进行比较,以对安全协议的形式化验证做更深入的了解。