强安全模型下TLS1.3协议的形式化分析与优化∗
2021-11-09陆思奇周思渊
陆思奇,周思渊,毛 颖
1(解放军信息工程大学,河南 郑州 450001)
2(信息安全国家重点实验室(中国科学院 信息工程研究所),北京 100093)
3(中国科学院大学 网络空间安全学院,北京 100093)
网络安全协议能够解决信息的传输安全问题,以互联网工程任务组(Internet engineering task force,简称IETF)为代表的有关组织,为了弥补基本的TCP/IP 协议簇在安全方面的设计缺陷,对现有的TCP/IP 协议簇进行设计和改进,从而构成了包含多层网络安全协议的TCP/IP 协议簇安全架构,传输层安全协议TLS(transport layer security)就是这个安全架构中重要的组成部分.
TLS 协议是在安全套阶层协议SSL(secure socket layer)获得了推广使用之后,由IETF 基于SSL3.0 协议[1]制定的正式行业标准[2],TLS1.2[3]为当前大部分浏览器和使用HTTPS 协议的Web 服务主要使用的版本.然而,随着网络环境日趋复杂,TLS1.2 也开始暴露出越来越多的漏洞,既有加密算法的漏洞,如RC4 的漏洞[4],也有协议设计中的漏洞,如 Lucky 13[5]、POODLE[6]、Logjam[7]、三次握手攻击[8],以及实现过程中的漏洞,如Heartbleed[9]、状态机攻击[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]等.
为了满足更高的安全需求,设计开发出更加安全稳定的网络安全协议,对网络安全协议进行更加严格、可信的分析,一直以来就是信……
