基于Tamarin的MQTT协议安全性分析方法

Tamarin-based security analysis of MQTT protocol

MQTT是物联网中被广泛应用的消息传输协议,其安全性问题备受关注。当前MQTT协议安全性分析主要面向协议实现平台,缺少面向协议标准的安全性测试,导致协议标准本身存在的安全缺陷难以发现。针对该问题,采用协议形式化分析技术,提出了一种基于Tamarin的MQTT协议安全性分析方法。该方法首先面向MQTT协议3.1.1标准,构建了协议状态机,并依据Tamarin语法规则,完成了形式化描述;然后针对保密属性和认证属性,给出了MQTT协议需要满足的安全属性引理描述;最后,基于Dolev-Yao威胁模型在Tamarin中完成了对47种协议安全属性的验证。结果显示有9种保密属性违反和29种认证属性违反,对结果进行攻击测试,验证了该方法对MQTT协议安全性分析的有效性,并提出了一种基于身份重认证的优化改进方案。

The MQTT protocol is widely used in the Internet of Things for message transmission,and its security issues have received much attention.Currently,security analysis of the MQTT protocol mainly focuses on protocol implementation platforms,lacking security testing based on protocol standards,which makes it difficult to detect security vulnerabilities in the protocol standards themselves.To address this issue,this paper proposed a formal analysis method for MQTT protocol security based on Tamarin.The method firstly constructed a protocol state machine based on the MQTT protocol 3.1.1 standard,and completed formal description based on Tamarin syntax rules.Then,for confidentiality and authentication properties,the security properties that MQTT protocol needed to satisfy were given in the form of lemma descriptions.Finally,it completed the verification of 47 protocol security attributes based on the Dolev-Yao threat model in Tamarin.The results show that there are 9 confidentiality attribute violations and 29 authentication attribute violations.It conducted an attack test on the results,and the test results verify the effectiveness of the proposed method for MQTT protocol security analysis.It also proposed an optimized and improved scheme based on identity reauthentication.