基于Tamarin的MQTT协议安全性分析方法 |
| |
引用本文: | 郑红兵,王焕伟,赵琪,董姝岐,井靖.基于Tamarin的MQTT协议安全性分析方法[J].计算机应用研究,2023(10):3132-3137+3143. |
| |
作者姓名: | 郑红兵 王焕伟 赵琪 董姝岐 井靖 |
| |
作者单位: | 中国人民解放军战略支援部队信息工程大学网络空间安全学院 |
| |
基金项目: | 国家重点研发项目(2019QY502); |
| |
摘 要: | MQTT是物联网中被广泛应用的消息传输协议,其安全性问题备受关注。当前MQTT协议安全性分析主要面向协议实现平台,缺少面向协议标准的安全性测试,导致协议标准本身存在的安全缺陷难以发现。针对该问题,采用协议形式化分析技术,提出了一种基于Tamarin的MQTT协议安全性分析方法。该方法首先面向MQTT协议3.1.1标准,构建了协议状态机,并依据Tamarin语法规则,完成了形式化描述;然后针对保密属性和认证属性,给出了MQTT协议需要满足的安全属性引理描述;最后,基于Dolev-Yao威胁模型在Tamarin中完成了对47种协议安全属性的验证。结果显示有9种保密属性违反和29种认证属性违反,对结果进行攻击测试,验证了该方法对MQTT协议安全性分析的有效性,并提出了一种基于身份重认证的优化改进方案。
|
关 键 词: | MQTT协议 保密属性 认证属性 形式化分析 Tamarin |
|
|