基于云平臺物聯(lián)網(wǎng)的多因子遠(yuǎn)程身份認(rèn)證方法

于光華 夏魁良 辛明遠(yuǎn) 王詩瑩

1(黑河學(xué)院計算機(jī)與信息工程學(xué)院 黑龍江 黑河 164300)2(哈爾濱商業(yè)大學(xué)管理學(xué)院 黑龍江 哈爾濱 150076)

0 引 言

遠(yuǎn)程身份認(rèn)證[1]是在不安全網(wǎng)絡(luò)中對遠(yuǎn)程用戶的合法性進(jìn)行認(rèn)證的過程。傳統(tǒng)的單因子密碼認(rèn)證存在很多缺陷，例如密碼容易被遺忘、容易被猜解攻擊等，不足以確保較高的安全性[2]。由于分布式環(huán)境越來越普及，傳統(tǒng)的單服務(wù)器方案[3]的局限性越來越明顯。云計算通過共享和優(yōu)化應(yīng)用對硬件資源的能力進(jìn)行擴(kuò)展，成為一種可靠的解決途徑。

王超等[4]提出基于橢圓曲線加密的多因子遠(yuǎn)程身份驗證方案，包括密碼、智能卡和生物統(tǒng)計信息3個因子。Dhillon等[5]提出了一種基于橢圓曲線密碼的多因子遠(yuǎn)程身份認(rèn)證方案，采用云物聯(lián)網(wǎng)技術(shù)，并將其應(yīng)用到遠(yuǎn)程醫(yī)療方案的解決中。Mishra[6]改進(jìn)了生物特征隱私的表示方法，但該方案容易受到智能卡丟失攻擊，也無法抵御冒名攻擊。崔維等[7]提出一種輕量級的動態(tài)化密鑰協(xié)商的身份認(rèn)證協(xié)議。該協(xié)議在用戶進(jìn)行登錄驗證時使用時間戳值，可防范重放攻擊以及拒絕服務(wù)攻擊，但該方案不能檢測無效輸入。Banerjee等[8]提出一種基于生物特征的遠(yuǎn)程用戶身份認(rèn)證的改進(jìn)方法。網(wǎng)關(guān)節(jié)點充當(dāng)?shù)谌剑荑€協(xié)商協(xié)議與首選傳感器節(jié)點協(xié)商為認(rèn)證，從而啟動會話密鑰，建立可靠連接。該方案使用單向散列函數(shù)、位異或(XOR)和concat操作。屈娟等[9]指出文獻(xiàn)[10]的缺點：易受智能卡丟失攻擊和模仿攻擊等，且用戶匿名性難以保證。文獻(xiàn)[9]提出一種改進(jìn)方法，利用生物特征和混沌函數(shù)完成身份認(rèn)證。

與以上相關(guān)方案技術(shù)不同，本文最大的特點是基于云計算的物聯(lián)網(wǎng)(Internet of Things, IoT)應(yīng)用，充分利用云計算處理多服務(wù)器的遠(yuǎn)程身份認(rèn)證，提出一種基于智能卡的多因子輕量級認(rèn)證方案，使用了XOR和散列函數(shù)使之具有輕量級，并具有其他眾多關(guān)鍵的安全屬性。

1 方法介紹

基于云計算的架構(gòu)如圖1所示，其中多個IoT網(wǎng)絡(luò)連接至云服務(wù)器。由此支持遠(yuǎn)程用戶訪問IoT網(wǎng)絡(luò)生成的數(shù)據(jù)。本文遠(yuǎn)程身份認(rèn)證方案基于此框架，主要包括6個階段：1) 預(yù)計算階段；2) 注冊階段；3) 登錄階段；4) 身份認(rèn)證階段；5) 密碼更改階段；6) 智能卡撤銷階段。本文方案所使用的數(shù)學(xué)符號及含義如表1所示。

圖1 本文遠(yuǎn)程身份認(rèn)證的云計算框架

表1 本文的符號說明

續(xù)表1

1.1 預(yù)計算階段

服務(wù)器以離線模式進(jìn)行參數(shù)初始化。服務(wù)器生成素數(shù)U、整數(shù)V，以使得：

U×V≡1(mod(p-1)(q-1))

(1)

并計算：

V≡U-1(mod(p-1)(q-1))

(2)

SR將U作為公鑰，V作為私鑰。私鑰保持保密性，并發(fā)布公鑰。本文方案使用輕量級加密散列函數(shù)，定義為：

h: {0, 1}*→ {0, 1}l

(3)

式中：l為h(·)的輸出長度。

1.2 注冊階段

該階段中，遠(yuǎn)程用戶注冊到服務(wù)器。為此，用戶Ui向服務(wù)器SR提交注冊請求。為成功完成注冊，Ui需要執(zhí)行以下步驟。

步驟1用戶Ui選擇唯一標(biāo)識usernamei、密碼PWi。 其后，用戶生成一個隨機(jī)數(shù)R1。此外，Ui計算掩藏標(biāo)識MIDi=h(R1‖usernamei)和掩藏密碼MPWi=h(R1‖PWi)。用戶通過安全信道將消息{MIDi}發(fā)送至遠(yuǎn)程服務(wù)器SR。

步驟2在接收到消息后，SR使用私鑰V計算MVi=h(MIDi‖V)，將參數(shù){MVi,h(·)}保存在智能卡SC內(nèi)并通過安全信道將SC發(fā)布至用戶Ui。

步驟3在接收到智能卡SC后，用戶Ui計算Xi=h(usernamei‖MPWi)，Yi=h(usernamei‖PWi)，Zi=MVi⊕Xi，Ai=h(usernamei⊕MPWi)，Bi=R1⊕Yi。用戶從智能卡存儲中刪除計算出的參數(shù)MVi。Ui將{Zi,Ai,Bi,h(·)}保存到智能卡SC中。

1.3 登錄階段

該階段中，用戶Ui向服務(wù)器提交登錄請求。為發(fā)起會話，需要執(zhí)行以下步驟。

步驟1用戶Ui將智能卡插入讀卡器，輸入標(biāo)識usernamei′和密碼PWi′。

步驟2智能卡SC計算Yi′ =h(usernamei′‖PWi′)。為計算MIDi′和MPWi′，SC提取R1′=Bi⊕Yi′并計算MIDi′=h(R1′‖usernamei′)，MPWi′=h(R1′‖PWi′)。

步驟3此外，SC計算Xi′=h(usernamei′‖MPWi′)，并提取MVi′，MVi′=Zi⊕Xi′。其計算Ai′=h(usernamei′⊕MPWi′)并檢查其存儲的Ai是否等于計算出的Ai′。若相等，則用戶通過認(rèn)證，SC繼續(xù)下一個步驟。否則，登錄請求將被中止。

步驟4在成功完成認(rèn)證后，智能卡AC在當(dāng)前時間戳T1生成一個隨機(jī)新鮮值R2。SC計算Auth1=h(R2‖MVi′ ‖T1)，Auth2=h(MIDi′ ‖MVi′‖T1) ⊕R2。SC將消息{MIDi′ ,Auth1,Auth2,T1}發(fā)送至服務(wù)器。

1.4 身份認(rèn)證階段

該階段中，服務(wù)器和用戶彼此進(jìn)行雙向認(rèn)證。在成功完成身份認(rèn)證后，生成共享的加密會話密鑰。身份認(rèn)證階段的步驟如下：

步驟1在接收到登錄消息后，服務(wù)器SR生成當(dāng)前時間戳Ti′，并認(rèn)證(Ti′-T1)≤△T是否成立。該條件確保本文方案能夠抵御重放攻擊。若條件不成立，中止身份認(rèn)證過程。若條件成立，SR計算MVi′=h(MIDi′‖V)，并從Auth2中提取R2，R2′=Auth2⊕h(MIDi′ ‖MVi′ ‖T1)。

步驟2此外，服務(wù)器計算Auth1′=h(R2‖MVi′‖T1)，并認(rèn)證Auth1′=Auth1是否成立。若條件成立，則遠(yuǎn)程服務(wù)器確認(rèn)用戶為合法用戶，繼續(xù)下一個階段。否則，SR將中止認(rèn)證過程。

步驟3SR在當(dāng)前時間戳T2生成隨機(jī)數(shù)R3，并計算加密會話密鑰SKey=h(MIDi‖R2′‖R3‖T1‖T2)，Auth3=R2′⊕R3，Auth4=h(SKey‖MVi′ ‖R3‖T1‖R2′ ‖T2)。其后，SR將消息{Auth3,Auth4,T2}發(fā)送至Ui。

步驟4在接收到消息后，SC首先對時間戳進(jìn)行檢查。SC生成當(dāng)前時間戳T2′，并認(rèn)證(T2′-T2) ≤ △T是否成立。若條件不成立，則中止會話。若條件成立，SC計算R3′=R2⊕Auth3，SKey=h(MIDi′‖R2‖R3′‖T1‖T2)，Auth4′=h(SKey‖MVi′‖R3′‖T1‖R2‖T2)。SC檢查Auth4′=Auth4是否成立。若條件成立，用戶Ui和遠(yuǎn)程服務(wù)器SR完成雙向認(rèn)證，繼續(xù)下一進(jìn)程。若不成立，則會話中止。

步驟5在當(dāng)前時間戳T3，SC計算AuthSKey=h(SKey‖MVi′ ‖MIDi′ ‖T2‖T3)，并通過安全信道將消息{AuthSKey,T3}發(fā)送至遠(yuǎn)程服務(wù)器SR。

步驟6在接收到消息后，SR生成當(dāng)前時間戳T3′，并認(rèn)證(T3′-T3) ≤ △T是否成立。若條件不成立，則會話中止。若條件成立，SR計算AuthSKey′=h(SKey‖MVi′‖MIDi′‖T2‖T3) ，并認(rèn)證AuthSKey′=AuthSKey是否成立。若條件成立，則會話密鑰SKey通過認(rèn)證。在完成雙向認(rèn)證后，使用會話密鑰SKey對所有消息進(jìn)行加密。

1.5 密碼更改階段

本文方案允許授權(quán)用戶進(jìn)行密碼更新。智能卡在啟動密碼更新之前，先對用戶進(jìn)行身份認(rèn)證。用戶可自主決定其密碼。該階段非常重要，因為定期更新密碼有助于提高安全性。密碼更改階段要執(zhí)行以下步驟：

步驟1用戶插入其智能卡SC，并輸入標(biāo)識usernamei′和舊密碼PWi′。

步驟2在授權(quán)用戶更新密碼之前，智能卡SC檢查用戶的真實性。SC計算Yi′=h(usernamei′‖PWi′)，提取R1′=Bi⊕Yi′，并計算MIDi′=h(R1′‖usernamei′)，MPWi′=h(R1′‖PWi′)。

步驟3此外，SC計算Xi′=h(usernamei′‖MPWi′) ，并提取MVi′=Zi⊕Xi′。其計算Ai′=h(usernamei′⊕MPWi′)，并認(rèn)證其保存的Ai與當(dāng)前計算出的Ai′是否匹配。若認(rèn)證未通過，則SC拒絕用戶Ui的請求并中止進(jìn)程。若認(rèn)證通過，SC要求用戶提交新密碼PWi*。

步驟4用戶向SC提交新密碼PWi*。

步驟5在接收到新密碼后，SC計算MPWi*=h(R1′ ‖PWi*)，Xi*=h(usernamei‖MPWi*)，Yi*=h(usernamei‖PWi*)，Zi*=MVi′⊕Xi*，Ai*=h(usernamei⊕MPWi*)，Bi*=R1′⊕Yi*。智能卡將之前保存的參數(shù){Zi,Ai,Bi}替換為{Zi*,Ai*,Bi*}。

1.6 智能卡撤銷階段

該階段中，用戶可對失竊或丟失的智能卡進(jìn)行撤銷。服務(wù)器再次執(zhí)行對用戶的注冊。本文方案可抵御冒名攻擊，因為其中未使用之前使用過的數(shù)值(例如密碼)。由此，攻擊者無法利用其提取出的數(shù)值假冒合法用戶。智能卡撤銷階段步驟如下：

步驟1用戶Ui向服務(wù)器SR請求撤銷智能卡。在啟動撤銷進(jìn)程之前，服務(wù)器SR先認(rèn)證用戶的憑證(例如檢驗生物特征或Ui預(yù)留的保密值)。

步驟2若用戶的撤銷請求成功通過認(rèn)證，則Ui選擇密碼PWi′并生成一個隨機(jī)數(shù)R1′。Ui計算掩藏標(biāo)識MIDi′=h(R1′‖usernamei)以及掩藏密碼MPWi′=h(R1′‖PWi′)。用戶通過安全信道將消息{MIDi′}發(fā)送至遠(yuǎn)程服務(wù)器SR。

步驟3服務(wù)器接收新的注冊請求消息，并計算MVi′h(MIDi′ ‖V)，其中V為SR的私鑰。服務(wù)器為注冊用戶Ui生成新的智能卡SCnew，其中包含參數(shù){MVi′,h(·)}，并通過安全信道發(fā)送至Ui。

2 安全性分析與認(rèn)證

2.1 安全性分析

2.1.1抵御偽造攻擊

本文方案可抵御偽造攻擊。竊聽者可能攔截到合法實體之間正在進(jìn)行的通信，并再次進(jìn)行提交，試圖假冒認(rèn)證用戶。假定攻擊者J記錄下用戶在登錄階段發(fā)送的消息{MIDi′,Auth1,Auth2,T1}。但攻擊者J無法假冒認(rèn)證用戶，因為要計算合法登錄請求，J必須具有參數(shù)PWi和R1的先驗知識。這些參數(shù)從未傳輸過，因此J無法成功生成有效消息。

2.1.2抵御重放攻擊

本文方案可抵御重放攻擊。攻擊者J可能記錄下之前會話中發(fā)送過的消息，并嘗試將消息再次發(fā)送至服務(wù)器。本文方案所使用的時間戳，通過檢測傳輸時間的延遲來防止重放攻擊。假定攻擊者再次傳輸其攔截到的消息：J記錄下登錄請求{MIDi′,Auth1,Auth2,T1}。J通過發(fā)送Auth1=h(R2‖MVi′ ‖T1)、Auth2=h(MIDi′ ‖MVi′ ‖T1)R2以發(fā)起一個新會話。首先，本文方案采用了時間戳，所以請求將被取消。J不可能在多項式時間內(nèi)利用蠻力分析攻擊破解所有參數(shù)[11-12]，這會造成傳輸延遲，被遠(yuǎn)程服務(wù)器所檢測。

2.1.3抵御密碼猜測攻擊

本文方案可抵御密碼猜測攻擊。假定攻擊者J記錄下兩條消息：請求消息{MIDi′,Auth1,Auth2,T1}和應(yīng)答消息{Auth3,Auth4,T2}，以猜解密合法用戶的密碼PWi或唯一標(biāo)識usernamei。攻擊者J無法生成有效的PWi和usernamei。首先，參數(shù){usernamei,PWi,R1,R2,V}是不可知的，因為這些參數(shù)既未傳輸過，也未保存在智能卡中。其次，安全參數(shù)通過不可逆單向散列函數(shù)h(·)進(jìn)行了加密。

2.1.4抵御會話密鑰泄漏攻擊

本文方案能抵御會話密鑰泄漏攻擊。假定攻擊者J偵聽到正在進(jìn)行的通信，并記錄下登錄消息{MIDi′,Auth1,Auth2,T1}、認(rèn)證請求{Auth3,Auth4,T2}和應(yīng)答{AuthSKey,T3}。首先，J無法從AuthSKey中提取SKey，因為AuthSKey受抗碰撞單向散列函數(shù)h(·)的保護(hù)。其次，為成功生成SKey，SKey=h(MIDi‖R2′‖R3‖T1‖T2)，J必須具有唯一標(biāo)識usernamei、PWi、隨機(jī)新鮮值R2′和R3的知識。參數(shù)usernamei和PWi從未傳輸過，且通過單向散列函數(shù)h(·)進(jìn)行了加密，不會被攻擊者所提取。

2.1.5抵御內(nèi)部者攻擊

本文方案能抵御內(nèi)部者攻擊。假定攻擊者J在服務(wù)器SR處獲得了掩藏表示MIDi。Ui的唯一標(biāo)識通過隨機(jī)新鮮值進(jìn)行過散列，即注冊階段中MIDi=h(R1‖usernamei)。由于散列函數(shù)不可逆，J無法成功推導(dǎo)出標(biāo)識usernamei和R1，無法從散列值中解密出信息。此外，無法使用MIDi生成認(rèn)證階段中的任何參數(shù)。

2.1.6抵御拒絕服務(wù)攻擊

本文方案可抵御拒絕服務(wù)攻擊。其中，遠(yuǎn)程服務(wù)器會認(rèn)證用戶的usernamei和密碼PWi的真實性。此外，本文方案使用了時間戳。

2.1.7抵御失竊智能卡攻擊

本文方案可抵御失竊智能卡攻擊。智能卡SC保存參數(shù){Zi,Ai,Bi,h(·)}。假定攻擊者J成功竊取智能卡，并嘗試提交有效登錄請求{MIDi′,Auth1,Auth2,T1}。為此，J必須成功計算MVi=h(MIDi‖V)、Auth1=h(R2‖MVi′ ‖T1)、Auth2=h(MIDi′ ‖MVi′ ‖T1)⊕R2。為計算這些參數(shù)，J需要得到標(biāo)識usernamei、密碼PWi、MVi′、服務(wù)器私鑰V和MPWi。這些參數(shù)并未保存在智能卡中。因此，即使攻擊者竊得智能卡，也無法成功計算出這些參數(shù)。

2.1.8抵御服務(wù)器欺騙攻擊

本文方案可抵御服務(wù)器欺騙攻擊。為了假冒認(rèn)證服務(wù)器SR，攻擊者J嘗試對服務(wù)器發(fā)送的有效應(yīng)答消息{Auth3,Auth4,T2}進(jìn)行偽造。為生成有效消息，J必須擁有服務(wù)器私鑰V、用戶標(biāo)識usernamei、掩藏密碼MPWi的知識，以成功計算出Auth3、Auth4，因為Auth3=R2′⊕R3、Auth4=h(SKey‖MVi′‖R3‖T1‖R2‖T2)、MVi′ =h(MIDi′ ‖V)、R2′ =Auth2⊕h(MIDi′ ‖MVi′ ‖T1)這些參數(shù)從未傳輸過。因此，攻擊者J無法生成合法應(yīng)答消息。

2.1.9抵御并行會話攻擊

本文方案可抵御并行會話攻擊。假定攻擊者J攔截到之前會話中傳輸?shù)牡卿浾埱笙MIDi′,Auth1,Auth2,T1}，并再次發(fā)送該消息。由于本文方案使用了時間戳，每次會話中時間戳均是不同的。因此竊聽到的消息在另一次會話中是無效的。

2.1.10用戶匿名性

本文方案能確保用戶匿名性。竊聽者試圖偵聽用戶與遠(yuǎn)程服務(wù)器之間正在進(jìn)行的消息交換。必須保證用戶標(biāo)識不被竊聽者所獲取。本文方案采用了具有隨機(jī)性的掩藏標(biāo)識MIDi。首先，用戶標(biāo)識usernamei從未傳輸過。因此，竊聽者無法得到唯一標(biāo)識。即使竊聽者得到了MIDi，其也無法由此解密其他消息，因為認(rèn)證參數(shù)均未使用MIDi。其次，所有參數(shù)均使用單向散列函數(shù)h(·)保護(hù)，攻擊者無法檢索到任何信息。此外，用戶標(biāo)識與隨機(jī)新鮮值相關(guān)聯(lián)，使其在每次會話中均具有唯一性。

2.2 安全性的形式化認(rèn)證

本文使用互聯(lián)網(wǎng)安全協(xié)議和應(yīng)用的自動化認(rèn)證[13](Automated Validation of Internet Security Protocols and Applications, AVISPA)對本文方案進(jìn)行形式化安全分析。結(jié)果表明，本文方案足夠安全。

2.2.1AVISPA概述

AVISPA是安全驗證工具，以高級協(xié)議規(guī)范語言[14](High Level Protocol Specification Language, HLPSL)編寫要執(zhí)行的代碼，AVISPA工具為每個參與者提供角色模型，每個角色均獨(dú)立于其他角色。使用AVISPA進(jìn)行方案檢驗需要執(zhí)行以下步驟：

步驟1首先，以HLPSL語言編寫方案。

步驟2使用HLPSL2IF翻譯工具將HLPSL代碼自動轉(zhuǎn)換為中間格式(Intermediate Format，IF)。

步驟3將IF規(guī)范輸入到后端。

執(zhí)行IF后，后端通過分析輸出格式(Output Format，OF)展示仿真結(jié)果，表明方案是否安全。后端還會確認(rèn)方案的安全屬性，例如抵御重放攻擊、身份認(rèn)證和密鑰保密性等。

2.2.2本文方案在HLPSL代碼中的規(guī)范

本文方案中存在兩個基本角色，用戶Ui和服務(wù)器SR。首先，在注冊階段，用戶Ui將注冊請求消息{MVi}傳遞至服務(wù)器SR。通過SND()和對稱密鑰SyKus發(fā)送該請求。在保密聲明中，username為保密參數(shù)，僅為用戶所知。啟動器(用戶Ui)角色的HLPSL規(guī)范如代碼1所示。用戶Ui使用RCV()和對稱密鑰SyKus，接收包含參數(shù){MVi′}的智能卡。其后，用戶接收來自SR的認(rèn)證應(yīng)答消息RCV({Auth3′.Auth4′.T2′}_SyKus)。在成功通過認(rèn)證后，用戶生成會話密鑰：Skey′ :=h(MIDi′.R2′.R3′.T1′.T2′)。為認(rèn)證生成的會話密鑰，用戶生成：AuthSkey′ :=h(Skey′.MVi′.MIDi′.T2′.T3′)。并將其發(fā)送至服務(wù)器。

代碼1用戶的角色規(guī)范

role user(Ui, SR:agent,

%Ui使用戶, SR是服務(wù)器

h:hash_func,

SyKus:symmetric_key,

SND,RCV:channel(dy))

played_by Ui

def=

Local State:nat,

username, PWi, M, MVi, U, V, MIDi, MPWi:text,

Zi, Ai, Bi, Auth1, Auth2, Auth3, Auth4:text,

R1,R2,R3,T1,T2,T3,P,Q,Skey,AuthSkey:text

Mu:hash_func

const alice_bob_r2, alice_bob_t1, alice_bob_t3,

alice_bob_t2,bob_alice_r3

subs1, subs2, subs3: protocol_id

init State :=0

transition

1. State=0∧RCV(start)=|>

State′:=1∧R1′:=new()

∧MIDi′:=h(R1′.username)

∧SND({MIDi′}_SyKus)

∧secret({username},sub1,Ui)

%從服務(wù)器安全接收智能卡SC

2. State=1∧RCV({MVi′.Mu(P′.Q′).U′}_SyKus)=|>

%登錄和身份驗證階段

State′:=2∧secret({V′,P′,Q′},sub2,{SR})

∧MPWi′:=h(R1’,PWi)

∧PVi′:=xor(h(MID′.V),h(username.MPWi′))

∧R2′:=new()

∧T1′:=new()

∧Auth1′:=h(R2′.MVi.T1)

∧Auth2′:=xor(h(MIDi′.MVi′.T1′),R2′)

%向服務(wù)器發(fā)送登錄請求消息{MIDi′, Auth1, Auth2, T1}

∧SND({MIDi′.Auth1′Auth2′.T1′}_SyKus)

∧witness(Ui,SR,alice_bob_r2,R2′)

∧witness(Ui,SR,alice_bob_t1,T1′)

%從服務(wù)器中接受身份驗證信息{Auth3, Auth4,T2}

3. State=2∧RCV({Auth3′.Auth4′,T2′}_SyKus)=|>

State′:=3∧T3′:=new()

∧Skey′:=h(MIDi′.R2′.R3′.T1′.T3′)

∧SND({AuthSkey′.T3}_SyKus)

∧witness(Ui,SR,alice_bob_t3,T3′)

∧request(SR,Ui,bob_alice_t2,T2′)

∧request(SR,Ui,bob_alice_r2,R2′)

end role

服務(wù)器SR的角色的HLPSL規(guī)范如代碼2所示。遠(yuǎn)程服務(wù)器通過RCV({MID′}_SyKus)接收用戶發(fā)送的注冊請求消息。SR向用戶發(fā)放智能卡。SR接收來自用戶的登錄請求消息{MID′,Auth1′,Auth2′,T1′}并認(rèn)證該請求。SR計算參數(shù){Auth4′,Auth5′,T2′}，并通過SND和對稱密鑰SyKus將該參數(shù)提交至用戶。SR生成會話密鑰并進(jìn)行認(rèn)證。

代碼2服務(wù)器的角色規(guī)范

role user(Ui, SR:agent,

%Ui使用戶, SR是服務(wù)器

h:hash_func,

SyKus:symmetric_key,

SND,RCV:channel(dy))

played_by SR

def=

Local State:nat,

username, PWi, M, MVi, U, V, MIDi, MPWi:text,

Zi, Ai, Bi, Auth1, Auth2, Auth3, Auth4:text,

R1,R2,R3,T1,T2,T3,P,Q,Skey,AuthSkey:text

Mu:hash_func

const alice_bob_r2, alice_bob_t1, alice_bob_t3,

alice_bob_t2,bob_alice_r3

subs1, subs2, subs3: protocol_id

init State :=0

Transition

%從用戶信息中接受登記信息

1. State=0∧RCV({MID}′_SyKus)=|>

State′:=1∧P′:=new()

∧Q′:=new()

∧U′:=new()

∧V′:=inv(U′)

∧MVi′:=h(h(R1′.username).V′)

∧SND({MIDi′}_SyKus)

%接收智能卡給用戶

∧secret({username},sub3,Ui)

∧secret({V′,P′,Q′},sub2,{SR})

%登錄和身份驗證階段

2. State=1∧RCV({MIDi′.Auth′, Auth2′, T1′}_SyKus)=|>

State′:=2∧R2′:=new()

∧R3′:=new()

∧T2′:=new()

∧R2′:=xor(Auth2′,h(MID′,MVi′,T1′))

∧Auth3′:=xor(R2′,R3′)

∧Skey′:=h(MIDi′.R2′.R3′.T1′.T2′)

∧Auth4′:=h(Skey′.MVi.R3′.T1′.R2′.T2′)

∧SND({Auth3’.Auth4’.T2’}_SyKus)

%發(fā)送身份驗證反饋信息給用戶

∧witness(SR,Ui,bob_alice_t2,T2′)

∧witness(SR,Ui,bob_alice_r3,R3′)

3. State=2∧RCV({AuthSkey′.T3′}_SyKus)=|>

State′:=3∧AuthSkey′:=h(Skey′.MVi.MIDi′.T2′.T3′)

∧request(Ui,SR, alice_bob_t1,T1′)

∧request(Ui,SR, alice_bob_t2,R1′)

∧request(Ui,SR, alice_bob_t3,T3′)

end role

2.2.3模擬結(jié)果

模擬所得結(jié)果如圖2所示，其中：CL-AtSe和OFMC是后端分析工具，分析狀態(tài)數(shù)為7個；可到達(dá)狀態(tài)數(shù)為7個；轉(zhuǎn)換耗時為0.17 s；計算時間為0.01 s；解析時間為0.01 s；搜索時間為0.14 s；訪問節(jié)點數(shù)為52個；深度為7層。結(jié)果證明本文方案可抵御所有積極和消極攻擊。生成的輸出包括以下部分：

SUMMARY：描述協(xié)議是否安全(SAFE，UNSAFE)或不確定(INCONCLUSIVE)。

DETAILS：描述本文方案的分析，例如方案是否被發(fā)現(xiàn)易于受到任何攻擊、分析中采用的模型、分析未得到確定結(jié)果的原因等。

PROTOCOL：描述方案名稱。

GOAL：描述分析目標(biāo)。

BACKEND：描述使用了哪個后端。

STATISTICS：描述后端執(zhí)行方案所耗時間。

ATTACK TRACE：描述攻擊入侵方案的方式(若存在)。

圖2 本文案例的模擬結(jié)果

3 性能比較

本節(jié)將比較本文方案與其他方案的計算成本，其中：TH表示執(zhí)行散列運(yùn)算的計算復(fù)雜度；TE表示執(zhí)行指數(shù)函數(shù)的計算復(fù)雜度；TM表示執(zhí)行乘法/除法函數(shù)的計算復(fù)雜度；TS表示執(zhí)行對稱加密/解密函數(shù)的計算復(fù)雜度。

各方案在計算復(fù)雜度上的比較如表2所示。由表2可發(fā)現(xiàn)，本文方案效率最高。因為本文方案足夠輕量級，僅使用XOR和單向散列運(yùn)算，單向散列運(yùn)算的計算成本可忽略不計。其他方案采用的加密/解密運(yùn)算的計算成本比散列運(yùn)算高得多。各方案的安全特征比較分析如表3所示。

表2 計算復(fù)雜度比較

表3 各方案的安全性比較

文獻(xiàn)[4]對很多攻擊的抵御性有所提高，但不提供智能卡撤銷操作，無法抵御隱藏服務(wù)器攻擊，但包含了大量的指數(shù)運(yùn)算，計算開銷較大。文獻(xiàn)[5]是一種多因子的解決方案，包含密碼、生物特征和智能卡，其主要面向遠(yuǎn)程醫(yī)療解決方案，該方案無法抵御內(nèi)部特權(quán)攻擊，需要較多的指數(shù)運(yùn)算和非對稱密碼運(yùn)算，尤其在身份認(rèn)證階段需要較多的計算開銷。文獻(xiàn)[8]由于其固有設(shè)計，無法抵御如隱藏服務(wù)器攻擊、服務(wù)器欺騙攻擊、密碼猜測攻擊等攻擊。由于該方案使用單向散列函數(shù)、XOR和Concat操作，這些運(yùn)算大多屬于輕量級，因此總體開銷與其他方案比較，屬于中等。本文方案滿足眾多安全要求，可抵御很多已知安全威脅。由表2和表3可知本文方案的綜合性能最高。

4 結(jié) 語

在基于云計算的物聯(lián)網(wǎng)架構(gòu)，多個IoT網(wǎng)絡(luò)連接至云服務(wù)器，由此支持遠(yuǎn)程用戶訪問IoT網(wǎng)絡(luò)生成的數(shù)據(jù)。在此基礎(chǔ)上，本文提出多因子智能卡的輕量級遠(yuǎn)程用戶身份認(rèn)證方案。嚴(yán)格的安全分析表明，本文方案能夠抵御多種網(wǎng)絡(luò)攻擊。在AVISPA中進(jìn)行了模擬，證明了本文方案的安全性。性能評價結(jié)果表明，本文方案的安全性優(yōu)于其他相關(guān)方案。