摘 要:以ISO/IEC 11770-2密鑰建立機(jī)制為例,對(duì)無(wú)可信第三方的身份認(rèn)證協(xié)議進(jìn)行研究,進(jìn)行嚴(yán)格的形式化分析和安全性能分析,發(fā)現(xiàn)其在不可否認(rèn)性方面存在一定的缺陷,并提出了改進(jìn)的方案,進(jìn)一步增強(qiáng)了協(xié)議的安全性能。
關(guān)鍵詞:無(wú)可信第三方;身份認(rèn)證;形式化分析
引言
隨著移動(dòng)互聯(lián)網(wǎng)的飛速發(fā)展,各種互聯(lián)網(wǎng)服務(wù)給人們帶來(lái)了便利,其安全問(wèn)題也成為一個(gè)社會(huì)關(guān)注的焦點(diǎn)。身份認(rèn)證是確保網(wǎng)絡(luò)應(yīng)用安全的第一道關(guān)卡,已成為當(dāng)前信息安全領(lǐng)域的研究熱點(diǎn)之一。
根據(jù)協(xié)議中可信第三方的參與情況,可以將身份認(rèn)證協(xié)議分為有可信第三方的和無(wú)可信第三方的兩大類[1]。在有可信第三方的身份認(rèn)證協(xié)議中,協(xié)議的交互需要借助可信的第三方來(lái)認(rèn)證用戶的身份,通常需要用戶在第三方處進(jìn)行相關(guān)的信息注冊(cè),可信第三方與每個(gè)用戶都分別有共享的秘密信息。在無(wú)可信第三方的身份認(rèn)證協(xié)議中,雙方進(jìn)行身份認(rèn)證不需要可信第三方的參與,僅通過(guò)交換消息便可進(jìn)行實(shí)體認(rèn)證,協(xié)議執(zhí)行中用于加密消息的密鑰需要保存在雙方本地。如果使用對(duì)稱加密體制,需要各用戶之間存在共享的密鑰。
文章著重研究的無(wú)服務(wù)器密鑰建立協(xié)議,是一種非常典型的無(wú)可信第三方身份認(rèn)證協(xié)議,協(xié)議雙方不利用服務(wù)器而直接完成雙向認(rèn)證并成功交換密鑰。ISO/IEC 11770-2密鑰建立協(xié)議[2]是其中的典型,一共定義了13種密鑰建立機(jī)制,前6種密鑰建立機(jī)制不需要可信第三方的參與。文章重點(diǎn)對(duì)其第6種密鑰建立機(jī)制進(jìn)行深入的分析,運(yùn)用BAN邏輯對(duì)其進(jìn)行嚴(yán)謹(jǐn)?shù)男问交治觯l(fā)現(xiàn)其存在的缺陷,并提出相應(yīng)的改進(jìn)方案。
1 ISO/IEC 11770-2密鑰建立機(jī)制6
ISO/IEC 11770-2密鑰建立機(jī)制6使用對(duì)稱加密體制,涉及兩個(gè)主體A和B,均擁有長(zhǎng)期共享的密鑰Kab,通過(guò)引入隨機(jī)數(shù)來(lái)保持信息的新鮮性,具體過(guò)程如圖1所示。
(1)B→A:Nb B向A發(fā)出通信請(qǐng)求,發(fā)送隨機(jī)數(shù)Nb。
(2)A→B:{Na,Nb,B,F(xiàn)ab}Kab A收到來(lái)自B的請(qǐng)求后,用與B長(zhǎng)期共享的密鑰Kab加密消息{Na,Nb,B,F(xiàn)ab}發(fā)送給B,其中隨機(jī)數(shù)Na、Nb用以標(biāo)識(shí)該會(huì)話信息的新鮮性,B為身份區(qū)分標(biāo)識(shí)符,密鑰材料Fab用來(lái)后繼生成會(huì)話密鑰K。
(3)B→A:{Nb,Na,F(xiàn)ba}Kab B將收到的消息解密,通過(guò)核對(duì)隨機(jī)數(shù)Nb和身份標(biāo)識(shí)B確認(rèn)這是與A之間的會(huì)話,然后用密鑰Kab將{ Nb,Na,F(xiàn)ba}加密后發(fā)送給A,其中密鑰材料Fba用來(lái)生成會(huì)話密鑰K。
通過(guò)上述3個(gè)步驟,會(huì)話雙方A和B能夠確認(rèn)對(duì)方身份,并生成新的會(huì)話密鑰K=F(Fab,F(xiàn)ba),A和B能借助K建立新的安全會(huì)話。
2 ISO/IEC 11770-2密鑰建立機(jī)制6的形式化分析
2.1 BAN邏輯簡(jiǎn)介
目前廣泛使用的安全協(xié)議形式化分析方法是基于知識(shí)和信念的形式邏輯分析法[3],其中最有影響力的是BAN邏輯[4]。BAN邏輯是一種基于信念的模態(tài)邏輯,其目標(biāo)是認(rèn)證參與協(xié)議的主體的身份,分析協(xié)議能否達(dá)到預(yù)定的目標(biāo),其基本語(yǔ)句及其含義如表1所示。
BAN邏輯的主要推理規(guī)則如下:
(1)消息含義規(guī)則R1:(P|≡Q P, P△{X}K)/(P|≡Q|~X),表示若P相信K為P、Q間的共享密鑰,且P收到過(guò)信息{X}K ,那么P就相信Q曾發(fā)送過(guò)信息X。
(2)隨機(jī)數(shù)驗(yàn)證規(guī)則R2:{P|≡#(X),P|≡Q|~X}/(P|≡Q|≡X),表示若P相信消息X是新鮮的,且P相信Q曾發(fā)送過(guò)X,那么P就相信Q是相信X的。
(3)信仰規(guī)則R3:{P|≡Q|≡(X,Y)}/(P|≡Q|≡X),表示若P相信Q相信消息(X,Y),則P相信Q相信X。
(4)管轄規(guī)則R4:(P|≡Q|=>X,P|≡Q|≡X)/(P|≡X),如果P相信Q對(duì)X具有管轄權(quán),而且P相信Q相信X,那么P就相信X。
(5)新鮮性規(guī)則R5:{P|≡#(X)}/{P|≡#(X,Y)},表示若P相信消息X是新鮮的,則P相信消息(X,Y)也是新鮮的。
2.2 協(xié)議的形式化分析
(1)協(xié)議的形式化描述
主體A和B之間主要通過(guò)以下三步完成認(rèn)證:
1.B→A:Nb;2.A→B:{Na,Nb,B,F(xiàn)ab}Kab;3.B→A:{Nb,Na,F(xiàn)ba}Kab
(2)初始假設(shè)
A、B相信彼此間的共享密鑰Kab:P1:A|≡A B;P2:B|≡A B;
A、B相信各自發(fā)送隨機(jī)數(shù)的新鮮性:P3:A|≡#(Na);P4:B|≡#(Nb);
A、B相信彼此對(duì)密鑰材料具有控制權(quán):P5:A|≡B|=>Fba;P6:B|≡A|=>Fab。
(3)協(xié)議的安全目標(biāo)
A、B相信對(duì)方傳來(lái)的密鑰材料Fba和Fab:G1:A|≡Fba;G2:B|≡Fab
(4)形式化分析過(guò)程
a.當(dāng)B△{Na,Nb,B,F(xiàn)ab}Kab時(shí),根據(jù)初始假設(shè)P2和消息含義規(guī)則R1:
(B|≡A B,B△{Na,Nb,B,F(xiàn)ab}Kab)/{B|≡A|~(Na,Nb,B,F(xiàn)ab)},
可得:B|≡A|~(Na,Nb,B,F(xiàn)ab) (1)
即:B相信A曾發(fā)送過(guò)消息{Na,Nb,B,F(xiàn)ab}。
b.根據(jù)初始假設(shè)P4與消息新鮮性規(guī)則R5:
{B|≡#(Nb)}/{B|≡#(Na,Nb,B,F(xiàn)ab)},
可得:B|≡#(Na,Nb,B,F(xiàn)ab) (2)
即:B相信消息{Na,Nb,B,F(xiàn)ab}的新鮮性。
c.由(1)、(2)和隨機(jī)數(shù)驗(yàn)證規(guī)則R2:
{B|≡#(Na,Nb,B,F(xiàn)ab),B|≡A|~(Na,Nb,B,F(xiàn)ab)}/{B|≡A|≡(Na,Nb,B,F(xiàn)ab)},
可得:B|≡A|≡(Na,Nb,B,F(xiàn)ab) (3)
即:B相信A相信消息{Na,Nb,B,F(xiàn)ab}的真實(shí)性。
d.由(3)和信仰規(guī)則R3:
{B|≡A|≡(Na,Nb,B,F(xiàn)ab)}/(B|≡A|≡Fab),
可得:B|≡A|≡Fab (4)
即:B相信A相信密鑰材料Fab。
e.由(4)、初始假設(shè)P6和管轄規(guī)則R4:
(B|≡A|=>Fab,B|≡A|≡Fab)/(R|≡P),可得:B|≡Fab,表示B信任收到的密鑰材料Fab,安全目標(biāo)G2得證。
同理,可推導(dǎo)出安全目標(biāo)G1:A|≡Fba。
至此,ISO/IEC 11770-2密鑰建立機(jī)制6的形式化分析結(jié)果表明,認(rèn)證主體A和B可以實(shí)現(xiàn)相互之間的雙向認(rèn)證,可以通過(guò)密鑰派生函數(shù)得到新的會(huì)話密鑰K=F(Fab,F(xiàn)ba),并能借此建立新的安全會(huì)話,達(dá)到預(yù)期的目標(biāo)。
3 ISO/IEC 11770-2密鑰建立機(jī)制6的安全性分析及改進(jìn)
由上述形式化分析可以看出,ISO/IEC 11770-2密鑰建立機(jī)制6能夠使雙方主體A和B實(shí)現(xiàn)雙向認(rèn)證,雙方信任收到的密鑰材料并生成可信的會(huì)話密鑰。但就協(xié)議的執(zhí)行流程而言,在不可否認(rèn)性方面存在一定的缺陷。Fab和隨機(jī)數(shù)Na、Nb一起組合加密發(fā)送給B,B通過(guò)向A返還Na,表明B收到了A發(fā)送給的消息,即主體A可以確認(rèn)B收到密鑰材料Fab。反之,B卻無(wú)法確認(rèn)A一定收到Fba。即如果協(xié)議第三步傳輸?shù)男畔G失,主體A就無(wú)法收到密鑰材料Fba,也將無(wú)法生成新的會(huì)話密鑰,而B(niǎo)卻對(duì)此一無(wú)所知。因此建議主體A在收到Fba并生成新的會(huì)話密鑰K后,回傳一條信息{Nb}K給B,主體B就可以確認(rèn)A收到了密鑰材料,從而使雙方都能夠確認(rèn)對(duì)方能夠生成新的會(huì)話密鑰,同時(shí)也可以避免會(huì)話主體間的惡意否認(rèn)和相互欺詐。
4 結(jié)束語(yǔ)
ISO/IEC 11770-2密鑰建立機(jī)制6作為一種簡(jiǎn)單的無(wú)可信第三方身份認(rèn)證協(xié)議有著計(jì)算量小、簡(jiǎn)單易實(shí)現(xiàn)的優(yōu)勢(shì),同時(shí)也存在適用范圍有限、難以大規(guī)模使用的局限性。該協(xié)議通過(guò)長(zhǎng)期共享的密鑰來(lái)生成新的會(huì)話密鑰,并通過(guò)引入隨機(jī)數(shù)來(lái)保證消息的新鮮性,用于抵抗重放攻擊,并使用身份標(biāo)識(shí)來(lái)抵抗預(yù)重放、反射攻擊。文章運(yùn)用BAN邏輯對(duì)ISO/IEC 11770-2密鑰建立機(jī)制6進(jìn)行了嚴(yán)格的形式化分析,結(jié)果表明,在協(xié)議執(zhí)行完整的情況下,雙方主體能夠?qū)崿F(xiàn)雙向認(rèn)證,信任收到的密鑰材料并生成可信的會(huì)話密鑰。對(duì)協(xié)議的安全性分析表明,該協(xié)議無(wú)法抵御通信主體之間的惡意否認(rèn)和相互欺詐,文章對(duì)此提出了改進(jìn)方案,通過(guò)增加一條主體A返回B的驗(yàn)證性消息以抵御否認(rèn),增加協(xié)議的安全性,進(jìn)一步完善了該協(xié)議。
參考文獻(xiàn)
[1]衛(wèi)劍釩,陳鐘.安全協(xié)議分析與設(shè)計(jì)[M].人民郵電出版社,2010.
[2]ISO/IE 1170-2.Information Technology-Security Techniques-Key Management-Part 2:Mechanisms Using Symmetric Techniques[S].1996.
[3]雷新鋒,薛銳.密碼協(xié)議分析的邏輯方法[M].北京:科學(xué)出版社,2013.
[4]Burrrows M,Abadi M,Needham R.A logic of authentication[J].ACM Transactions on Computer Systems,1990,8(1):18-36.