| 基于Tamarin的MQTT协议安全性分析方法 |
| |
| 引用本文： | 郑红兵,王焕伟,赵琪,董姝岐,井靖. 基于Tamarin的MQTT协议安全性分析方法[J]. 计算机应用研究, 2023, 40(10): 3132-3137+3143 |
| |
| 作者姓名： | 郑红兵 王焕伟 赵琪 董姝岐 井靖 |
| |
| 作者单位： | 中国人民解放军战略支援部队信息工程大学网络空间安全学院 |
| |
| 基金项目： | 国家重点研发项目(2019QY502)； |
| |
| 摘 要： | MQTT是物联网中被广泛应用的消息传输协议，其安全性问题备受关注。当前MQTT协议安全性分析主要面向协议实现平台，缺少面向协议标准的安全性测试，导致协议标准本身存在的安全缺陷难以发现。针对该问题，采用协议形式化分析技术，提出了一种基于Tamarin的MQTT协议安全性分析方法。该方法首先面向MQTT协议3.1.1标准，构建了协议状态机，并依据Tamarin语法规则，完成了形式化描述；然后针对保密属性和认证属性，给出了MQTT协议需要满足的安全属性引理描述；最后，基于Dolev-Yao威胁模型在Tamarin中完成了对47种协议安全属性的验证。结果显示有9种保密属性违反和29种认证属性违反，对结果进行攻击测试，验证了该方法对MQTT协议安全性分析的有效性，并提出了一种基于身份重认证的优化改进方案。
|
| 关 键 词： | MQTT协议 保密属性 认证属性 形式化分析 Tamarin |
| 收稿时间： | 2023-02-03 |
| 修稿时间： | 2023-09-08 |
Tamarin-based security analysis of MQTT protocol |
| |
| Zheng Hongbing,Wang Huanwei,Zhao Qi,Dong Shuqi and Jing Jing. Tamarin-based security analysis of MQTT protocol[J]. Application Research of Computers, 2023, 40(10): 3132-3137+3143 |
| |
| Authors: | Zheng Hongbing Wang Huanwei Zhao Qi Dong Shuqi Jing Jing |
| |
| Affiliation: | PLA Strategic Support Force Information Engineering University,,,, |
| |
| Abstract: | |
| |
| Keywords: | MQTT protocol confidentiality property authentication property formal analysis Tamarin |
|
| 点击此处可从《计算机应用研究》浏览原始摘要信息 |
|
点击此处可从《计算机应用研究》下载全文 |
