李曉樂,翁 鳴,羅應(yīng)機,文 英
(1.廣西財經(jīng)學(xué)院實驗教學(xué)中心,廣西南寧530003;2.中國移動通信集團(tuán)廣西分公司,廣西南寧530022)
協(xié)議自動生成機制[1,2]能夠提高安全協(xié)議設(shè)計的效率和質(zhì)量,但應(yīng)用范圍有限,可以結(jié)合組合設(shè)計方法[3-5]進(jìn)行復(fù)合協(xié)議的設(shè)計,但是必須確保各原語具備可組合性。針對此問題的研究有“應(yīng)用環(huán)境相符”、“安全目標(biāo)相容”、“避免符號重復(fù)”、“選擇無干擾性原語”、“規(guī)范符號描述”等規(guī)則[6,7],屬于協(xié)議表示符號的規(guī)范性約束,不能保證原語本身的可組合性,若在組合設(shè)計過程中才進(jìn)行原語的可組合性設(shè)計,必將增加設(shè)計過程的復(fù)雜度。
應(yīng)該通過改進(jìn)原語結(jié)構(gòu),比如添加可組合元素等方式,實現(xiàn)原語的可組合性,并有效降低針對多個原語組合設(shè)計過程的復(fù)雜度。因此構(gòu)建了一種基于原語自動生成的安全協(xié)議組合設(shè)計的新策略,提出了新的可組合元素附加規(guī)則和組合設(shè)計規(guī)則,進(jìn)行了應(yīng)用研究,通過實例說明了策略的可行性;最后給出了總結(jié)和展望。
該組合設(shè)計策略模型分為原語自動設(shè)計、可組合元素附加和原語組合設(shè)計3個模塊,如圖1所示。
圖1 策略模型
(1)原語自動設(shè)計:利用自動生成工具,首先將安全需求和系統(tǒng)規(guī)格輸入到生成器中;然后基于系統(tǒng)規(guī)格對原語空間進(jìn)行搜索,產(chǎn)生候選原語和每個原語的驗證條件;最后對每個原語的驗證條件進(jìn)行校驗并輸出正確結(jié)果。
(2)可組合元素附加:根據(jù)4類新的原語可組合元素附加規(guī)則(“參與方-秘密項綁定規(guī)則”、“多回合抗干擾規(guī)則”、“認(rèn)證性可組合規(guī)則”、“保密性可組合規(guī)則”等),通過修改原語中消息的結(jié)構(gòu),添加可組合元素,使簡單原語可用作組合設(shè)計復(fù)合協(xié)議的基本元素,為后續(xù)的組合設(shè)計提供正確性保障并降低復(fù)雜度,也可驗證原語的可組合性。
(3)原語組合設(shè)計:根據(jù)針對可組合性原語的新組合設(shè)計規(guī)則,確定多事件組合順序、合并相似消息并消除冗余信息。
通過自動化設(shè)計工具,可以高效生成滿足單個安全目標(biāo)的簡單原語。然而將多個簡單原語組合為復(fù)合協(xié)議時,必須考慮到原語組合可能造成不同原語的安全屬性互相影響甚至破壞。為保證原有的安全性,基于串空間和認(rèn)證測試,提出了新的針對簡單原語的4類可組合元素附加規(guī)則,通過修改原語中項的結(jié)構(gòu),在原語中添加可組合元素,使簡單原語可用作組合設(shè)計復(fù)合協(xié)議的基本元素,為后續(xù)的組合設(shè)計過程提供正確性保障和降低復(fù)雜度。
為保障多原語組合設(shè)計的安全性,當(dāng)原語中的參與者在一個協(xié)議回合中產(chǎn)生了一個秘密時,需要將這個秘密關(guān)聯(lián)到相應(yīng)的參與者上。若參與者與秘密之間的綁定缺失,往往導(dǎo)致協(xié)議存在安全缺陷,遭到類似于針對NSPK協(xié)議的中間人攻擊:
在上述協(xié)議回合中,由于{NA,NB}eKA里缺少秘密的綁定信息,導(dǎo)致攻擊者I可以假冒A的身份與B進(jìn)行通信,從而得到A與B間的秘密NB。以此為鑒,為有效規(guī)避中間人攻擊等安全威脅,提出參與方-秘密項綁定規(guī)則如下。
參與方-秘密項綁定規(guī)則:若在加密信息中包含秘密x,則必須同時包含x的綁定組。
在該規(guī)則的保護(hù)下,協(xié)議中的發(fā)起者發(fā)送包含秘密及其綁定組的一則消息,然后收到一則來自響應(yīng)者的消息,對項綁定進(jìn)行確認(rèn)。每則挑戰(zhàn)消息都明確發(fā)送者和接收者,不論響應(yīng)者在何時創(chuàng)建了一個回復(fù),都明確表達(dá)消息的含義。
作為安全基本元素,每個原語在單獨運行時不會干擾其它原語。然而,由于消息的相似性,多個原語運行在同一個協(xié)議中時可能互相干擾。以雙向認(rèn)證協(xié)議的組合設(shè)計為例,P1和P2是兩個單向認(rèn)證原語,P=P1P2,其中P1和P2如下所示,x≠y,且βx=βy=(A,B)。
P1和P2在作為獨立的協(xié)議時不會互相影響,但是作為P的一部分組合在一起時,卻產(chǎn)生互相干擾。若A收到形如M2或N2的消息,那么該消息既可以解釋為原語P1的一個回合中的消息(在該回合中扮演發(fā)起者的角色),又可以解釋為原語P2的一個回合中的消息(在該回合中扮演響應(yīng)者的角色)。干擾產(chǎn)生的原因是原語中存在相似的認(rèn)證消息結(jié)構(gòu),導(dǎo)致組合產(chǎn)生的協(xié)議面臨剪切攻擊和粘貼攻擊的威脅。因此需要在認(rèn)證消息項中添加索引或相關(guān)參與者名稱,用以區(qū)分不同的原語,如下所示:
以此為鑒,提出多回合抗干擾規(guī)則如下:
多回合抗干擾規(guī)則:針對同一個會話中同時運行的多個原語,為所有的結(jié)構(gòu)相似的認(rèn)證消息項添加一個唯一的索引值或相關(guān)主體名稱。
在該規(guī)則的保護(hù)下,即使存在多條類似結(jié)構(gòu)的認(rèn)證消息,也可根據(jù)索引或參與者名稱標(biāo)明不同的消息屬于哪個原語,避免相似消息間的混亂。為保證抗干擾的有效性,索引或參與者名稱需要插入到發(fā)生密碼學(xué)轉(zhuǎn)換的消息中。
使認(rèn)證可組合的兩個最重要的屬性是不可構(gòu)造性和不可破壞性,因此分別從這兩個屬性出發(fā)建立規(guī)則,實現(xiàn)原語認(rèn)證性的可組合。
2.3.1 不可構(gòu)造性規(guī)則
采用一致性測試[8]作為認(rèn)證機制后可以確保認(rèn)證性的不可構(gòu)造性,因此提出不可構(gòu)造性規(guī)則如下:
認(rèn)證性可組合規(guī)則1(不可構(gòu)造性規(guī)則):
(1)作為一個挑戰(zhàn),以明文的形式發(fā)送現(xiàn)時值,在隨后以加密的形式收到,且加密密鑰為對稱密鑰體制下雙方共享的保密密鑰或非對稱密鑰體制下響應(yīng)者獨有的簽名密鑰;
(2)在同一協(xié)議回合中,發(fā)起者與響應(yīng)者的角色唯一對應(yīng)且在與所有變量相關(guān)的數(shù)據(jù)值上達(dá)成一致。
2.3.2 不可破壞性規(guī)則
認(rèn)證目標(biāo)的不可破壞性與用于認(rèn)證的長期值和短期值的保密性相關(guān)。但是同一個現(xiàn)時值的兩次使用也可能破壞認(rèn)證性目標(biāo),不應(yīng)在對超過一個參與者的認(rèn)證中使用相同的現(xiàn)時值。因此提出不可破壞性規(guī)則如下。
認(rèn)證性可組合規(guī)則2(不可破壞性規(guī)則):確保長期密鑰安全,且同一個現(xiàn)時值不用于對兩個以上不同參與者認(rèn)證。
2.3.3 保密性可組合規(guī)則
保密性可組合問題包括長期秘密和短期秘密的可組合。每一個協(xié)議回合中,參與者的長期秘密(如簽名密鑰和解密密鑰)和回合的短期秘密(如對稱密鑰和傳遞的秘密)都不能被入侵者分析得到,因此提出保密性可組合規(guī)則如下:
保密性可組合規(guī)則:不能將長期秘密用作現(xiàn)時值或短期秘密,且任何長期和短期秘密的保護(hù)域Sx都是I兼容的。
針對組合設(shè)計規(guī)則的研究主要包括單步協(xié)議選取、組合順序、去掉冗余、non-Dos,以及組合順序、替換實現(xiàn)組合、子協(xié)議合并、消息合并、消息組合等[6,7]。通過可組合元素附加階段的設(shè)計,原語已經(jīng)具備了可組合性,組合設(shè)計的復(fù)雜度得到較大降低,因此組合設(shè)計過程比較簡單,主要考慮多事件順序、相似消息的合并以及冗余信息的消除。
事件組合順序規(guī)則:
(1)e+(x)<e-(x)且(vx)<e+(x),即項x所有的發(fā)送事件都先于接收事件,在生成新變量x之后才能對其發(fā)送;
(2)不同原語相似事件的組合順序由主體在協(xié)議中扮演的角色決定,發(fā)起者事件的優(yōu)先級高于響應(yīng)者相似事件。
消息合并規(guī)則:
(1)不同原語的多個協(xié)議步合并時,從第一個擁有相同的消息發(fā)送者和接收者的消息開始依次合并;
(2)同一步協(xié)議中,將采用相同加密體制和密鑰的加密消息項合并。
冗余信息消除規(guī)則:
(1)同一步協(xié)議中,內(nèi)容或功能重復(fù)的項只保留一個;若某個明文字段在該消息項的加密字段中亦出現(xiàn),則刪去該明文字段。
(2)不同協(xié)議步中,內(nèi)容或功能重復(fù)的消息項可以互相替換。
基于策略模型,進(jìn)行了應(yīng)用研究,分別設(shè)計出了非對稱密鑰體制下雙向認(rèn)證協(xié)議和對稱密鑰體制下雙向認(rèn)證及密鑰建立協(xié)議。實踐結(jié)果表明,該策略同時具備自動設(shè)計正確高效以及組合設(shè)計簡便易行的優(yōu)點。
(1)非對稱密鑰體制下單向認(rèn)證原語的自動設(shè)計
使用協(xié)議自動生成工具設(shè)計非對稱密鑰體制下單向認(rèn)證原語可得:
轉(zhuǎn)化為標(biāo)準(zhǔn)協(xié)議工程符號形式,得到原語P1如下:
同理,得到原語P2如下:
(2)原語可組合元素附加
根據(jù)協(xié)議的設(shè)計目標(biāo)和原語結(jié)構(gòu),為使原語P1和P2具備可組合性,需要根據(jù)“參與方-秘密綁定規(guī)則”、“多回合抗干擾規(guī)則”、“認(rèn)證性可組合規(guī)則”、“保密性可組合規(guī)則”等新提出的4類原語可組合元素附加規(guī)則,修改某些消息項的結(jié)構(gòu),使原語具備可組合性:
1)根據(jù)“參與方-秘密項綁定規(guī)則”,由于原語P1和P2中的現(xiàn)時值用于單向認(rèn)證,不作為交換的秘密,因此無需在加密消息項中添加針對秘密的綁定組信息。
2)根據(jù)“多回合抗干擾規(guī)則”,原語P1和P2均使用結(jié)構(gòu)相似的認(rèn)證消息項完成單向認(rèn)證,針對同一個會話中應(yīng)同時進(jìn)行的多個原語,為認(rèn)證消息項中的現(xiàn)時值添加一個唯一的索引值(或主體名稱)。修改后的原語P11和P21如下:
3)根據(jù)“認(rèn)證性可組合規(guī)則1”,原語P11和P21的消息項結(jié)構(gòu)滿足不可構(gòu)造性;根據(jù)“認(rèn)證性可組合規(guī)則2”,兩次單向認(rèn)證不能使用相同的現(xiàn)時值,修改原語P12如下:
同理,得到原語P22如下:
4)根據(jù)“保密性可組合規(guī)則”,由于原語P1和P2中的現(xiàn)時值用于單向認(rèn)證,不作為交換的秘密,也未將長期密鑰用作現(xiàn)時值或短期秘密,因此無需對消息項進(jìn)行修改。
(3)原語組合設(shè)計
1)根據(jù)事件組合順序規(guī)則,確定時間組合順序。
首先注明原語P12和P22中的各事件:
確定事件順序為:
2)根據(jù)“消息合并規(guī)則”,令P=P12P22。
首先合并不同原語的多個協(xié)議步:
然后將同一協(xié)議步中采用相同加密體制和密鑰的加密消息項合并:
3)根據(jù)“冗余信息消除規(guī)則”,消減同一步協(xié)議中內(nèi)容或功能重復(fù)的消息項,替換不同協(xié)議步中功能重復(fù)的消息項,可得非對稱密鑰體制下兩方認(rèn)證協(xié)議如下:
為增加可讀性,可將索引替換為主體名稱:
(1)對稱密鑰體制下帶有可信第三方的單向認(rèn)證且密鑰建立原語的自動設(shè)計
使用協(xié)議自動生成工具設(shè)計對稱密鑰體制下帶有可信第三方的單向認(rèn)證且密鑰建立原語可得:
轉(zhuǎn)化為標(biāo)準(zhǔn)協(xié)議工程符號形式,得到原語P1如下:
(2)對稱密鑰體制下帶有可信第三方的單向認(rèn)證原語的自動設(shè)計
使用協(xié)議自動生成工具設(shè)計對稱密鑰體制下帶有可信第三方的單向認(rèn)證原語可得:
轉(zhuǎn)化為標(biāo)準(zhǔn)協(xié)議工程符號形式,得到原語P2如下:
(3)可組合元素附加
同理,為使原語P1和P2具備可組合性,需要添加可組合元素:
1)根據(jù)“參與方-秘密項綁定規(guī)則”,在原語P1包含秘密kAB的加密項中,分別添加kAB的綁定組βSA=(S,A)和βSB=(S,B),修改后的原語P11如下:
由于原語P2中的現(xiàn)時值用于單向認(rèn)證,不作為交換秘密,因此無需在加密消息項中添加針對秘密的綁定組信息。
2)根據(jù)“多回合抗干擾規(guī)則”,針對同一個會話中應(yīng)同時進(jìn)行的多個原語,為所有的結(jié)構(gòu)相似的消息添加一個唯一的索引值,修改后的兩個原語如下:
3)根據(jù)“認(rèn)證性可組合規(guī)則1”,原語P12和P21的消息項結(jié)構(gòu)滿足不可構(gòu)造性;根據(jù)“認(rèn)證性可組合規(guī)則2”,原語P12和P21的消息項結(jié)構(gòu)滿足不可破壞性。因此無需修改原語的消息項。
4)根據(jù)“保密性可組合規(guī)則”,由于原語P12中的現(xiàn)時值用于單向認(rèn)證,不作為交換的秘密,且對稱密鑰kAB的保護(hù)域Sx與I是兼容的,因此無需對消息項進(jìn)行修改;由于原語P21中的現(xiàn)時值用于單向認(rèn)證,不作為交換的秘密,也未將長期密鑰用作現(xiàn)時值或短期秘密,因此無需對消息項進(jìn)行修改。
(4)原語組合設(shè)計
1)根據(jù)事件組合順序規(guī)則,確定時間組合順序。
首先注明原語P12和P21中的各事件:
確定事件順序為:
由于協(xié)議的設(shè)計目標(biāo)是在完成雙向認(rèn)證后建立密鑰,因此有:
2)根據(jù)“消息合并規(guī)則”,令P=P12P21。
首先合并不同原語的多個協(xié)議步:
然后將同一協(xié)議步中采用相同加密體制和密鑰的加密消息項合并:
3)由于組合設(shè)計過程中,某些消息項結(jié)構(gòu)發(fā)生改變,通過合并加密消息項避免了相似消息項結(jié)構(gòu)帶來的多回合干擾問題,因此索引信息成為冗余。
根據(jù)“冗余信息消除規(guī)則”,消減同一步協(xié)議中內(nèi)容或功能重復(fù)的消息項,替換不同協(xié)議步中功能重復(fù)的消息項,可得對稱密鑰體制下帶有可信第三方的兩方認(rèn)證且密鑰建立協(xié)議:
以下從安全性、設(shè)計效率和復(fù)雜度的角度,分析新策略的應(yīng)用效果。
(1)安全性分析
組合設(shè)計得到的安全協(xié)議,其安全性依賴于單獨原語的安全屬性和組合設(shè)計過程的安全性:單獨原語均通過協(xié)議自動生成工具產(chǎn)生,其安全性得到串空間協(xié)議驗證技術(shù)[9,10]的證明;組合設(shè)計過程的安全性已經(jīng)在安全協(xié)議組合設(shè)計與分析理論[11,12]中得到證明。
(2)設(shè)計效率分析
正確的原語是組合設(shè)計的基礎(chǔ),而傳統(tǒng)的手動設(shè)計過程較為復(fù)雜且容易出錯。通過利用自動生成工具,原語設(shè)計具備較高的質(zhì)量和效率。以非對稱密鑰體制下單向認(rèn)證原語、對稱密鑰體制下帶有可信第三方的單向認(rèn)證且密鑰建立原語、對稱密鑰體制下帶有可信第三方的單向認(rèn)證原語等3個原語的設(shè)計為例,效率數(shù)據(jù)見表1。
表1 效率數(shù)據(jù)
得到正確的原語后,可根據(jù)4類原語可組合元素附加規(guī)則和3類組合設(shè)計規(guī)則,較為便捷地完成復(fù)合協(xié)議設(shè)計,整個過程具備較高的效率。
(3)復(fù)雜度分析
原語的設(shè)計通過自動工具完成,只需在設(shè)計前選中相應(yīng)的安全需求,即可從自動生成的正確結(jié)果中選取合適的原語;接下來通過修改消息項的結(jié)構(gòu),添加可組合元素,使簡單原語可用作組合設(shè)計復(fù)合協(xié)議的基本元素;然后,由于原語已經(jīng)具備了可組合性,組合設(shè)計的復(fù)雜度得到較大降低,只需遵循3條簡單的組合設(shè)計規(guī)則,即可獲得正確的復(fù)合協(xié)議。整個設(shè)計過程便捷可行。
實踐分析結(jié)果表明,新策略同時具備自動設(shè)計正確高效以及組合設(shè)計簡便易行的優(yōu)點,是一種較為可行的、適用于復(fù)合協(xié)議設(shè)計的策略。
提出了一種基于原語自動生成的安全協(xié)議組合設(shè)計新策略,為較大規(guī)模安全協(xié)議的組合設(shè)計提供了新的思路,但也存在需要進(jìn)一步完善的地方。特別是在自動設(shè)計階段,由于受到計算量爆炸和篩選規(guī)則的限制,得到的原語種類有限,主要限于認(rèn)證、秘密傳遞、密鑰建立等,限制了新策略的應(yīng)用范圍。若能進(jìn)一步將原語種類擴展至不可否認(rèn)性、公平性、可追究性等方面,則可在復(fù)合協(xié)議(尤其是電子商務(wù)協(xié)議)的設(shè)計領(lǐng)域發(fā)揮更大的作用。
[1]ZHOU Yajie,GUAN Huanmei,CHEN Ping,et al.Automatic design of security protocols[J].Computer Engineering,2007,33(20):137-138(in Chinese).[周雅潔,關(guān)煥梅,陳萍,等.安全協(xié)議的自動化設(shè)計[J].計算機工程,2007,33(20):137-138.]
[2]LIU Dongmei,QING Sihan,HOU Yuwen,et al.Automatic generation of fair exchange protocol based on fitness function genetic algorithm[J].Chinese Journal of Electronics,2010,38(5):1089-1094(in Chinese).[劉冬梅,卿斯?jié)h,侯玉文,等.一種基于適應(yīng)度函數(shù)遺傳算法的公平交換協(xié)議自動生成方法[J].電子學(xué)報,2010,38(5):1089-1094.]
[3]LI Xiaole,DONG Rongsheng,WU Guangwei.Design and verification of secure payment protocol based on composition method[J].Journal of Guangxi Academy of Sciences,2007,23(4):287-291(in Chinese).[李曉樂,董榮勝,吳光偉.基于組合設(shè)計方法的安全支付協(xié)議的設(shè)計與驗證[J].廣西科學(xué)院學(xué)報,2007,23(4):287-291.]
[4]XIE Hongbo,WU Yuancheng,LIU Yijing,et al.A study on the combined analysis model of security protocols[J].Acta Electronica Sinica,2008,36(11):2262-2267(in Chinese).[謝鴻波,吳遠(yuǎn)成,劉一靜,等.一種安全協(xié)議的組合分析模型研究[J].電子學(xué)報,2008,36(11):2262-2267.]
[5]XIONG Weijian,LI Xiaole,LUO Yongjun.Design and verification of security protocol of information transmission for teaching affairs administration system[J].Computer Applications and Software,2009,26(8):113-114(in Chinese).[熊偉建,李曉樂,羅擁軍.教務(wù)管理系統(tǒng)中信息傳輸安全協(xié)議的設(shè)計與驗證[J].計算機應(yīng)用與軟件,2009,26(8):113-114.]
[6]DENG Fan,DENG Shaofeng,LI Yifa.Security protocol design by composition method[J].Journal of Computer Applications,2010,30(4):1033-1037(in Chinese).[鄧帆,鄧少鋒,李益發(fā).應(yīng)用組合方法設(shè)計安全協(xié)議[J].計算機應(yīng)用,2010,30(4):1033-1037.]
[7]YANG Fan,LI Tong,CAO Qiying.Security protocol for ubiquitous computing network design by composition method[J].Application Research of Computers,2009,26(3):1073-1075(in Chinese).[楊帆,李彤,曹奇英.應(yīng)用組合方法設(shè)計普適計算網(wǎng)絡(luò)安全協(xié)議[J].計算機應(yīng)用研究,2009,26(3):1073-1075.]
[8]YU Lei,WEI Shimin.Analysis on properties for principals'keys on construction of test components[J].Computer Engineering and Applications,2013,49(6):114-117(in Chinese).[余磊,魏仕民.協(xié)議主體密鑰在測試組件構(gòu)造上的性質(zhì)分析[J].計算機工程與應(yīng)用,2013,49(6):114-117.]
[9]WU Xiaoying,ZHOU Qinglei.Kind of automated analysis method of security protocol[J].Application Research of Computers,2010,27(6):2301-2303(in Chinese).[毋曉英,周清雷.一種安全協(xié)議自動化分析方法[J].計算機應(yīng)用研究,2010,27(6):2301-2303.]
[10]ZHANG Xiaohong,LI Xiehua.Automatic verification algorithm for security protocol based on string space[J].Computer Engineering,2011,37(5):131-133(in Chinese).[張孝紅,李謝華.基于串空間的安全協(xié)議自動化驗證算法[J].計算機工程,2011,37(5):131-133.]
[11]WANG Huibin,ZHU Yuefei,CHANG Qingmei.Study of protocol composition logic[J].Journal of Zhengzhou University(Nat Sci Ed),2008,40(4):56-59(in Chinese).[王惠斌,祝躍飛,常青美.協(xié)議組合邏輯系統(tǒng)研究[J].鄭州大學(xué)學(xué)報(理學(xué)版),2008,40(4):56-59.]
[12]JIA Hongyong,QING Sihan,GU Lize,et al.Universally composable group key exchange protocol[J].Journal of Electronics &Information Technology,2009,31(7):1571-1575(in Chinese).[賈洪勇,卿斯?jié)h,谷利澤,等.通用可組合的組密鑰交換協(xié)議[J].電子與信息學(xué)報,2009,31(7):1571-1575.]