-
题名强安全模型下TLS1.3协议的形式化分析与优化
被引量：7
- 1
-
-
作者
陆思奇
周思渊
毛颖
-
机构
解放军信息工程大学
信息安全国家重点实验室(中国科学院信息工程研究所)
中国科学院大学网络空间安全学院
-
出处
《软件学报》
EI
CSCD
北大核心
2021年第9期2849-2866,共18页
-
基金
国家自然科学基金(61472414,61772514,61602061)。
-
文摘
TLS协议在TCP/IP体系中的传输层和应用层之间工作,通过提供机密性、完整性、必选的服务器认证以及可选的客户端认证等一系列安全服务,有效保护了传输层的安全.TLS1.3协议为了降低网络延迟,增加了对0-RTT数据的支持,通过客户端缓存服务器的长期公钥,在第1条消息中,直接利用该长期公钥生成一个会话密钥发送部分应用层数据.针对3种0-RTT模式,使用Scyther工具对其进行了形式化分析,得出了在CK安全模型下,0-RTT数据的两种攻击,并基于其中的1-RTT semi-static模式提出了一种优化协议.通过安全性证明和形式化分析,证明了该优化协议在CK安全模型下能够抵抗针对0-RTT数据的KCI攻击和重放攻击.
-
关键词
TLS1.3
形式化分析
syther
CK安全模型
KCI攻击
-
Keywords
TLS1.3
formal analysis
Scyther
CK security model
KCI attacks
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
