| 基于符号模型的TLS1.3协议安全性自动化分析 |
| |
| 引用本文： | 王小峰,张奇林,刘加兵.基于符号模型的TLS1.3协议安全性自动化分析[J].数学的实践与认识,2019(5). |
| |
| 作者姓名： | 王小峰 张奇林 刘加兵 |
| |
| 作者单位： | 深圳大学传播学院;武汉大学政治与公共管理学院;中南民族大学计算机科学学院 |
| |
| 摘 要： | 网络安全是网络空间安全的一个重要研究领域,网络安全协议则是实现网络安全的核心技术.在2017年最新发布的TLS1.3协议是实现网络安全的一个关键传输层安全协议,因此其安全性受到了人们的广泛关注.为了验证TLS1.3协议的安全性,尤其是秘密性和认证性,尝试基于符号模型,首先基于Applied PI演算对TLS1.3协议进行形式化建模,进而使用非单射性建模认证性,然后将针对TLS1.3协议的Applied PI演算模型转换为安全协议分析工具ProVerif的输入,应用ProVerif对其进行形式化分析,实验结果表明TLS 1.3协议具有良好的认证性和机密性.
|
| 关 键 词： | 认证性 秘密性 Applied PI演算 符号模型 形式化方析 ProVerif |
Automatic Analysis of Security of TLS1.3 Protocol Based on the Symbolic Model |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 等数据库收录！ |
|
