一種改進(jìn)的NSSK認(rèn)證協(xié)議及其實現(xiàn)方法

于金剛,趙治剛

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

1 引 言

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

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

2 NS協(xié)議分析

R.M.Needham和M.D.Schoreder于1978年首次提出了利用加密技術(shù)設(shè)計認(rèn)證密鑰分配協(xié)議[3](簡稱NS協(xié)議),NS協(xié)議的運行原理共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條消息是在密鑰分發(fā)中心S的幫助下,完成共享密鑰KAB的分配,后2條消息是為了確認(rèn)雙方已經(jīng)收到共享密鑰,并且可以進(jìn)行正常通信.但存在不能使B相信消息3的新鮮性的缺陷及消息4只攜帶接收方的隨機(jī)數(shù),無法使發(fā)送方A識別接收方的身份的不足.

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

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

1.A→S:A、B、NA

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

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

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協(xié)議的正常通信,消息3被身份冒充者I攔截,因為原始協(xié)議消息4中沒有發(fā)送方A的身份標(biāo)示,故I將一個與原始消息(NB)KAB格式相同的NI發(fā)給發(fā)送方A,發(fā)送方A對消息NI使用共享密鑰KAB解密,對所得結(jié)果進(jìn)行函數(shù)操作,使用共享密鑰KAB加密后發(fā)送給B,同時消息5也被I截獲,但是發(fā)送方A認(rèn)為接收方B已經(jīng)接收共享密鑰KAB并且能夠正常通話.

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

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

3 改進(jìn)版認(rèn)證協(xié)議的設(shè)計

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

在原始NS協(xié)議的基礎(chǔ)上,改進(jìn)版的認(rèn)證協(xié)議增加接收方發(fā)送隨機(jī)數(shù)給密鑰分發(fā)中心的過程,并在密鑰分發(fā)中心生成的消息中添加發(fā)送方和接收方的隨機(jī)數(shù)及其對應(yīng)的身份標(biāo)示,達(dá)到確保消息新鮮性的同時完成對密鑰分發(fā)中心身份認(rèn)證的目的[8];將使用共享密鑰加密后的發(fā)送方的隨機(jī)數(shù)添加到接收方發(fā)送給發(fā)送方的消息中,以便使發(fā)送方在完成消息新鮮性驗證的同時,確保接收方已經(jīng)收到共享密鑰.

改進(jìn)版的認(rèn)證協(xié)議交互過程如圖1所示.

圖1 改進(jìn)的認(rèn)證協(xié)議運行原理圖Fig.1 Improved protocol operation diagram

協(xié)議的運行步驟描述如下:

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

詳細(xì)描述如下:

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

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

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

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

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

4 改進(jìn)版認(rèn)證協(xié)議的形式化驗證

本文使用基于信念的模態(tài)邏輯BAN邏輯對改進(jìn)協(xié)議進(jìn)行形式化驗證[2],以保證該認(rèn)證協(xié)議可以達(dá)到安全目標(biāo)(機(jī)密性、認(rèn)證性、不可否認(rèn)性、完整性)[7].其驗證流程如圖2所示.

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

上圖對應(yīng)的驗證步驟如下:

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

2.規(guī)定使協(xié)議安全運行的初始假設(shè)集.

3.用BAN邏輯規(guī)則,通過理想化模型和假設(shè)集合進(jìn)行推理演算,得到協(xié)議運行的結(jié)果集.

4.通過分析結(jié)果集來判定協(xié)議是否達(dá)到設(shè)計目標(biāo).

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

4.1 對改進(jìn)的認(rèn)證協(xié)議進(jìn)行理想化建模

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

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

(P2)S→B:

(P3)B→A:

4.2 建立初始假設(shè)集合

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

4.3 形式化驗證

利用初始假設(shè)和推理規(guī)則對協(xié)議進(jìn)行進(jìn)行形式化驗證過程如下:

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

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

(1)

由初始假設(shè)3、4和消息含義規(guī)則有:

S|≡A|～NA

(2)

S|≡B|～NB

(3)

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

(4)

由初始假設(shè)2和消息含義規(guī)則有:

(5)

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

(6)

(7)

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

(8)

(9)

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

(10)

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

(11)

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

(12)

(13)

由初始假設(shè)6、11和管轄規(guī)則有:

(14)

(15)

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

(16)

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

(17)

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

(18)

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

(19)

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

(20)

協(xié)議的最終推理結(jié)果集合為:

4.4 驗證結(jié)果

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

5 改進(jìn)版協(xié)議的實現(xiàn)

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

在TF加密卡基礎(chǔ)上的加密通信圖見圖3.

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

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

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

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

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

圖4 登錄界面Fig.4 Login interface

登錄界面及登錄成功后狀態(tài)見圖4.

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

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

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

1.sessionInit(session,SecId,SecId):發(fā)送方A調(diào)用該接口,通過業(yè)務(wù)服務(wù)器通知接收方B進(jìn)行會話初始化.

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

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

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

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

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

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

6 改進(jìn)版協(xié)議的應(yīng)用

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

圖5 本端證書Fig.5 Local certification

圖5展示了改進(jìn)版的認(rèn)證協(xié)議在即時消息通信中各個環(huán)節(jié)的使用效果:

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

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

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

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

使用共享密鑰進(jìn)行文本消息及文件信息的交互,交互過程中與業(yè)務(wù)服務(wù)器之間的信息都是密文形式:

圖7為消息交互界面.

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

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

圖8 消息abc對應(yīng)密文Fig.8 Cphertext of the message abc

圖9 文件發(fā)送前內(nèi)容Fig.9 Cntent of file before sending

使用共享密鑰對文件內(nèi)容進(jìn)行加密后,以附件形式通過http協(xié)議上傳到業(yè)務(wù)服務(wù)器,發(fā)送方將文件描述信息作為本文消息加密發(fā)送到接收方,收到文件描述信息解密后,從業(yè)務(wù)服務(wù)器下載密文文件到本地進(jìn)行解密:

圖9為發(fā)送前的文件內(nèi)容.

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

圖10標(biāo)示業(yè)務(wù)服務(wù)器已經(jīng)接收到該文件(圖7中發(fā)送的文件名).

7 結(jié)束語

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

[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.

附中文參考文獻(xiàn)：

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

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

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

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

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

[11]王 坤，周清雷.新物聯(lián)網(wǎng)下的RFID雙向認(rèn)識協(xié)議[J].小型微型計算機(jī)系統(tǒng)，2015，36(4)：732-738.

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

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