关键词：
安全协议
TLS
形式化方法
状态机学习
摘要：
协议的安全性分析一直是网络空间安全领域的重点研究问题。近几年来,云计算、智能终端、5G等新兴技术发展极为迅速,以移动互联网、物联网、卫星互联网等为代表的新一代网络方兴未艾。在这些网络中,协议作为构建网络的必要组成部分,是保障整个系统正常工作的基础,国内外研究者通过设计安全协议等方式来保证网络安全。安全协议就是通过密码学的方法为网络节点提供安全保证的分布式算法,由规范层（Specification）、实现层（Implemention）以及配置层（Configuration）三个层次构成。它是当前信息网络安全的基础之一,旨在保护公共网络上的通信。安全协议对错误十分敏感,一旦存在安全缺陷,即安全协议没有满足它声明的安全性,将会对信息安全产生极大威胁,可能会造成重大的经济、社会甚至军事影响。形式化方法是基于严格数学基础,在计算机领域对目标系统进行规约、开发和验证的技术。形式化方法在分析高安全性需求的关键系统时,具有不可比拟的重要性,尤其在安全协议分析领域中更加突出。安全协议的漏洞主要出现在规范层和实现层中。规范层通常采用形式化方法进行安全性分析,实现层则多使用测试方法。目前的安全性分析方法仍然存在不足。在规范层,传统形式化方法中的敌手模型不足以表征敌手的攻击能力,无法准确分析协议规范的安全性;在实现层,传统测试方法多聚焦在挖掘内存溢出等实现漏洞上,很难找到协议实现的逻辑漏洞。本文深入研究基于形式化方法的协议安全性分析技术,解决了传统方法在协议的规范层和实现层安全性分析中存在的问题与不足。论文的主要研究工作及创新点如下:（1）提出了基于操作语义的拓展敌手模型。首先使用操作语义拓展了敌手攻击规则,丰富了对敌手攻击能力的描述,并根据拓展规则建立了敌手长期密钥攻击模型以及敌手短期数据攻击模型,相较传统敌手模型对敌手攻击的表达能力更加完整。为了验证该拓展敌手模型的有效性,本文通过Scyther[1]对HMQV协议进行自动化验证,结果表明,所提拓展模型能够获得HMQV协议的会话密钥,找到HMQV协议的安全漏洞,具有比传统Dolev-Yao敌手模型[2]更强的表征能力,能够更加准确地分析HMQV协议规范的安全性。（2）提出了递归协议安全性判定算法。该算法针对递归协议难以形式化描述的问题,能够对安全路由协议进行验证。该算法首先通过对递归协议消息项建模,建立递归协议安全性判定约束系统;其次在拓展的敌手模型条件下,通过简化规则,将协议拓展敌手模型下的可推导项置于约束系统下;最后给出了基于映射的递归语言的判定过程,并证明该递归语言的安全性判定是一个NP问题。（3）提出了基于状态机学习的安全协议实现模型提取技术,有效提高传统状态机模型提取算法效率。该算法首先针对测试序列生成较慢的问题,提出检查点算法,通过构造前缀树来存储之前已经执行过的查询,使得测试序列生成所用步骤减少,缩短了状态机生成时间。其次针对测试序列生成数量多的问题,提出了套接字约简方法,根据安全协议自身的安全机制,利用影响协议后续交互的套接字,约简相应生成的测试序列。实验针对TLS协议实现的状态机进行学习,成功学习到了Gnu TLS、Open SSL、NSS三种TLS协议实现的状态机模型。实验结果证明,与传统方法相比,该技术能够减少学习过程中测试序列的等价查询数量及所用学习时间,解决了传统状态机模型提取算法中状态机学习时间随目标系统状态数增长而呈指数级增长的问题。（4）提出了基于模型检测的协议实现分析方法。该方法以协议实现的状态机为输入,将协议规范及实现声明的安全属性建模为线性时态逻辑,通过模型检测器Nu SMV对安全属性进行验证,将验证结果分为属性满足和不满足。同时基于协议的安全声明,建立了安全属性、密钥交换属性以及功能属性3类共8项安全属性。实验对TLS实现进行分析,找到了两个TLS协议实现的协议逻辑漏洞,证明该方法所得的模型检测结果可以发现协议规范与协议实现之间的差异,有效发现协议实现状态机的逻辑漏洞。
欢迎来到三峡大学图书馆！
