一種改進的NSSK認證協議及其實現方法

于金剛,趙治剛

(中國科學院大學,北京 100049)

1 引 言

在網絡通訊產品如網絡電話、實時消息系統等大力發展的今天,眾多相關開源軟件的出現降低了實現該類系統的困難,如實現了SIP協議的Linphone、PJSIP等;實現了MQTT協議的Mosquitto等.但此類開源軟件只提供了簡單的本地信息加解密功能,無法完成會話中通信雙方身份的認證和共享密鑰的生成與分發,使得該類開源軟件不能更好地服務于安全性要求較高的領域.本文在深入分析著名的認證協議Needham-Schroeder(NS)協議的基礎上,設計了一種優化和改進版的認證協議[4,5],目的在于避免原始協議存在的各種缺陷,并在不增加信息交換次數的基礎上提供身份認證和共享會話密鑰服務.

為確保改進版認證協議的可靠性,必須對改進協議進行形式化分析驗證.BAN邏輯是迄今使用最廣泛的認證協議形式化分析方法[6].故本文通過BAN邏輯對改進協議進行形式化驗證.在確保改進版協議安全、可靠的基礎上,借助于硬件TF加密卡及其對應的SDK工具包,實現了改進版協議的身份認證功能和共享密鑰分發功能.通過修改開源軟件Mosquitto消息通信部分的源碼,在消息通信前后調用SDK提供的相關接口,對修改后的源碼重新編譯,從而在應用中達到安全通信的目標.

2 NS協議分析

R.M.Needham和M.D.Schoreder于1978年首次提出了利用加密技術設計認證密鑰分配協議[3](簡稱NS協議),NS協議的運行原理共5步如下:

1.A→S:A、B、NA

2.S→A:(NA、B、KAB、(KAB、A)KBS)KAS

3.A→B:(KAB、A)KBS

4.B→A:(NB)KAB

5.A→B:(NB-1)KAB

前3條消息是在密鑰分發中心S的幫助下,完成共享密鑰KAB的分配,后2條消息是為了確認雙方已經收到共享密鑰,并且可以進行正常通信.但存在不能使B相信消息3的新鮮性的缺陷及消息4只攜帶接收方的隨機數,無法使發送方A識別接收方的身份的不足.

以下描述了原生NS協議存在的a、b兩種缺陷以及在改進協議中避免缺陷所采取的措施:

a.存在接收方無法識別重放消息的缺陷,攻擊如下:

1.A→S:A、B、NA

2.S→A:(NA、B、KAB、(KAB、A)KBS)KAS

為保證消息新鮮性和防止重放攻擊,本協議中采取的措施是:在圖1第2次交互中,由接收方B給密鑰分發中心發送隨機數NB,在第3次交互密鑰分發中心返回給B的消息中,解密出隨機數NB,保證該消息的新鮮性,從而避免重放舊消息.發送方A驗證消息新鮮性的原理相同.相比于現有的防止重放攻擊的方案,本改進版的認證協議在沒有增加協議執行步驟數的基礎上,確保了發送方A和接收方B都可以在保證消息新鮮性的同時避免攻擊者使用舊消息進行重放攻擊.

b.存在接收方身份被冒充的缺陷,攻擊如下:

1.A→S:A、B、NA

2.S→A:(NA、B、KAB、(KAB、A)KBS)KAS

3.A→I(B):(KAB、A)KBS

4.I(B)→A:NI

其中消息1、2屬于原始NS協議的正常通信,消息3被身份冒充者I攔截,因為原始協議消息4中沒有發送方A的身份標示,故I將一個與原始消息(NB)KAB格式相同的NI發給發送方A,發送方A對消息NI使用共享密鑰KAB解密,對所得結果進行函數操作,使用共享密鑰KAB加密后發送給B,同時消息5也被I截獲,但是發送方A認為接收方B已經接收共享密鑰KAB并且能夠正常通話.

為了避免身份冒充,本協議中使用的方式是:

在圖1的第3次交互中,在密鑰分發中心發送給發送方A的消息中,添加接收方的身份標示B,保證本次會話的接收方為用戶B,由此當接收方B轉發后,發送方A解密、驗簽消息,可以對本次會話的接收方B進行身份確認,從而避免了身份冒充.

3 改進版認證協議的設計

改進版的認證協議采用非對稱加密方式制定,主要完成身份認證和獲取共享的共享密鑰兩項功能.在網絡通信中,首先要完成通信雙方的身份認證,以及雙方各自對密鑰分發中心的身份認證,才能進一步進行通話;其次通過密鑰分發中心生成共享密鑰,保證一次一密,即保證每次通話的共享密鑰都是新的[9].

在原始NS協議的基礎上,改進版的認證協議增加接收方發送隨機數給密鑰分發中心的過程,并在密鑰分發中心生成的消息中添加發送方和接收方的隨機數及其對應的身份標示,達到確保消息新鮮性的同時完成對密鑰分發中心身份認證的目的[8];將使用共享密鑰加密后的發送方的隨機數添加到接收方發送給發送方的消息中,以便使發送方在完成消息新鮮性驗證的同時,確保接收方已經收到共享密鑰.

改進版的認證協議交互過程如圖1所示.

圖1 改進的認證協議運行原理圖Fig.1 Improved protocol operation diagram

協議的運行步驟描述如下:

1.A→B:A、B、((NA)KSA)KPS

2.B→S:A、B、(((NA)KSA)KPS、(NB)KSB)KPS

3.S→B:((((NA、B、KAB、NB)KSS)KPA,NB、A、KAB、NA)KSS)KPB

4.B→A:(((NA、B、KAB、NB)KSS)KPA,(NA)KAB

5.A→B:(NB-1)KAB

詳細描述如下:

步驟1.發送方A將其名稱A、接收方名稱B以及使用它的私鑰KSA簽名并使用密鑰分發中心S的公鑰KPS加密的隨機數NA發送給接收方B.

步驟2.接收方B將收到的消息,添加B的隨機數NB后,使用自身的私鑰KSB簽名NB并使用S的公鑰加密全部消息后,發送給S.

步驟3.S用自身私鑰和通信雙方各自公鑰解密消息,提取NA和NB,并生成共享密鑰KAB.用自身私鑰KSS對發送方A的隨機數NA,接收方名稱B,共享密鑰KAB及接收方隨機數NB簽名并使用發送方A的公鑰KPA加密.之后用自身私鑰KSS對上一步的密文與接收方B的隨機數NB,發送方的名稱A,共享密鑰KAB,發送方的隨機數NA整體簽名并使用接收方B的公鑰KPB加密,發送給B.

步驟4.B用自身私鑰和S公鑰解密消息,提取共享密鑰KAB以及NB,完成對消息新鮮性驗證以及對S的身份驗證及發送方的身份驗證.使用共享密鑰KAB對提取的發送方A的隨機數NA加密,與S發送給A的消息一起發送給A.

步驟5.A首先用自身私鑰及S的公鑰解密S發送給其的消息,提取隨機數NA,完成對消息的新鮮性和S的身份認證及對接收方B身份的確認.提取共享密鑰KAB,解密接收方B加密的隨機數NA,并驗證B已經接收到共享密鑰KAB.之后使用共享密鑰KAB加密隨機數NB-1(使用與B商定的函數對NB進行操作),發送給B.B接收到消息后,使用共享密鑰KAB解密消息,使用與A商定的函數對信息進行反操作,提取隨機數NB,驗證A已經收到共享密鑰KAB.

4 改進版認證協議的形式化驗證

本文使用基于信念的模態邏輯BAN邏輯對改進協議進行形式化驗證[2],以保證該認證協議可以達到安全目標(機密性、認證性、不可否認性、完整性)[7].其驗證流程如圖2所示.

圖2 BAN邏輯驗證流程圖Fig.2 Flow diagram of BAN logic

上圖對應的驗證步驟如下:

1.需要將待分析協議理想化建模,使用BAN邏輯可以識別的公式描述協議.

2.規定使協議安全運行的初始假設集.

3.用BAN邏輯規則,通過理想化模型和假設集合進行推理演算,得到協議運行的結果集.

4.通過分析結果集來判定協議是否達到設計目標.

其中1、2對協議的分析非常重要,為了確保其正確性,在理想化建模和規定初始假設集時,使用文獻[5]中提供的改進方法,保證理想化建模過程和初始假設集合的規范性.本次驗證過程用到的推理規則包括:消息含義規則、臨時值驗證規則、管轄規則、消息新鮮性規則、信念規則.

4.1 對改進的認證協議進行理想化建模

去掉第一步發送的消息,因為其只是由接收方B進行轉發,與分析論證無關.得理想化模型如下:

(P1)B→S:((((NA)KSA)KPS,NB)KSB)KPS

(P2)S→B:

(P3)B→A:

4.2 建立初始假設集合

假設1至5明顯成立,因為KPS、KPB、KPA分別為公鑰,由不可偽造的證書對其進行證明,故可信;KAB是由S生成的密鑰,所以S必定對其信任;6、7假設,說明A、B信任密鑰分發中心對共享密鑰KAB擁有管轄權;8、9、10說明A、B、S分別信任自己生成的隨機數是新鮮性;11、12說明A、B分別信任S對新的共享密鑰有管轄權.

4.3 形式化驗證

利用初始假設和推理規則對協議進行進行形式化驗證過程如下:

由理想模型(P1)S收到消息:

S?((((NA)KSA)KPS,NB)KSB)KPS

(1)

由初始假設3、4和消息含義規則有:

S|≡A|～NA

(2)

S|≡B|～NB

(3)

由理想模型(p2)B收到消息:

(4)

由初始假設2和消息含義規則有:

(5)

由初始假設9和式(5)以及消息新鮮性規則、臨時值驗證規則、和信念規則有:

(6)

(7)

通過初始假設7和式(6),初始假設12和式(7)分別使用管轄規則得:

(8)

(9)

由理想模型(p3)A收到消息:

(10)

由初始假設1和式(10),使用消息含義規則有:

(11)

由初始假設1和式(11),使用新鮮性規則、臨時值驗證規則及信念規則有:

(12)

(13)

由初始假設6、11和管轄規則有:

(14)

(15)

對于消息后半部分使用共享密鑰KAB加密的內容,由式(10)、(14)及消息含義規則有:

(16)

由式(15),使用消息新鮮性規則、臨時值驗證規則、信念規則有:

(17)

由理想模型(P4)B收到消息:

(18)

由式(8)及消息含義規則得:

(19)

由初始假設9或時(9)及式(19)和臨時值驗證規則、消息新鮮性規則及信念邏輯規則有:

(20)

協議的最終推理結果集合為:

4.4 驗證結果

由以上推理過程和結果集合可知,通信雙方分別完成對對方身份的認證,認證過程中的消息是新鮮的;同時通信雙方都得到共享密鑰KAB并且驗證對方也收到了該共享密鑰,同時認證了該共享密鑰的新鮮性.故該改進協議是安全、可靠的.

5 改進版協議的實現

本文中改進版協議的實現,借助于硬件TF加密卡以及封裝了TF加密卡硬件接口的SDK工具包.該加密卡用硬件的方式實現了國標非對稱加密算法SM2和對稱加密算法SM4及摘要生成算法SM3,并提供證書的存儲、密鑰的生成、驗簽和加解密等功能.通過調用SDK接口,實現TF卡激活、安全登錄、證書上傳、身份認證、獲取對端證書、獲取共享密鑰、通信內容加解密等功能,SDK對上層應用屏蔽了具體的實現細節.

在TF加密卡基礎上的加密通信圖見圖3.

在加密通信前,通信雙方首先要初始化TF加密卡、在業務服務器和密鑰分發中心進行注冊(或登錄)、將本端證書上傳至密鑰分發中心、獲取聯系人證書等操作.完成以上操作需要調用的接口及對應接口說明如下:

1.setPin(pin p):當遇到更換TF卡、終端開機、重啟的情況,需要調用該接口登陸TF加密卡,使用pin碼作為參數,完成TF加密卡的初始化.

在TF卡完成初始化的過程中,SDK內部進了設備檢測、激活證書及私鑰、生成隨機數、獲取密鑰分發中心證書、向密鑰分發中心上傳本端證書的操作.

圖3 加密通信圖Fig.3 Encrypted communication diagram

2.loginEnc(sission,SecId,rand,ts,pubs,pric):通過調用該接口,可以對登錄信息使用客戶端私鑰簽名,使用密鑰分發中心公鑰加密生成密文,將密文經由業務服務器轉發給密鑰分發中心,進行登錄驗證.rand為隨機數,ts為時間戳,pubs為密鑰分發中心公鑰,pric為用戶私鑰.密鑰分發中心將驗證結果簽名并加密后,同樣經由業務服務器轉發給客戶端.服務平臺根據返回消息的明文部分,決定業務是否可用,從而完成業務號和唯一標示的綁定,生成token.在登錄成功的同時,會更新聯系人列表,并向密鑰分發中心獲取聯系人證書保存到TF加密卡中.

圖4 登錄界面Fig.4 Login interface

登錄界面及登錄成功后狀態見圖4.

在完成初始化并登陸操作后,發送方再與密鑰分發中心以及接收方進行身份認證、一次一密的加密通信.通過調用SDK的接口,將身份認證的消息使用SM3算法取摘要后再使用SM2算法簽名并加密,通過與密鑰分發中心交互,進行身份認證,并得到一次一密的共享密鑰.使用該共享密鑰加密與聯系人之間的消息,雙方通過業務服務器進行消息通信.

因為純文本消息和文件(圖片、語音、視頻、文件)消息格式的不同,本文采用不同的解決方案,通過調用SDK不同的接口來實現,同時需要業務服務器提供http服務器的功能,以便完成文件的上傳、下載.

為完成上述功能,需要調用的接口及接口解析如下:

1.sessionInit(session,SecId,SecId):發送方A調用該接口,通過業務服務器通知接收方B進行會話初始化.

2.getKey(session,SecId,SecId,Ts):接收方B在收到業務服務器的通知后,調用該接口,完成與密鑰分發中心的通信,密鑰分發中心通過對消息進行解密和驗簽,通過本地SDK接口使得TF卡調用密鑰生成接口生成共享密鑰.使用密鑰分發中心的私鑰簽名及發送方A和接收方B的公鑰分別加密發送給各方的消息,返回給接收方B.接收方B收到消息后,使用公鑰解密私鑰驗簽后,完成對消息新鮮性和密鑰分發中心身份的驗證.

3.putKeyPack(session,ksdata):ksdata為接收方B調用getKey()接口后,返回給發送方A的部分及接收方B使用共享密鑰加密的發送方A的隨機數.通過調用該接口,將該部分發送至發送方A.

4.getKeyPack(session,ksdata):發送方A通過調用該接口,對ksdata使用密鑰分發中心的公鑰解密和己方的私鑰驗簽后,完成對消息新鮮性及密鑰分發中心身份的認證并解密出共享密鑰;使用共享密鑰解密第二部分密文,完成對接收方B的身份認證及確認其收到共享密鑰.

5.putKeyRand(session,ksdata2):ksdata2為發送方A解密出的接收方B的隨機數并使用共享密鑰加密后的消息.

6.getKeyRand(session,ksdata2):接收方B收到消息后,調用該接口解密ksdata2,驗證發送方A也收到共享密鑰.

至此,發送方A和接收方B通過調用SDK相關接口,完成了改進版協議的所有交互過程,并同時完成了身份認證、分別獲取到共享密鑰.雙方在收到共享密鑰的過程中,會將其存儲在TF加密卡中,只在本機內存中存儲會話與密鑰的對應關系,當本次會話結束后,調用接口releaseKey(session)釋放與該會話相關的共享密鑰.

6 改進版協議的應用

為了在實際應用中使用該改進版的認證協議,本文通過修改mosquitto的源碼,在其消息發送部分,調用SDK提供的加解密接口(文本加密接口、文件加密接口),完成消息發送前的加密.對于文本消息直接將密文通過業務服務器發送給接收方;文件則由發送方將其加密后作為附件上傳到http服務器,使用服務器返回的文件標示URI作為文本進行交互.對于文本消息,消息接收方直接調用SDK的文本解密接口[10],可直接完成對文本消息的解密;對于文件信息,根據文件標示URI先從http服務器將加密文件下載到本地,后調用文件解密接口解密.

圖5 本端證書Fig.5 Local certification

圖5展示了改進版的認證協議在即時消息通信中各個環節的使用效果:

TF加密卡初始化之后,本端證書信息:

在完成登錄過程后,通過調用SDK提供的認證接口,完成在加密通信前的身份認證和共享密鑰的獲取.

圖6為雙方本地獲取的共享密鑰信息(密文).

圖6 共享會話密鑰(16進制)Fig.6 Shared session key (Hexadecimal)

使用共享密鑰進行文本消息及文件信息的交互,交互過程中與業務服務器之間的信息都是密文形式:

圖7為消息交互界面.

圖7 消息交互圖Fig.7 Message interaction diagram

圖8為消息(abc)對應密文.

圖8 消息abc對應密文Fig.8 Cphertext of the message abc

圖9 文件發送前內容Fig.9 Cntent of file before sending

使用共享密鑰對文件內容進行加密后,以附件形式通過http協議上傳到業務服務器,發送方將文件描述信息作為本文消息加密發送到接收方,收到文件描述信息解密后,從業務服務器下載密文文件到本地進行解密:

圖9為發送前的文件內容.

圖10 上傳到服務器的文件Fig.10 File uploaded to the server

圖10標示業務服務器已經接收到該文件(圖7中發送的文件名).

7 結束語

本文首先說明制定改進版認證協議的目的,指出原始NS協議存在重放攻擊和身份冒充缺陷;而后說明了改進版認證協議的原理,在不增加信息交互次數的基礎上,改進版協議在使接收方B轉發發送方A加密消息的同時,將自己的隨機數也加密發送給密鑰管理中心,目的在于防止重放攻擊;通過將接收方的名字添加到發送給A的消息中,防止接收方身份的冒充;以及通過共享密鑰KAB加密發送方隨機數NA來保證消息新鮮性的同時驗證了接收方B已經接收到共享密鑰KAB.通過采取以上措施,保證了本協議的可靠性.最后使用BAN邏輯對改進后的協議進行形式化驗證,從理論上證明改進協議完全符合安全協議的要求.在完成協議安全性論證后,借助于封裝了TF加密卡的SDK提供的接口,完成用戶登錄、證書獲取和上傳、身份認證、共享密鑰獲取、文本加解密、文件加解密的功能.最后通過軟件實例,展示了該協議在正常商業軟件上的應用過程.

[1] Lei Xin-feng,Song Shu-min,Liu Wei-bing,et al.A srvey on computationally sound formal analysis of cryptographic [J].Chinese Journal of Computers,2014,37(5):993-1016.

[2] Hu Xiao-hui,Chen Hui-li,Shi Guang-tian,et al.Formal modeling and verification of CTCS-4 security[J].Computer Engineering and Applications,2014,50(4):81-85.

[3] Liu S M,Ye J Y,Wang Y L.Improvement and security analysis on symmetric key authentication needham-schroeder[J].Applied Mechanics & Materials,2014,513-517:1289-1293.

[4] Lai Y,Chen Y,Zou Q,et al.Design and analysis on trusted network equipment access authentication[J].Simulation Modelling Practice & Theory,2015,51(51):157-169.

[5] Wang Zheng-cai,Xu Dao-yun,Wang Xiao-feng,et al.Reliability analysis and improvement of BAN logic[J].Computer Engineering,2012,38(17):110-115.

[6] Lu Si-qi,Cheng Qing-feng,Zhao Jin-hua.Comparison study of formal verification tools for security protocols[J].Journal of Cryptologic Research,2014,1(6):568-577.

[7] Xue Rui,Feng Deng-guo.A survey on formal analysis of security[J].Journal of Cryptologic Research,2014,1(5):504-512.

[8] Xue Rui,Lei Xin-feng.Present status and trends of researches on analyses of security[J].Bulletin of Chinese Academy of Sciences,2011,(3):287-296.

[9] Shi Guang-tian,Chen Hui-li.Formal analysis and verification of a new improved NSSK protocol [C].Proceedings of the 2014 International Conference on E-Commerce,E-Business and E-Service(EEE 2014),Information Engineering Research Institute,USA,2014:20-24.

[10] Needham R M,Schroeder M D.Using encryption for authentication in large networks of computers[J].Communications of the ACM,1978,21(12):993-999.

[11]Wang Kun,Zhou Qing-lei.RFID mutual authentication protocol of new internet of things[J].Journal of Chinese Computer Systems,2015,36(4):732-738.

[12]Cai Da-zhuang,Yang Hai-bo.Research on a secure communication model for IMS assess layer using two-stage DH algorithm[J].Journal of Chinese Computer Systems,2016,37(4):782-786.

[13]Shao Fei,Meng Bo.A Non-interactive deniable authentication protocol based on elliptic curve discrete logarithm problem[J].Journal of Chinese Computer Systems,2014,35(1):89-92.

附中文參考文獻：

[1] 雷新鋒,宋書民,劉偉兵,等.計算可靠的密碼協議形式化分析綜述[J].計算機學報,2014,37(5):993-1016.

[2] 胡曉輝,陳慧麗,石廣田,等.CTCT-4級安全通信協議的形式化建模與驗證[J].計算機工程與應用,2014,50(4):81-85.

[5] 王正才,許道云,王曉峰,等.BAN邏輯的可靠性分析與改進[J].計算機工程,2012,38(17):110-115.

[6] 陸思奇,程慶豐,趙進華.安全協議形式化分析工具比較研究[J].密碼學報,2014,1(6):568-577.

[8] 薛 銳,雷新鋒.安全協議:信息安全保障的靈魂—安全協議分析研究現狀與發展趨勢[J].中國科學院院刊,2011,(3):287-296.

[11]王 坤，周清雷.新物聯網下的RFID雙向認識協議[J].小型微型計算機系統，2015，36(4)：732-738.

[12]才大壯，楊海波.使用兩階段DH算法的IMS接入側安全通信模型研究[J].小型微型計算機系統，2016，37(4)：782-786.

[13]邵 飛，孟 博.一種基于橢圓曲線離散對數問題的非交互式可否認認證協議[J].小型微型計算機系統，2014，35(1)：89-92.