基于Tamarin的MQTT協(xié)議安全性分析方法

鄭紅兵　王煥偉　趙琪　董姝岐　井靖

摘 要：MQTT是物聯(lián)網(wǎng)中被廣泛應(yīng)用的消息傳輸協(xié)議，其安全性問(wèn)題備受關(guān)注。當(dāng)前MQTT協(xié)議安全性分析主要面向協(xié)議實(shí)現(xiàn)平臺(tái)，缺少面向協(xié)議標(biāo)準(zhǔn)的安全性測(cè)試，導(dǎo)致協(xié)議標(biāo)準(zhǔn)本身存在的安全缺陷難以發(fā)現(xiàn)。針對(duì)該問(wèn)題，采用協(xié)議形式化分析技術(shù)，提出了一種基于Tamarin的MQTT協(xié)議安全性分析方法。該方法首先面向MQTT協(xié)議3.1.1標(biāo)準(zhǔn)，構(gòu)建了協(xié)議狀態(tài)機(jī)，并依據(jù)Tamarin語(yǔ)法規(guī)則，完成了形式化描述；然后針對(duì)保密屬性和認(rèn)證屬性，給出了MQTT協(xié)議需要滿足的安全屬性引理描述；最后，基于Dolev-Yao威脅模型在Tamarin中完成了對(duì)47種協(xié)議安全屬性的驗(yàn)證。結(jié)果顯示有9種保密屬性違反和29種認(rèn)證屬性違反，對(duì)結(jié)果進(jìn)行攻擊測(cè)試，驗(yàn)證了該方法對(duì)MQTT協(xié)議安全性分析的有效性，并提出了一種基于身份重認(rèn)證的優(yōu)化改進(jìn)方案。

關(guān)鍵詞：MQTT協(xié)議；保密屬性；認(rèn)證屬性；形式化分析；Tamarin

中圖分類(lèi)號(hào)：TP309 文獻(xiàn)標(biāo)志碼：A 文章編號(hào)：1001-3695（2023）10-038-3132-06

doi：10.19734/j.issn.1001-3695.2023.02.0038

Tamarin-based security analysis of MQTT protocol

Zheng Hongbing，Wang Huanwei，Zhao Qi，Dong Shuqi，Jing Jing

（College of Cyberspace Security，PLA Strategic Support Force Information Engineering University，Zhengzhou 450001，China）

Abstract：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.

Key words：MQTT protocol；confidentiality property；authentication property；formal analysis；Tamarin

0 引言

隨著物聯(lián)網(wǎng)、人工智能、6G等新技術(shù)的飛速發(fā)展，構(gòu)建“萬(wàn)物互聯(lián)”的智慧地球?qū)⒅饾u成為現(xiàn)實(shí)。根據(jù)IoT Analytics的調(diào)查報(bào)告，2022年，全球活躍的物聯(lián)網(wǎng)設(shè)備已達(dá)144億臺(tái)，預(yù)計(jì)2025年，將有270億臺(tái)物聯(lián)網(wǎng)設(shè)備接入網(wǎng)絡(luò)［1］，海量的設(shè)備接入和設(shè)備管理對(duì)網(wǎng)絡(luò)帶寬、通信協(xié)議以及平臺(tái)服務(wù)架構(gòu)帶來(lái)了極大的挑戰(zhàn)。MQTT協(xié)議憑借其簡(jiǎn)單易實(shí)現(xiàn)，支持QoS（服務(wù)質(zhì)量）、報(bào)文小等特點(diǎn)，被廣泛應(yīng)用于智慧城市、智慧醫(yī)療、工業(yè)互聯(lián)網(wǎng)等場(chǎng)景中。然而，根據(jù)CVE漏洞平臺(tái)數(shù)據(jù)顯示，目前已經(jīng)發(fā)現(xiàn)多種針對(duì)MQTT協(xié)議的漏洞［2］，包括命令注入、文件上傳、緩沖區(qū)溢出、堆溢出、未授權(quán)認(rèn)證等。攻擊者通過(guò)利用MQTT協(xié)議的安全漏洞發(fā)起攻擊，可能會(huì)造成用戶隱私泄露、設(shè)備被惡意控制、強(qiáng)制下線，嚴(yán)重的會(huì)造成設(shè)備崩潰。因此面向MQTT協(xié)議的安全性分析成為物聯(lián)網(wǎng)安全領(lǐng)域當(dāng)前研究的熱點(diǎn)問(wèn)題之一。

目前國(guó)內(nèi)外研究人員對(duì)MQTT協(xié)議的安全性分析主要針對(duì)協(xié)議實(shí)現(xiàn)的平臺(tái)。Jia等人［3］通過(guò)對(duì)MQTT協(xié)議在物聯(lián)網(wǎng)云平臺(tái)進(jìn)行研究，手動(dòng)分析評(píng)估了平臺(tái)在部署協(xié)議存在的漏洞。Ramos等人［4］在基于MQTT的安全解決方案中，提出了一種基于模板的模糊測(cè)試方法，對(duì)協(xié)議的安全性進(jìn)行分析。文獻(xiàn)［5］針對(duì)MQTT協(xié)議平臺(tái)提出了一種基于攻擊模式自動(dòng)生成測(cè)試用例的方法，該方法將測(cè)試用例生成應(yīng)用于MQTT協(xié)議實(shí)現(xiàn)的代理平臺(tái)，手動(dòng)分析了代理中的問(wèn)題缺陷。Roets等人［6］對(duì)MQTT協(xié)議使用默認(rèn)的配置，在IoTPenn程序上進(jìn)行了安全性分析，發(fā)現(xiàn)了協(xié)議遭遇了拒絕服務(wù)、偽造身份非法訪問(wèn)等安全問(wèn)題。文獻(xiàn)［7，8］圍繞MQTT協(xié)議在國(guó)內(nèi)的部署情況展開(kāi)研究，提出了一種黑盒模糊測(cè)試方法，針對(duì)MQTT協(xié)議客戶端實(shí)現(xiàn)，驗(yàn)證了消息通過(guò)代理服務(wù)器轉(zhuǎn)發(fā)實(shí)現(xiàn)攻擊的可能性。Wang等人［9］對(duì)MQTT、CoAP、AMQP協(xié)議實(shí)現(xiàn)平臺(tái)進(jìn)行了安全性分析，開(kāi)發(fā)了物聯(lián)網(wǎng)應(yīng)用層協(xié)議檢測(cè)工具M(jìn)PInspector，分析了不同平臺(tái)協(xié)議實(shí)現(xiàn)層面的安全性。針對(duì)MQTT協(xié)議的安全性分析，僅僅面向協(xié)議實(shí)現(xiàn)層面分析，不能從根本上解決協(xié)議的安全隱患，因此需要對(duì)MQTT協(xié)議標(biāo)準(zhǔn)層面進(jìn)行安全性驗(yàn)證。

針對(duì)MQTT協(xié)議缺乏面向協(xié)議標(biāo)準(zhǔn)的安全分析問(wèn)題，本文提出了一種基于Tamarin［10］的MQTT協(xié)議安全性分析方法。該方法基于MQTT 3.1.1標(biāo)準(zhǔn)［11］，用符號(hào)化的語(yǔ)言對(duì)協(xié)議狀態(tài)機(jī)［12］、安全目標(biāo)屬性以及攻擊者模型進(jìn)行形式化建模［13］。利用模型檢測(cè)工具Tamarin對(duì)協(xié)議目標(biāo)屬性進(jìn)行了安全性驗(yàn)證和結(jié)果分析，并在具體協(xié)議部署的環(huán)境中對(duì)分析結(jié)果進(jìn)行了驗(yàn)證。最后，提出了協(xié)議優(yōu)化改進(jìn)方案。

1 MQTT協(xié)議概述

消息隊(duì)列遙測(cè)傳輸（message queuing telemetry transport，MQTT）協(xié)議是一種輕量級(jí)的消息傳遞協(xié)議。本文分析及驗(yàn)證的對(duì)象采用當(dāng)前服務(wù)支持和使用最廣泛的3.1.1版本。

1.1 MQTT協(xié)議對(duì)象模型

MQTT協(xié)議采用發(fā)布訂閱式的體系結(jié)構(gòu)，由訂閱者（subscriber）、發(fā)布者（publisher）以及代理（broker）三個(gè)主要實(shí)體組成，如圖1所示。在這種架構(gòu)下，溫濕度等傳感器作為發(fā)布者，通過(guò)MQTT協(xié)議將感知的數(shù)據(jù)傳遞給MQTT代理，代理再將信息發(fā)送給訂閱者，訂閱者可以是移動(dòng)終端、可編程邏輯控制器PLC等。需要注意的是，不同的應(yīng)用場(chǎng)景下，客戶端設(shè)備既可以是發(fā)布者，也可以是訂閱者。這種體系結(jié)構(gòu)的優(yōu)點(diǎn)在于，發(fā)布者和訂閱者之間的通信是松耦合的，發(fā)布者不需要知道訂閱者的身份，也不需要知道訂閱者何時(shí)接收信息，而訂閱者也不需要知道發(fā)布者的身份。代理作為中間人，負(fù)責(zé)管理發(fā)布者和訂閱者之間的通信，實(shí)現(xiàn)了高效的信息傳遞和管理。同時(shí)，MQTT協(xié)議還支持QoS，可以保證信息的可靠傳遞。

1.2 MQTT協(xié)議交互過(guò)程

MQTT協(xié)議規(guī)定通信雙方按照發(fā)布者和訂閱者的角色完成數(shù)據(jù)交互，交互過(guò)程包括設(shè)備注冊(cè)、密鑰協(xié)商、連接、訂閱/取消訂閱、發(fā)布和斷開(kāi)連接六個(gè)部分。

a）設(shè)備注冊(cè)。發(fā)布者和訂閱者在信息傳遞之前在服務(wù)器中進(jìn)行注冊(cè)，服務(wù)器為發(fā)布、訂閱設(shè)備分配唯一的客戶端標(biāo)識(shí)符（clientID）。

b）密鑰協(xié)商。發(fā)布和訂閱設(shè)備通過(guò)密鑰協(xié)商確定客戶端設(shè)備的用戶名和密碼以及臨時(shí)密鑰key，用于對(duì)客戶端設(shè)備進(jìn)行身份驗(yàn)證和權(quán)限授權(quán)。

c）設(shè)備與服務(wù)器連接包括設(shè)備連接和連接確認(rèn)。設(shè)備向代理發(fā)送connect請(qǐng)求，進(jìn)行設(shè)備連接。如果connect消息格式不正確或發(fā)送連接超時(shí)，連接關(guān)閉，防止消耗代理服務(wù)器資源。代理服務(wù)器收到connect請(qǐng)求后，對(duì)發(fā)送連接請(qǐng)求的設(shè)備進(jìn)行認(rèn)證和授權(quán)，并發(fā)送ConnAck響應(yīng)消息。

d）訂閱和取消訂閱過(guò)程。訂閱客戶端和代理服務(wù)器建立連接后，向代理服務(wù)器發(fā)送Subscribe消息進(jìn)行主題訂閱。為了確定每一個(gè)訂閱，代理服務(wù)器向客戶端發(fā)送SubAck確認(rèn)消息數(shù)據(jù)包。與訂閱消息相對(duì)應(yīng)的是Unsubscribe消息，代理服務(wù)器接收到取消訂閱后刪除設(shè)備的訂閱，同時(shí)代理向訂閱設(shè)備發(fā)送一個(gè)UnsubAck確認(rèn)消息。

e）消息發(fā)布過(guò)程。如圖2所示，發(fā)布設(shè)備在收到ConnAck消息后，發(fā)送publish數(shù)據(jù)包，包含主題（topic）、有效載荷、QoS，以及deviceID以字節(jié)格式傳輸?shù)臄?shù)據(jù)。為了保證消息的可靠傳輸，MQTT協(xié)議提供了三種QoS供用戶選擇。QoS 0依賴底層的TCP/IP網(wǎng)絡(luò)來(lái)傳遞消息；QoS 1服務(wù)器的消息接收由PUBACK消息進(jìn)行確認(rèn)；QoS 2確保消息到達(dá)一次，并且消息不會(huì)重復(fù)發(fā)送，訂閱者需要向發(fā)布者發(fā)送Pubrec數(shù)據(jù)包，代理轉(zhuǎn)發(fā)后，發(fā)布者發(fā)送Pubrel數(shù)據(jù)包，訂閱者接收后發(fā)送Pubcomp來(lái)結(jié)束消息發(fā)布，保證實(shí)時(shí)性交互。具體消息發(fā)布過(guò)程如圖2所示。

f）設(shè)備斷開(kāi)連接。發(fā)布和訂閱設(shè)備向代理服務(wù)器發(fā)送disconnect消息，斷開(kāi)與服務(wù)器的連接。

2 MQTT協(xié)議形式化建模

本文采用協(xié)議形式化建模分析工具Tamarin對(duì)MQTT協(xié)議進(jìn)行形式化建模，使用安全協(xié)議理論語(yǔ)言（spthy）描述協(xié)議狀態(tài)轉(zhuǎn)移的過(guò)程，使用rule來(lái)表示協(xié)議的狀態(tài)，使用lemma來(lái)描述需要驗(yàn)證的安全屬性。下面分別描述對(duì)協(xié)議狀態(tài)機(jī)、安全屬性、攻擊者模型的建模過(guò)程。

2.1 MQTT協(xié)議狀態(tài)機(jī)建模

協(xié)議狀態(tài)機(jī)是對(duì)協(xié)議流程的動(dòng)態(tài)化描述，是用來(lái)進(jìn)行協(xié)議行為建模的有力工具，它描述了協(xié)議實(shí)體在它的生命周期內(nèi)所經(jīng)歷的狀態(tài)序列，以及如何響應(yīng)來(lái)自外界的各種事件。

在協(xié)議的模型中包括代理服務(wù)器、發(fā)布設(shè)備和訂閱設(shè)備三類(lèi)實(shí)體。根據(jù)MQTT協(xié)議標(biāo)準(zhǔn)對(duì)代理服務(wù)器、發(fā)布設(shè)備和訂閱設(shè)備進(jìn)行分析描述，構(gòu)建了協(xié)議運(yùn)行過(guò)程的狀態(tài)變化。服務(wù)器狀態(tài)機(jī)交互如圖3所示。

服務(wù)器在接收到連接請(qǐng)求后，會(huì)將其從初始狀態(tài)（server_init）轉(zhuǎn)換為連接確認(rèn)發(fā)送狀態(tài)（connack_sent），隨后在接收到設(shè)備訂閱消息時(shí)，會(huì)將其轉(zhuǎn)換為訂閱確認(rèn)狀態(tài)（suback_sent）。此外，服務(wù)器還能夠接收其他設(shè)備發(fā)送的訂閱（publish）、連接（connect）、取消訂閱（unsuback）等消息，并在接收到相關(guān)消息后轉(zhuǎn)換為相應(yīng)的確認(rèn)發(fā)送狀態(tài)。因此，服務(wù)器構(gòu)成的狀態(tài)集合為{server_init，connack_sent，suback_sent，puback_sent，unsuback_sent}。

發(fā)布設(shè)備交互過(guò)程如圖4所示，包括了連接、發(fā)布、取消發(fā)布以及斷開(kāi)連接的狀態(tài)交互變化。

發(fā)布設(shè)備初始狀態(tài)（publisher_init）在發(fā)送連接消息后轉(zhuǎn)換為連接發(fā)送狀態(tài)（connect_sent）并等待接收連接確認(rèn)消息（connack_sent），轉(zhuǎn)換為接收連接確認(rèn)狀態(tài)（connack_rcvd）。在發(fā)布（publish）消息后，客戶端狀態(tài)依次轉(zhuǎn)換為訂閱發(fā)送狀態(tài)發(fā)布狀態(tài)（publish_sent），發(fā)布確認(rèn)接收狀態(tài)（puback_recvd）以及斷開(kāi)連接發(fā)送狀態(tài)（disconnect_sent）如圖4所示，發(fā)布設(shè)備構(gòu)成的狀態(tài)集合為{publisher_init，connect_sent，connack_rcvd，publish_sent，puback_rcvd，disconnect_sent}。

訂閱設(shè)備交互過(guò)程如圖5所示，包括連接、訂閱、取消訂閱、斷開(kāi)連接的狀態(tài)交互變化。

訂閱設(shè)備初始狀態(tài)（subscriber_init）發(fā)送連接消息后轉(zhuǎn)換為連接發(fā)送狀態(tài)（connect_sent）并等待接收連接確認(rèn)消息（connack_sent），轉(zhuǎn)換為接收連接確認(rèn)狀態(tài)（connack_rcvd）。在發(fā)送訂閱（subscribe）、取消訂閱（unsubscribe）消息后，客戶端狀態(tài)依次轉(zhuǎn)換為訂閱發(fā)送狀態(tài)（subscribe_sent）、取消訂閱狀態(tài)（unsubscribe_sent），如圖5所示，客戶端設(shè)備構(gòu)成的狀態(tài)集合為{subscriber_init，connect_sent，connack_sent，connack_rcvd，subscribe_sent，suback_sent，suback_rcvd，unsubscribe_sent，unsuback_recvd，disconnect_sent}。

服務(wù)器和客戶端設(shè)備狀態(tài)機(jī)初始化在Tamarin中描述如下，其中rule表示對(duì)協(xié)議狀態(tài)的描述：

2.2 安全屬性建模

本文從協(xié)議標(biāo)準(zhǔn)規(guī)范出發(fā)，歸納了參與協(xié)議交互實(shí)體需要滿足的保密屬性和認(rèn)證屬性。在認(rèn)證屬性方面，考慮到參與協(xié)議交互雙方的身份認(rèn)證需求，本文采用文獻(xiàn)［14］的定義進(jìn)行分類(lèi)，主要包括存活性（aliveness）、弱一致性（weak agreement）、非單射一致性（noninjective agreement）和單射一致性（injective agreement）。在保密屬性方面，考慮到協(xié)議實(shí)體交互過(guò)程中信息的私密性，主要涉及設(shè)備密鑰以及主題（topic）和負(fù)載（payload）的保密性。其中，主題保密性包括發(fā)布主題、訂閱主題以及取消訂閱主題的保密性。

2.2.1 認(rèn)證屬性

根據(jù)協(xié)議規(guī)范，交互實(shí)體分為發(fā)布設(shè)備、訂閱設(shè)備和代理服務(wù)器三類(lèi)。根據(jù)這三類(lèi)實(shí)體發(fā)送的不同數(shù)據(jù)包類(lèi)型，將操作分為連接、取消連接、訂閱、取消訂閱和發(fā)布五種。此外，代理服務(wù)器向客戶端設(shè)備發(fā)送的操作也可以分為連接確認(rèn)、訂閱確認(rèn)、取消訂閱確認(rèn)和發(fā)布確認(rèn)四種?；谶@些操作，本文可以對(duì)36種認(rèn)證屬性進(jìn)行形式化建模，包括存活性、弱一致性、非單射一致性和單射一致性。認(rèn)證屬性如表1和2所示。

為了說(shuō)明建模過(guò)程，下面以訂閱設(shè)備向代理服務(wù)器發(fā)送數(shù)據(jù)為例，詳細(xì)介紹MQTT協(xié)議交互過(guò)程中連接devid單射一致性、訂閱的存活性、取消訂閱的弱一致性以及斷開(kāi)連接的非單射一致性的認(rèn)證屬性建模過(guò)程，安全屬性在Tamarin中用lemma表示。

1）訂閱設(shè)備到服務(wù)器devid_connect的單射一致性

代理服務(wù)器和發(fā)布客戶端在進(jìn)行connect的過(guò)程中devid的單射一致性。代理服務(wù)器認(rèn)為自己與客戶端設(shè)備完成了一次協(xié)議數(shù)據(jù)交換，并且數(shù)據(jù)交換是一一對(duì)應(yīng)的，協(xié)議參與的實(shí)體是代理服務(wù)器和客戶端設(shè)備，攻擊者沒(méi)有獲取數(shù)據(jù)交換的密鑰，且只存在一次協(xié)議的運(yùn)行，代理服務(wù)器認(rèn)為與設(shè)備進(jìn)行的通信消息沒(méi)有被

2）訂閱設(shè)備向服務(wù)器訂閱的存活性

客戶端設(shè)備向代理服務(wù)器發(fā)送訂閱請(qǐng)求，代理服務(wù)器對(duì)請(qǐng)求回應(yīng)。存活性要求除了在此時(shí)間點(diǎn)以外，設(shè)備和服務(wù)器都可以完成過(guò)MQTT協(xié)議運(yùn)行，防止設(shè)備掉線。在Tamarin中形式化建模為

3）訂閱設(shè)備向服務(wù)器取消訂閱的弱一致性

設(shè)備向代理服務(wù)器發(fā)送取消訂閱主題的消息完成一次信息交互，代理服務(wù)器認(rèn)為設(shè)備的身份可信。在Tamarin中形式化建模為

4）訂閱設(shè)備與服務(wù)器斷開(kāi)連接的非單射一致性

代理服務(wù)器認(rèn)為自己與設(shè)備端完成了一次協(xié)議的運(yùn)行，至少存在一次協(xié)議運(yùn)行，代理服務(wù)器認(rèn)為協(xié)議之間傳輸?shù)南⑹钦鎸?shí)設(shè)備提供的，消息沒(méi)有被竄改。在Tamarin中形式化建模為

2.2.2 保密屬性

保密屬性分別從發(fā)布設(shè)備、訂閱設(shè)備和代理服務(wù)器的角度對(duì)設(shè)備密鑰（secret_key）、客戶端編號(hào)（clientid）、發(fā)布主題及發(fā)布負(fù)載、訂閱主題和取消訂閱主題內(nèi)容等方面對(duì)期望協(xié)議滿足的保密屬性進(jìn)行建模，如表3所示。

下面以客戶端設(shè)備為例介紹保密屬性的建模過(guò)程。

1）設(shè)備私鑰sk的保密屬性

從客戶端的角度考慮私鑰sk的安全性，若客戶端聲明會(huì)話密鑰是保密的，并且攻擊者無(wú)法獲取其私鑰sk，則攻擊者不能夠造成加密信息泄露，只有合法的目標(biāo)可以實(shí)現(xiàn)消息的解密，在Tamarin中形式化建模為

2.3 攻擊者建模

在協(xié)議形式化安全性分析中，有eCK［15］和Dolev-Yao［16］兩種常用的攻擊者模型。其中，eCK模型是安全性較強(qiáng)的形式化模型，攻擊者可以獲取協(xié)議參與方的臨時(shí)密鑰，因此在該模型下證明安全的協(xié)議具有極高的安全保證。但是，eCK模型進(jìn)行安全證明的過(guò)程需要使用雙線性映射，導(dǎo)致計(jì)算效率較低。相比之下，Dolev-Yao模型能夠更好地模擬MQTT環(huán)境中的威脅，且代碼量較少，進(jìn)行協(xié)議分析時(shí)效率更高。因此，本文選擇Dolev-Yao攻擊者模型對(duì)攻擊者進(jìn)行建模。

在Dolev-Yao攻擊者模型中，攻擊者的能力主要包括以下幾個(gè)方面：

a）可以在不被察覺(jué)的情況下，嗅探公開(kāi)信道中的協(xié)議通信數(shù)據(jù)；

b）攻擊者可以丟棄、重構(gòu)公共信道中傳輸?shù)南?，從而破壞通信的完整性?/p>

c）攻擊者可以假冒合法的參與主體，參與協(xié)議通信，從而破壞通信的真實(shí)性；

d）攻擊者遵循所有的密碼學(xué)加密規(guī)范，只有在掌握密鑰的情況下才可以對(duì)消息進(jìn)行解密。

上述攻擊者能力在Tamarin中形式化建模為

3 驗(yàn)證及結(jié)果分析

基于前文構(gòu)建的MQTT協(xié)議狀態(tài)機(jī)、安全屬性以及攻擊者模型，利用Tamarin可以完成協(xié)議安全屬性的驗(yàn)證。Tamarin的驗(yàn)證過(guò)程如圖6所示，Tamarin的輸入為rule和lemma，通過(guò)模擬協(xié)議通信交互過(guò)程，將所有交互的情況進(jìn)行遍歷，結(jié)合定義的期望滿足的安全屬性進(jìn)行檢測(cè)，驗(yàn)證是否存在屬性違反，若驗(yàn)證通過(guò)（true），表示滿足安全屬性，否則驗(yàn)證不通過(guò)（false），輸出反例及攻擊路徑。驗(yàn)證平臺(tái)采用16核CPU（Intel CoreTM i7-10875H 2.30 GHz），16 GB內(nèi)存，操作系統(tǒng)為Ubuntu 20.04，Tamarin版本為 1.6.1。

3.1 保密屬性驗(yàn)證結(jié)果及分析

通過(guò)將協(xié)議狀態(tài)機(jī)模型及11條保密屬性的形式化描述輸入Tamarin進(jìn)行驗(yàn)證，驗(yàn)證過(guò)程如圖7所示，其中左邊綠色部分表示已經(jīng)驗(yàn)證通過(guò)的lemma，紅色的箭頭表示進(jìn)行攻擊的過(guò)程（見(jiàn)電子版）。

表4展示了協(xié)議參與實(shí)體發(fā)布設(shè)備、訂閱設(shè)備和代理服務(wù)器在secret_key、clientiD、publishpayload、publishTopic、subscribeTopic、unsubscribeTopic上的11種保密屬性的驗(yàn)證情況，其中“√”表示滿足，“×”表示不滿足，“/”表示不涉及。由結(jié)果可知，11種保密屬性中有2種滿足，9種不滿足。

設(shè)備的secret_key和publishTopic的保密性沒(méi)有違反，原因在于設(shè)備密鑰和發(fā)布主題具有較強(qiáng)的可以選擇性與私密性，攻擊者無(wú)法提前竊取相關(guān)的隱私信息，而clientID、publishpayload、subscribeTopic、unsubscribeTopic分別遭受了屬性違反，易遭到中間人攻擊和拒絕服務(wù)攻擊等。

a）clientID屬性違反，攻擊者冒充受害者設(shè)備連接到代理服務(wù)器，發(fā)送非法消息數(shù)據(jù)包進(jìn)行破壞，特別是當(dāng)服務(wù)器端檢測(cè)到相同的clientID設(shè)備，服務(wù)器會(huì)斷開(kāi)與當(dāng)前客戶端的連接，迫使受害者下線。

b）subscribeTopic屬性違反，攻擊者可以利用自己的client-ID進(jìn)行主題訂閱，非法獲取訂閱的相關(guān)信息，當(dāng)受害者設(shè)備發(fā)送其秘密消息時(shí)，代理服務(wù)器將數(shù)據(jù)傳輸給攻擊者。

c）publishPayload屬性違反，攻擊者也可以通過(guò)攔截設(shè)備發(fā)布的信息，對(duì)publishPayload內(nèi)容進(jìn)行修改，植入木馬文件，通過(guò)代理服務(wù)器的轉(zhuǎn)發(fā)將惡意的載荷發(fā)送給訂閱設(shè)備進(jìn)行攻擊。

d）unsubscribeTopic屬性違反，攻擊者能夠?qū)⑷∠嗛喯l(fā)送給服務(wù)器，迫使受害者無(wú)法恢復(fù)對(duì)相關(guān)主題的訂閱，影響設(shè)備的正常工作。

3.2 認(rèn)證屬性驗(yàn)證結(jié)果及分析

通過(guò)將協(xié)議狀態(tài)機(jī)模型及36條認(rèn)證屬性的形式化描述輸入Tamarin進(jìn)行驗(yàn)證，驗(yàn)證結(jié)果如表5所示。

表5展示了MQTT協(xié)議參與實(shí)體的connect、disconnect、subscribe、publish、connack、suback、unsuback、puback操作的存活性、弱一致性、非單射一致性、單射一致性認(rèn)證屬性的驗(yàn)證結(jié)果，共驗(yàn)證了36種認(rèn)證屬性，其中有29種屬性遭到違反，7種安全屬性得到滿足。

從實(shí)驗(yàn)結(jié)果中分析可知，從設(shè)備端到代理服務(wù)器端，除去unsubscribe的操作，其他的協(xié)議運(yùn)行操作都存在不同程度的認(rèn)證屬性違反，存在一定的安全風(fēng)險(xiǎn)。下面重點(diǎn)分析從設(shè)備端到服務(wù)器的通信交互過(guò)程中屬性違反安全風(fēng)險(xiǎn)等級(jí)最高的三種情況：

a）connect操作單射一致性沒(méi)有得到保證，說(shuō)明攻擊者可以收集客戶端向代理服務(wù)器發(fā)送的歷史信息，并重新發(fā)送到服務(wù)器上進(jìn)行重放攻擊。

b）subscribe操作、publish操作認(rèn)證屬性全部違反，攻擊者可以對(duì)設(shè)備發(fā)送的信息進(jìn)行竄改，劫持客戶端身份，發(fā)送精心構(gòu)建的消息負(fù)載，如木馬文件，將代理服務(wù)器作為“跳板”轉(zhuǎn)發(fā)給訂閱主題的設(shè)備，實(shí)施中間人攻擊。

c）disconnect操作認(rèn)證屬性違反，攻擊者可以重復(fù)發(fā)送斷開(kāi)連接消息，導(dǎo)致設(shè)備無(wú)法進(jìn)行重新連接，實(shí)施拒絕服務(wù)攻擊。

從代理服務(wù)器到客戶端的角度，connack、suback、un-suback、puback的認(rèn)證屬性全部違反，反映出在公共信道上的通信更容易遭受攻擊。攻擊者可以在服務(wù)器和客戶端之前的信道上隨意發(fā)送偽造代理的數(shù)據(jù)包，而訂閱設(shè)備和發(fā)布設(shè)備由于資源受限并不能分辨代理服務(wù)器真?zhèn)?，造成設(shè)備被非法控制，導(dǎo)致服務(wù)器到客戶端之間的認(rèn)證屬性遭到破環(huán)。

3.3 分析結(jié)果驗(yàn)證

針對(duì)發(fā)現(xiàn)的MQTT協(xié)議安全隱患，通過(guò)配置具體的協(xié)議應(yīng)用場(chǎng)景進(jìn)行安全性驗(yàn)證。驗(yàn)證實(shí)驗(yàn)環(huán)境采用16核CPU（Intel CoreTM i7-10875H 2.30 GHz），16 GB內(nèi)存，操作系統(tǒng)為Ubuntu 20.04，選擇MQTT協(xié)議開(kāi)源軟件Mosquittio v2.0.15作為MQTT協(xié)議代理服務(wù)器，選擇MQTTX v1.9.1作為協(xié)議信息交互的訂閱者和發(fā)布者，選擇滲透測(cè)試工具Burp suite［17］作為攻擊者實(shí)施攻擊測(cè)試（包括數(shù)據(jù)截獲、數(shù)據(jù)竄改、數(shù)據(jù)利用、身份劫持等），測(cè)試結(jié)果如表6所示。

其中：“/”表示不涉及；“√”表示存在。

根據(jù)測(cè)試結(jié)果，部署MQTT協(xié)議3.1.1標(biāo)準(zhǔn)的平臺(tái)，利用滲透測(cè)試工具可以實(shí)施數(shù)據(jù)截獲、竄改、利用及身份劫持。其中數(shù)據(jù)截獲、竄改、違反了協(xié)議的保密屬性，數(shù)據(jù)利用和身份劫持違反了協(xié)議的認(rèn)證屬性。測(cè)試結(jié)果驗(yàn)證了本文基于Tamarin的MQTT協(xié)議安全性分析方法的有效性。

4 基于身份重認(rèn)證的優(yōu)化方案

現(xiàn)有MQTT協(xié)議安全加固的方法是基于特定的實(shí)現(xiàn)框架（如OAuth 1.0a）［18］和基于AugPAKE協(xié)議的MQTT安全解決方案［19］，適用場(chǎng)景有限，無(wú)法從根本上解決MQTT協(xié)議的安全隱患。本文基于Tamarin對(duì)MQTT協(xié)議的形式化驗(yàn)證結(jié)果，提出了一種基于身份重認(rèn)證的優(yōu)化方案，該方案主要包括密鑰重計(jì)算和隨機(jī)會(huì)話標(biāo)識(shí)符生成兩部分，重點(diǎn)用來(lái)解決通信交互雙方身份確認(rèn)問(wèn)題和會(huì)話競(jìng)爭(zhēng)問(wèn)題。

1）密鑰重計(jì)算

首先，客戶端設(shè)備將通信雙方在密鑰協(xié)商階段已經(jīng)產(chǎn)生的共享密鑰key與連接消息組合；然后，通過(guò)消息驗(yàn)證碼算法，將加密后的消息發(fā)送給代理服務(wù)器，服務(wù)器通過(guò)計(jì)算MAC確定設(shè)備身份，將connack數(shù)據(jù)包與key重新計(jì)算MAC發(fā)送給客戶端設(shè)備，實(shí)現(xiàn)客戶端設(shè)備與代理服務(wù)器的身份認(rèn)證。這里選擇基于hash的MD5的MAC加密算法［20］對(duì)消息進(jìn)行加密，也稱(chēng)為HMAC-MD5，加密計(jì)算公式如下：

2）隨機(jī)會(huì)話標(biāo)識(shí)符生成

針對(duì)發(fā)布設(shè)備和代理服務(wù)器缺少會(huì)話綁定而導(dǎo)致的會(huì)話競(jìng)爭(zhēng)問(wèn)題，可能會(huì)導(dǎo)致客戶端設(shè)備發(fā)送的信息無(wú)法被代理服務(wù)器接收，從而無(wú)法滿足弱一致性的要求。為了解決這個(gè)問(wèn)題，可以在客戶端和代理之間的publish會(huì)話中添加隨機(jī)生成的會(huì)話標(biāo)識(shí)符m。通過(guò)消息中的會(huì)話標(biāo)識(shí)符，可以識(shí)別來(lái)自不同客戶端設(shè)備的兩個(gè)相同deviceID發(fā)送的消息，從而避免相同deviceID之間的資源爭(zhēng)奪，進(jìn)而減少攻擊者偽造合法用戶身份進(jìn)行信息竊取的可能性。

上述的協(xié)議改進(jìn)方案能夠解決協(xié)議交互過(guò)程中雙方無(wú)法確認(rèn)身份的問(wèn)題，并且能夠減少攻擊者竊取用戶身份爭(zhēng)奪服務(wù)器資源造成正常用戶無(wú)法正常使用的問(wèn)題。此外，改進(jìn)方案的兩部分可根據(jù)需要靈活選擇，若設(shè)備資源有限，只需在通信交互過(guò)程中添加隨機(jī)生成會(huì)話標(biāo)識(shí)符，若設(shè)備資源充足，可選擇密鑰重計(jì)算和隨機(jī)標(biāo)識(shí)符生成同時(shí)部署。

5 結(jié)束語(yǔ)

本文針對(duì)MQTT 3.1.1協(xié)議標(biāo)準(zhǔn)，對(duì)MQTT協(xié)議狀態(tài)機(jī)和期望滿足的安全屬性進(jìn)行了形式化建模，在Tamarin中驗(yàn)證了MQTT協(xié)議11種保密屬性和36種認(rèn)證屬性的滿足情況，發(fā)現(xiàn)了38種屬性違反，評(píng)估了MQTT協(xié)議在標(biāo)準(zhǔn)層面可能面臨的安全風(fēng)險(xiǎn)并進(jìn)行驗(yàn)證。針對(duì)面臨的安全屬性違反的情況，提出了一種基于身份重認(rèn)證的認(rèn)證屬性優(yōu)化方案。

下一步工作，一方面，利用Tamarin完成改進(jìn)后的MQTT協(xié)議的有效性驗(yàn)證，并從時(shí)間消耗和資源消耗等方面，詳細(xì)分析改進(jìn)方案的效率問(wèn)題；另一方面，把改進(jìn)方案與其他改進(jìn)方案進(jìn)行詳細(xì)比較分析，完成改進(jìn)方案的優(yōu)化工作。此外，為了進(jìn)一步提高形式化驗(yàn)證方法在協(xié)議安全性分析中的效率，基于機(jī)器學(xué)習(xí)的協(xié)議自動(dòng)化建模方法也是未來(lái)值得研究的內(nèi)容。

參考文獻(xiàn)：

［1］Hasan M.State of IoT 2022：number of connected IoT devices growing 18% to 14.4 billion globally［EB/OL］.（2022-05-19）.https：//iot-analytics.com/number-connected-iot-devices/.

［2］U.S.Department of Homeland Security（DHS） Cybersecurity and Infrastructure Security Agency（CISA）.CVE records［EB/OL］.［2022-10-18］.https：//cve.mitre.org/cgi-bin/cvekey.cgi？keyword=mqtt.

［3］Jia Yan，Xing Luyi，Mao Yuhang，et al.Burglars IoT paradise：understanding and mitigating security risks of general messaging protocols on IoT clouds［C］//Proc of IEEE Symposium on Security and Privacy.Piscataway，NJ：IEEE Press，2020：465-481.

［4］Ramos S H，Villalba M T，Lacuesta R.MQTT security：a novel fuzzing approach［J］.Wireless Communications and Mobile Computing，2018，2018：article ID 8261746.

［5］Sochor H，F(xiàn)errarotti F，Ramler R.Automated security test generation for MQTT using attack patterns［C］//Proc of the 15th International Conference on Availability，Reliability and Security.New York：ACM Press，2020：article No.97.

［6］Roets A，Tait B L.IoT-Penn：a security penetration tester for MQTT in the IoT environment［M］//Jahankhani H.Cybersecurity in the Age of Smart Societies.Cham：Springer，2023：141-157.

［7］徐繪凱，劉躍，馬振邦，等.MQTT安全大規(guī)模測(cè)量研究［J］.信息網(wǎng)絡(luò)安全，2020，20（9）：37-41.（Xu Huikai，Liu Yue，Ma Zhenbang，et al.MQTT security large-scale measurement research［J］.Information Network Security，2020，20（9）：37-41.）

［8］Xu Huikai，Yu Miao，Wang Yanhao，et al.Trampoline over the air：breaking in IoT devices through MQTT brokers［C］//Proc of the 7th European Symposium on Security and Privacy.Piscataway，NJ：IEEE Press，2022：171-187.

［9］Wang Qinying，Ji Shouling，Tian Yuan，et al.MPInspector：a systema-tic and automatic approach for evaluating the security of IoT messaging protocols［C］//Proc of the 30th USENIX Security Symposium.Berkeley，CA：USENIX Association，2021：4205-4222.

［10］Basin D，Cremers C，Dreier J，et al.The Tamarin manual［EB/OL］.https：//tamarin-prover.github.io/.

［11］Coppen R，Craggs I.ISO/IEC 20922：2016，OASIS message queuing telemetry transport（MQTT） TC［S/OL］.（2014-10-29）.http：//docs.oasis-open.org/mqtt/mqtt/v3.1.1/os/mqtt-v3.1.1-os.html.

［12］李峻辰，程光，楊剛芹.基于網(wǎng)絡(luò)流量的私有協(xié)議逆向技術(shù)綜述［J］.計(jì)算機(jī)研究與發(fā)展，2023，60（1）：167-190.（Li Junchen，Cheng Guang，Yang Gangqin.Private protocol reverse engineering based on network traffic：a survey［J］.Journal of Computer Research and Development，2023，60（1）：167-190.）

［13］苗新亮，常瑞，潘少平，等.可信執(zhí)行環(huán)境訪問(wèn)控制建模與安全性分析［J/OL］.軟件學(xué)報(bào).（2023-01-19）.https：//doi.org/10.13328/j.cnki.jos.006612.（Miao Xinliang，Chang Rui，Pan Shao-ping.Modeling and security analysis of access control in trusted execution environment［J/OL］.Journal of Software.（2023-01-19）.https：//doi.org/10.13328/j.cnki.jos.006612.

［14］Lowe G.A hierarchy of authentication specifications［C］//Proc of the 10th Computer Security Foundations Workshop.Piscataway，NJ：IEEE Press，1997：31-43.

［15］Lamacchia B，Lauter K，Mityagin A.Stronger security of authenticated key exchange［C］//Proc of International Conference on Provable Security.Berlin：Springer，2007：1-16.

［16］Dolev D，Yao A.On the security of public key protocols［J］.IEEE Trans on Information Theory，1983，29（2）：198-208.

［17］Arvind S，Narayanan V A.An overview of security in coap：attack and analysis［C］//Proc of the 5th International Conference on Advanced Computing & Communication Systems.Piscataway，NJ：IEEE Press，2019：655-660.

［18］Niruntasukrat A，Issariyapat C，Pongpaibool P，et al.Authorization mechanism for MQTT-based Internet of Things［C］//Proc of IEEE International Conference on Communications Workshops.Piscataway，NJ：IEEE Press，2016：290-295.

［19］Sahmi I，Abdellaoui A，Mazri T，et al.MQTT-PRESENT：approach to secure Internet of Things applications using MQTT protocol［J］.International Journal of Electrical & Computer Engineering，2021，11（5）：4577-4586.

［20］Lawrence T，Li Fagen，Ali I，et al.A computationally efficient HMAC-based authentication scheme for network coding［J］.Telecommunication Systems，2022，79（1）：47-69.

收稿日期：2023-02-03；修回日期：2023-04-04 基金項(xiàng)目：國(guó)家重點(diǎn)研發(fā)項(xiàng)目（2019QY502）

作者簡(jiǎn)介：鄭紅兵（1995-），男，河南平頂山人，碩士研究生，主要研究方向?yàn)槲锫?lián)網(wǎng)安全；王煥偉（1987-），男，河南周口人，講師，博士研究生，主要研究方向?yàn)槲锫?lián)網(wǎng)安全、協(xié)議安全；趙琪（1999-），男，河南三門(mén)峽人，主要研究方向?yàn)槲锫?lián)網(wǎng)安全；董姝岐（1997-），女，河南商丘人，碩士研究生，主要研究方向?yàn)槲锫?lián)網(wǎng)安全；井靖（1980-），女（通信作者），河南鄭州人，副教授，碩導(dǎo)，博士，主要研究方向?yàn)槲锫?lián)網(wǎng)安全、信息物理系統(tǒng)安全（jingjing_cs@hotmail.com）．