Page 226 - 《软件学报》2021年第9期

2850 Journal of Software 软件学报 Vol.32, No.9, September 2021

IETF)为代表的有关组织,为了弥补基本的 TCP/IP 协议簇在安全方面的设计缺陷,对现有的 TCP/IP 协议簇进行
设计和改进,从而构成了包含多层网络安全协议的 TCP/IP 协议簇安全架构,传输层安全协议 TLS(transport layer
security)就是这个安全架构中重要的组成部分.
TLS 协议是在安全套阶层协议 SSL(secure socket layer)获得了推广使用之后,由 IETF 基于 SSL3.0 协议 [1]
[2]
[3]
制定的正式行业标准 ,TLS1.2 为当前大部分浏览器和使用 HTTPS 协议的 Web 服务主要使用的版本.然而,
[4]
随着网络环境日趋复杂,TLS1.2 也开始暴露出越来越多的漏洞,既有加密算法的漏洞,如 RC4 的漏洞 ,也有协
[7]
[8]
[5]
[6]
议设计中的漏洞,如 Lucky 13 、POODLE 、Logjam 、三次握手攻击 ,以及实现过程中的漏洞,如
[9]
Heartbleed 、状态机攻击 [10] 等.虽然很多安全漏洞已经通过不定期更新和补丁解决,但由于 TLS 庞大的规模以
及许多不同的设置,这些反复的修改增加了 TLS 的复杂性和部署难度.因此,IETF 的 TLS 工作组开始着手设计
“下一代 TLS”——TLS1.3.目前,TLS1.3 正处于草案阶段 [11] ,吸引了协议研究者们的广泛关注,既有针对 TLS1.3
攻击方法的研究,如证书转发攻击 [12] 、中间人攻击 [13] 、DROWN [14] 、Client AuthenticationAttack [15,16] ,也有对
TLS1.3 的安全性分析和建议,如 OPTLS [17] ,TLS-Attacker 模型 [18] 等.
为了满足更高的安全需求,设计开发出更加安全稳定的网络安全协议,对网络安全协议进行更加严格、可
信的分析,一直以来就是信息安全和密码学领域的一大热点.形式化方法使用数学的方法描述和推理计算机系
统,具有准确的语法以及语义,并通过精确的数学手段和强大的分析工具实现技术支持.简而言之,就是规范语
言加形式推理 [19] .形式化方法遍历搜索协议在运行过程中所有可能的状态,往往能够挖掘出安全协议中难以发
现的细微漏洞,是目前非常流行的安全协议分析方法.
本文参考了 Krawczyk 等人 [17] 关于 OPTLS 的工作,使用形式化分析工具 Scyther 分析了 CK 模型下对 Early
Data 的具体攻击.一方面,Early Data 不具有 PFS 安全,数据可能被攻击者窃取;另一方面, Early Data 无法抵抗
KCI 攻击.根据分析结果,本文对 TLS1.3 协议进行了优化,有效提高了协议的安全性.
本文第 1 节介绍 TLS1.3 和 Syther 等预备知识.第 2 节为使用 Scyther 工具对 TLS1.3 协议进行分析的过程
和结论.第 3 节基于 TLS1.3 中的 1-RTT semi-static 模式设计一种优化的协议,在 CK 安全模型下从安全性证明
和形式化分析的角度证明优化协议能够抵抗 KCI 攻击,并进行效率分析.第 4 节对本文的工作进行小结,进一步
明确后续研究方向.
1 预备知识

1.1 Scyther简介
Scyther 是一款形式化分析安全协议的工具,该工具由牛津大学的 Cremers 教授及其团队 [20] 所开发.这款工
具综合运用了定理证明以及模型检测等分析技术,具有如下特点.
(1) 能够多协议并行分析;
(2) 能够通过无限会话来验证协议;
(3) 能够通过描述协议,产生所有协议可能行为的有限表示;
(4) 能够通过组合敌手能力构造各种安全模型.
Scyther 对协议分析者最友好的一面是其基于按钮的使用界面以及可视化的分析结果,这使得协议的研究
过程能够更加方便和直观.除此之外,Scyther 通过控制主体执行轮数和约束状态空间对搜索状态进行双重限制,
与之前仅通过约束状态空间的方法相比,减少了攻击漏报的可能性,而且不会因为状态爆炸而出现无分析结果
的情况.Scyther 的协议形式化语言 SPDL 简单易学,尽可能分割我们在安全协议形式化分析中的要点,即明确区
分了协议的静态描述、动态行为以及敌手模型.更进一步讲,该语言模型实现了多方协议并行运作的直观掌控、
安全声明的局部化、局部常量与角色实例的绑定以及初始敌手知识集合的简明定义.
Scyther 曾经被用来分析过许多著名协议,除了 Cremers [21,22] 曾经用其分析过 IKEv1 和 IKEv2 协议套件和
ISO/IEC 9798 系列认证协议,Yang 和 Oleshchuk 等人 [23,24] 还使用 Scyther 分析了群认证协议,Ray 和 Chowdhury
等人 [25] 则使用 Scyther 分析了物联网协议.该工具最新的版本为 Scyther v1.1.3(标准版本,如果需要支持更多敌