呂 良 李 瑞
(1.公安部第三研究所 上海 201204)
(2.華北電力大學 北京 102206)
近年來,黑客技術的發展使得信息化建設日益深入各類企業深陷網絡安全的風險之中,據統計絕大多數的安全事件都是由終端設備的非法接入內網引起。另一方面,軍工產業、政府部門、金融等領域相對系統復雜,保密性強,對內部網絡安全可靠性有著嚴格需求。為了保障網絡內部的安全可信,落實信息安全等級保護安全建設,終端安全接入技術應運而生。企業在應對網絡安全風險和安全威脅時,不僅需要自上而下的信息安全管理體系,還需要自下而上的保證終端用戶安全接入的認證協議,使接入企業內部網絡的終端成為一個可信終端。
本文針對目前終端接入面臨的安全風險和安全接入需求,提出一種基于SM2的雙向認證密鑰協商協議,分析其安全性,采用BAN邏輯進行形式化分析,最后給出安全性分析結果。
數字簽名是指發送方用自己的私鑰對數字指紋進行加密后所得的數據,其中包括非對稱密鑰加密和數字簽名兩個過程,在可以給數據加密的同時,也可用于接收方驗證發送方身份的合法性。采用數字簽名時,接收方需要使用發送方的公鑰才能解開數字簽名得到數字指紋。
數字指紋又稱為信息摘要,是指發送方通過HASH算法對明文信息計算后得出的數據。采用數字指紋時,發送方會對明文進行哈希運算后生成的數字指紋(還要經過數字簽名),以及采用對端公鑰對明文進行加密后生成的密文一起發送給接收方,接收方用同樣的HASH算法對明文計算生成的數據指紋,與收到的數字指紋進行匹配,如果一致,便可確定明文信息沒有被篡改。從以上數字簽名的加/解密過程中可以看出,數字簽名技術不但證明了信息未被篡改,還證明了發送方的身份。
國家密碼管理局在2010年12月份公布了《SM2橢圓曲線公鑰密碼算法》,SM2算法屬于橢圓曲線算法(ECC)當中的一種?!禨M2橢圓曲線公鑰密碼算法》說明了簽名驗簽、加密解密和密鑰交換算法的具體步驟。本論文參照《SM2橢圓曲線公鑰密碼算法》第三部分中的密鑰交換協議。考慮到終端設備的內存空間和性能的限制性,本文在應用SM2密鑰協商時省略了算法中的可選步驟,并與基于數字證書的雙向身份認證相結合,其安全性不會降低。
本文利用數字簽名技術,在SM2密鑰協商過程中實現了用戶A和用戶B的雙向身份認證,認證通過后得到雙方的會話密鑰。該協議適用于智能終端安全接入通信系統。用戶A和用戶B之間的認證協商過程如圖1所示。以下用到的符號做以下說明,如表1所示。

表1 認證協商通信符號說明
設用戶B和用戶A之間通過密鑰協商獲得的密鑰長度為LK,用戶A作為發起者,去連接用戶B,用戶B作為響應者。
用戶A:
步驟1:隨機產生隨機數rA,本次會話唯一標識rB,身份唯一標識IDA。
用戶B:
步驟2:隨機產生隨機數rB,身份唯一標識IDB。
用戶A:
用戶B:
步驟4:計算H(rA||Se||IDA),計算,如果得到結果為true,用戶B認證用戶A成功,到步驟5,如果得到結果為false,用戶B立即中斷與用戶A的連接。
用戶A:
步驟7:計算H(rB||Se||IDB),計算,如果得到結果為true,用戶A認證用戶B成功,至此用戶B和用戶A完成雙向認證,如果得到結果為false,用戶B立即中斷與用戶A的連接。
用戶B和用戶A完成雙向認證之后,進行以下密鑰協商過程。
用戶A:
步驟8:選擇橢圓曲線上一點A=(xA,yA),點A滿足橢圓曲線方程,是非無窮遠點。
用戶B:
步驟9:選擇橢圓曲線上一點B=(xB,yB),點B滿足橢圓曲線方程,是非無窮遠點。
步驟10:取出點B中的域元素,將其數據類型轉化為整數型,并計算,其中

圖1 認證協商過程圖
步驟12:取出點A中的域元素,將其數據類型轉化為整數型,并計算,其中
步驟14:計算KB=KDF(xV||yV||ZA||ZB||rA||rB,Lk)
用戶A:
步驟15:取出點A中的域元素,將其數據類型轉化為整數型,并計算,其中
步驟17:取出點B中的域元素,將其數據類型轉化為整數型,并計算,其中
步驟19:KA=KDF(xU||yU||ZA||ZB||rA||rB,Lk)。
步驟20:計算RA=rA?rB,將RA發送給用戶B。
用戶B:
步驟21:計算RB=rA?rB,計算,如果結果為false,協商失敗,立即中斷與用戶A的通信連接,如果結果為true,至此用戶A和用戶B密鑰協商成功,雙方分別得到接下來進行數據傳輸的會話密鑰KB=KA。
BAN邏輯語法具體說明如下:
1)P|≡X:P相信X,主體P相信X是真的。
2)P|:X:P曾說過X,主體P在某個時刻傳送X。
3)P<X:P曾看到過X,有主體曾發送過來包含X的信息,主體P可以讀出X。
4)#(X):X是新鮮的。
5){X}K:用密鑰K加密X得到的密文。
BAN主要推理規則如下。
1)消息含義規則

2)臨時值驗證規則

3)新鮮性規則

4)會話密鑰規則

使用BAN邏輯證明本文設計協議的安全性,形式化說明協議能夠達到預期安全目標。先根據BAN邏輯需求對協議步驟進行表示如下。


假設:A|≡#(rB),A|≡#(IDB),B|≡#(rA),B|≡#(IDA) ;需證明:1)A|≡#(K);2)B|≡#(K);3)A|≡
證明過程如下:
1)因A|≡#(rB),A|≡#(IDB),結合新鮮性規則,可得A|≡#(H(rB,Se,IDB)),再可得A|≡#{rB,Se,IDB},再可得A|≡#K。
2)因B≡#(rA),B|≡#(IDA),結合新鮮性規則,可得B|≡#(H(rA,Se,IDA)),再可得B|≡#{rA,Se,IDA},再可得B|≡#K。
因A|≡ #(H(rB,Se,IDB))?A|≡B|~(H(rB,Se,IDB)),結合臨時值校驗規則,可得A|≡B|≡(H(rB,Se,IDB))。
因A|≡#K?A|≡B|≡(H(rB,Se,IDB)),結合會話密鑰規則,可得A|≡
因B|≡ #(H(rA,Se,IDA))?B|≡A|~(H(rA,Se,IDA)),結合臨時值校驗規則,可得B|≡A|≡(H(rA,Se,IDA))。
因B|≡#K?B|≡A|≡(H(rA,Se,IDA)),結合會話密鑰規則,可得
綜上,可證明本文方案可以到達預期認證協商目標,本文協議是安全的。
在所提出的方案中,用戶的私鑰由用戶持有的安全芯片內的隨機數發生器生成。它存儲在安全芯片的存儲單元中,無法導出。受信任的第三方CA通過PKI技術發布用戶的簽名證書。證書包括用戶的公鑰。,只有合法用戶才能擁有與簽名公鑰對應的正確簽名私鑰。用戶A確定(rA||Se||IDA),發送給用戶B。用戶B通過驗證認證用戶A的身份,其中用戶B的運算涉及用戶A的公鑰。如果返回的結果為true,則表明消息的確由持有私鑰dA的合法用戶A發送的。同樣地,用戶A通過計算認證用戶B。因此,用戶A和用戶B之間實現了雙向身份認證。
用戶A發送給用戶B的認證請求中包含隨機數rA,其消息為即由密文傳輸。因此,如果攻擊者δ重放一條之前來自于用戶A的消息給用戶B,用戶B能夠通過計算驗證隨機數rA的新鮮性。因此,即使攻擊者δ發送相同的消息給B,通過B驗證隨機數的新鮮性確定其為非法用戶。因此提出的協議可以防止重放攻擊。
雙方用戶不僅可以相互進行雙向身份認證,也能確認其消息的發送者。在提出的協議中,用戶B會驗證,如果驗證計算返回結果為true,消息被確認為由合法用戶A發送的。否則,則可能發生了假冒攻擊。由于安全模型提出CA是可信的第三方,僅有合法用戶才能得到數字簽名公鑰。因此攻擊者δ無法利用假冒攻擊通過所提出協議的認證階段。
我們提出的協議在密鑰協商和認證之后,在雙方之間發送的傳輸數據上提供加密信道。只有達到身份驗證和密鑰協議的用戶才知道會話密鑰。攻擊者δ無法獲取共享會話密鑰。由于無法使用共享會話密鑰無法正確解密網絡數據包,因此無法注入惡意信息。如果發送由用戶A或用戶B加密的惡意數據,用戶B或用戶A將無法使用正確的共享會話密鑰正確解密惡意數據,并且丟棄錯誤數據。
攻擊者δ截取來自用戶A的消息。由于攻擊者δ無法得到用戶B的私鑰,所以即使截獲此消息也無法獲得(rA||Se||IDA),即不能對用戶B做出正確的回應消息。同樣,攻擊者δ也無法對用戶A做出正確的回應。因此,提出的協議可以抵抗中間人攻擊。
假設攻擊者δ執行暴力攻擊或離線字典攻擊以破解共享會話密鑰。由于相互認證的粒度,密鑰協議發生在每個TCP連接上。該協議在每次通信結束后判斷連接是否超時。超時的話,重新啟動密鑰協議和相互身份驗證以獲取新的共享會話密鑰。由于共享會話密鑰在短時間內更新,攻擊者δ無法獲得新的會話密鑰。因此一旦共享會話密鑰生效,攻擊者就無法在使用所提出的協議的通信雙方之間的會話上長時間竊聽。
用于生成密鑰的元素一次更改一個,并且不能生成其他密鑰,一個密鑰被破解,不會影響其他密鑰的安全性,提出的協議具有的這種特性,稱為完全前向保密(PFS)。認證協商協議將根據雙方提供的隨機數定期創建新密鑰。由于雙方都提供了只有在密鑰協議時才知道的隨機值,因此生成的每個新密鑰與先前創建的密鑰不同。即使對手截獲密鑰,它也不能長時間使用攔截的密鑰。此外,由于未通過密鑰協議獲得新密鑰,因此必須啟動新的暴力計算以獲取正在使用的密鑰。因此,攻擊者獲得會話密鑰很困難。
針對現有企業終端接入內網面臨的主要安全問題,本文結合數字簽名和SM2算法,設計了一種基于數字簽名和SM2的雙向認證協商協議,并給出了正確性證明。最后經過安全性分析,證明本文協議在抵抗消息注入攻擊、重放攻擊、中間人攻擊、竊聽攻擊、假冒攻擊等攻擊手段方面具有優勢。