李曉樂(lè)，翁 鳴，羅應(yīng)機(jī)，文 英

（1.廣西財(cái)經(jīng)學(xué)院實(shí)驗(yàn)教學(xué)中心，廣西南寧530003；2.中國(guó)移動(dòng)通信集團(tuán)廣西分公司，廣西南寧530022）

0 引 言

協(xié)議自動(dòng)生成機(jī)制［1，2］能夠提高安全協(xié)議設(shè)計(jì)的效率和質(zhì)量，但應(yīng)用范圍有限，可以結(jié)合組合設(shè)計(jì)方法［3－5］進(jìn)行復(fù)合協(xié)議的設(shè)計(jì)，但是必須確保各原語(yǔ)具備可組合性。針對(duì)此問(wèn)題的研究有“應(yīng)用環(huán)境相符”、“安全目標(biāo)相容”、“避免符號(hào)重復(fù)”、“選擇無(wú)干擾性原語(yǔ)”、“規(guī)范符號(hào)描述”等規(guī)則［6，7］，屬于協(xié)議表示符號(hào)的規(guī)范性約束，不能保證原語(yǔ)本身的可組合性，若在組合設(shè)計(jì)過(guò)程中才進(jìn)行原語(yǔ)的可組合性設(shè)計(jì)，必將增加設(shè)計(jì)過(guò)程的復(fù)雜度。

應(yīng)該通過(guò)改進(jìn)原語(yǔ)結(jié)構(gòu)，比如添加可組合元素等方式，實(shí)現(xiàn)原語(yǔ)的可組合性，并有效降低針對(duì)多個(gè)原語(yǔ)組合設(shè)計(jì)過(guò)程的復(fù)雜度。因此構(gòu)建了一種基于原語(yǔ)自動(dòng)生成的安全協(xié)議組合設(shè)計(jì)的新策略，提出了新的可組合元素附加規(guī)則和組合設(shè)計(jì)規(guī)則，進(jìn)行了應(yīng)用研究，通過(guò)實(shí)例說(shuō)明了策略的可行性；最后給出了總結(jié)和展望。

1 策略模型構(gòu)建

該組合設(shè)計(jì)策略模型分為原語(yǔ)自動(dòng)設(shè)計(jì)、可組合元素附加和原語(yǔ)組合設(shè)計(jì)3個(gè)模塊，如圖1所示。

圖1 策略模型

（1）原語(yǔ)自動(dòng)設(shè)計(jì):利用自動(dòng)生成工具，首先將安全需求和系統(tǒng)規(guī)格輸入到生成器中；然后基于系統(tǒng)規(guī)格對(duì)原語(yǔ)空間進(jìn)行搜索，產(chǎn)生候選原語(yǔ)和每個(gè)原語(yǔ)的驗(yàn)證條件；最后對(duì)每個(gè)原語(yǔ)的驗(yàn)證條件進(jìn)行校驗(yàn)并輸出正確結(jié)果。

（2）可組合元素附加:根據(jù)4類新的原語(yǔ)可組合元素附加規(guī)則（“參與方－秘密項(xiàng)綁定規(guī)則”、“多回合抗干擾規(guī)則”、“認(rèn)證性可組合規(guī)則”、“保密性可組合規(guī)則”等），通過(guò)修改原語(yǔ)中消息的結(jié)構(gòu)，添加可組合元素，使簡(jiǎn)單原語(yǔ)可用作組合設(shè)計(jì)復(fù)合協(xié)議的基本元素，為后續(xù)的組合設(shè)計(jì)提供正確性保障并降低復(fù)雜度，也可驗(yàn)證原語(yǔ)的可組合性。

（3）原語(yǔ)組合設(shè)計(jì):根據(jù)針對(duì)可組合性原語(yǔ)的新組合設(shè)計(jì)規(guī)則，確定多事件組合順序、合并相似消息并消除冗余信息。

2 可組合元素附加規(guī)則

通過(guò)自動(dòng)化設(shè)計(jì)工具，可以高效生成滿足單個(gè)安全目標(biāo)的簡(jiǎn)單原語(yǔ)。然而將多個(gè)簡(jiǎn)單原語(yǔ)組合為復(fù)合協(xié)議時(shí)，必須考慮到原語(yǔ)組合可能造成不同原語(yǔ)的安全屬性互相影響甚至破壞。為保證原有的安全性，基于串空間和認(rèn)證測(cè)試，提出了新的針對(duì)簡(jiǎn)單原語(yǔ)的4類可組合元素附加規(guī)則，通過(guò)修改原語(yǔ)中項(xiàng)的結(jié)構(gòu)，在原語(yǔ)中添加可組合元素，使簡(jiǎn)單原語(yǔ)可用作組合設(shè)計(jì)復(fù)合協(xié)議的基本元素，為后續(xù)的組合設(shè)計(jì)過(guò)程提供正確性保障和降低復(fù)雜度。

2.1 參與方－秘密項(xiàng)綁定規(guī)則

為保障多原語(yǔ)組合設(shè)計(jì)的安全性，當(dāng)原語(yǔ)中的參與者在一個(gè)協(xié)議回合中產(chǎn)生了一個(gè)秘密時(shí)，需要將這個(gè)秘密關(guān)聯(lián)到相應(yīng)的參與者上。若參與者與秘密之間的綁定缺失，往往導(dǎo)致協(xié)議存在安全缺陷，遭到類似于針對(duì)NSPK協(xié)議的中間人攻擊:

在上述協(xié)議回合中，由于｛NA，NB｝eKA里缺少秘密的綁定信息，導(dǎo)致攻擊者I可以假冒A的身份與B進(jìn)行通信，從而得到A與B間的秘密NB。以此為鑒，為有效規(guī)避中間人攻擊等安全威脅，提出參與方－秘密項(xiàng)綁定規(guī)則如下。

參與方－秘密項(xiàng)綁定規(guī)則:若在加密信息中包含秘密x，則必須同時(shí)包含x的綁定組。

在該規(guī)則的保護(hù)下，協(xié)議中的發(fā)起者發(fā)送包含秘密及其綁定組的一則消息，然后收到一則來(lái)自響應(yīng)者的消息，對(duì)項(xiàng)綁定進(jìn)行確認(rèn)。每則挑戰(zhàn)消息都明確發(fā)送者和接收者，不論響應(yīng)者在何時(shí)創(chuàng)建了一個(gè)回復(fù)，都明確表達(dá)消息的含義。

2.2 多回合抗干擾規(guī)則

作為安全基本元素，每個(gè)原語(yǔ)在單獨(dú)運(yùn)行時(shí)不會(huì)干擾其它原語(yǔ)。然而，由于消息的相似性，多個(gè)原語(yǔ)運(yùn)行在同一個(gè)協(xié)議中時(shí)可能互相干擾。以雙向認(rèn)證協(xié)議的組合設(shè)計(jì)為例，P1和P2是兩個(gè)單向認(rèn)證原語(yǔ)，P＝P1P2，其中P1和P2如下所示，x≠y，且βx＝βy＝（A，B）。

P1和P2在作為獨(dú)立的協(xié)議時(shí)不會(huì)互相影響，但是作為P的一部分組合在一起時(shí)，卻產(chǎn)生互相干擾。若A收到形如M2或N2的消息，那么該消息既可以解釋為原語(yǔ)P1的一個(gè)回合中的消息（在該回合中扮演發(fā)起者的角色），又可以解釋為原語(yǔ)P2的一個(gè)回合中的消息（在該回合中扮演響應(yīng)者的角色）。干擾產(chǎn)生的原因是原語(yǔ)中存在相似的認(rèn)證消息結(jié)構(gòu)，導(dǎo)致組合產(chǎn)生的協(xié)議面臨剪切攻擊和粘貼攻擊的威脅。因此需要在認(rèn)證消息項(xiàng)中添加索引或相關(guān)參與者名稱，用以區(qū)分不同的原語(yǔ)，如下所示:

以此為鑒，提出多回合抗干擾規(guī)則如下:

多回合抗干擾規(guī)則:針對(duì)同一個(gè)會(huì)話中同時(shí)運(yùn)行的多個(gè)原語(yǔ)，為所有的結(jié)構(gòu)相似的認(rèn)證消息項(xiàng)添加一個(gè)唯一的索引值或相關(guān)主體名稱。

在該規(guī)則的保護(hù)下，即使存在多條類似結(jié)構(gòu)的認(rèn)證消息，也可根據(jù)索引或參與者名稱標(biāo)明不同的消息屬于哪個(gè)原語(yǔ)，避免相似消息間的混亂。為保證抗干擾的有效性，索引或參與者名稱需要插入到發(fā)生密碼學(xué)轉(zhuǎn)換的消息中。

2.3 認(rèn)證性可組合規(guī)則

使認(rèn)證可組合的兩個(gè)最重要的屬性是不可構(gòu)造性和不可破壞性，因此分別從這兩個(gè)屬性出發(fā)建立規(guī)則，實(shí)現(xiàn)原語(yǔ)認(rèn)證性的可組合。

2.3.1 不可構(gòu)造性規(guī)則

采用一致性測(cè)試［8］作為認(rèn)證機(jī)制后可以確保認(rèn)證性的不可構(gòu)造性，因此提出不可構(gòu)造性規(guī)則如下:

認(rèn)證性可組合規(guī)則1（不可構(gòu)造性規(guī)則）:

（1）作為一個(gè)挑戰(zhàn)，以明文的形式發(fā)送現(xiàn)時(shí)值，在隨后以加密的形式收到，且加密密鑰為對(duì)稱密鑰體制下雙方共享的保密密鑰或非對(duì)稱密鑰體制下響應(yīng)者獨(dú)有的簽名密鑰；

（2）在同一協(xié)議回合中，發(fā)起者與響應(yīng)者的角色唯一對(duì)應(yīng)且在與所有變量相關(guān)的數(shù)據(jù)值上達(dá)成一致。

2.3.2 不可破壞性規(guī)則

認(rèn)證目標(biāo)的不可破壞性與用于認(rèn)證的長(zhǎng)期值和短期值的保密性相關(guān)。但是同一個(gè)現(xiàn)時(shí)值的兩次使用也可能破壞認(rèn)證性目標(biāo)，不應(yīng)在對(duì)超過(guò)一個(gè)參與者的認(rèn)證中使用相同的現(xiàn)時(shí)值。因此提出不可破壞性規(guī)則如下。

認(rèn)證性可組合規(guī)則2（不可破壞性規(guī)則）:確保長(zhǎng)期密鑰安全，且同一個(gè)現(xiàn)時(shí)值不用于對(duì)兩個(gè)以上不同參與者認(rèn)證。

2.3.3 保密性可組合規(guī)則

保密性可組合問(wèn)題包括長(zhǎng)期秘密和短期秘密的可組合。每一個(gè)協(xié)議回合中，參與者的長(zhǎng)期秘密（如簽名密鑰和解密密鑰）和回合的短期秘密（如對(duì)稱密鑰和傳遞的秘密）都不能被入侵者分析得到，因此提出保密性可組合規(guī)則如下:

保密性可組合規(guī)則:不能將長(zhǎng)期秘密用作現(xiàn)時(shí)值或短期秘密，且任何長(zhǎng)期和短期秘密的保護(hù)域Sx都是I兼容的。

3 原語(yǔ)組合設(shè)計(jì)規(guī)則

針對(duì)組合設(shè)計(jì)規(guī)則的研究主要包括單步協(xié)議選取、組合順序、去掉冗余、non－Dos，以及組合順序、替換實(shí)現(xiàn)組合、子協(xié)議合并、消息合并、消息組合等［6，7］。通過(guò)可組合元素附加階段的設(shè)計(jì)，原語(yǔ)已經(jīng)具備了可組合性，組合設(shè)計(jì)的復(fù)雜度得到較大降低，因此組合設(shè)計(jì)過(guò)程比較簡(jiǎn)單，主要考慮多事件順序、相似消息的合并以及冗余信息的消除。

3.1 事件組合順序規(guī)則

事件組合順序規(guī)則:

（1）e＋（x）＜e－（x）且（vx）＜e＋（x），即項(xiàng)x所有的發(fā)送事件都先于接收事件，在生成新變量x之后才能對(duì)其發(fā)送；

（2）不同原語(yǔ)相似事件的組合順序由主體在協(xié)議中扮演的角色決定，發(fā)起者事件的優(yōu)先級(jí)高于響應(yīng)者相似事件。

3.2 消息合并規(guī)則

消息合并規(guī)則:

（1）不同原語(yǔ)的多個(gè)協(xié)議步合并時(shí)，從第一個(gè)擁有相同的消息發(fā)送者和接收者的消息開(kāi)始依次合并；

（2）同一步協(xié)議中，將采用相同加密體制和密鑰的加密消息項(xiàng)合并。

3.3 冗余信息消除規(guī)則

冗余信息消除規(guī)則:

（1）同一步協(xié)議中，內(nèi)容或功能重復(fù)的項(xiàng)只保留一個(gè)；若某個(gè)明文字段在該消息項(xiàng)的加密字段中亦出現(xiàn)，則刪去該明文字段。

（2）不同協(xié)議步中，內(nèi)容或功能重復(fù)的消息項(xiàng)可以互相替換。

4 策略應(yīng)用研究

基于策略模型，進(jìn)行了應(yīng)用研究，分別設(shè)計(jì)出了非對(duì)稱密鑰體制下雙向認(rèn)證協(xié)議和對(duì)稱密鑰體制下雙向認(rèn)證及密鑰建立協(xié)議。實(shí)踐結(jié)果表明，該策略同時(shí)具備自動(dòng)設(shè)計(jì)正確高效以及組合設(shè)計(jì)簡(jiǎn)便易行的優(yōu)點(diǎn)。

4.1 非對(duì)稱密鑰體制下兩方認(rèn)證協(xié)議的組合設(shè)計(jì)

（1）非對(duì)稱密鑰體制下單向認(rèn)證原語(yǔ)的自動(dòng)設(shè)計(jì)

使用協(xié)議自動(dòng)生成工具設(shè)計(jì)非對(duì)稱密鑰體制下單向認(rèn)證原語(yǔ)可得:

轉(zhuǎn)化為標(biāo)準(zhǔn)協(xié)議工程符號(hào)形式，得到原語(yǔ)P1如下:

同理，得到原語(yǔ)P2如下:

（2）原語(yǔ)可組合元素附加

根據(jù)協(xié)議的設(shè)計(jì)目標(biāo)和原語(yǔ)結(jié)構(gòu)，為使原語(yǔ)P1和P2具備可組合性，需要根據(jù)“參與方－秘密綁定規(guī)則”、“多回合抗干擾規(guī)則”、“認(rèn)證性可組合規(guī)則”、“保密性可組合規(guī)則”等新提出的4類原語(yǔ)可組合元素附加規(guī)則，修改某些消息項(xiàng)的結(jié)構(gòu)，使原語(yǔ)具備可組合性:

1）根據(jù)“參與方－秘密項(xiàng)綁定規(guī)則”，由于原語(yǔ)P1和P2中的現(xiàn)時(shí)值用于單向認(rèn)證，不作為交換的秘密，因此無(wú)需在加密消息項(xiàng)中添加針對(duì)秘密的綁定組信息。

2）根據(jù)“多回合抗干擾規(guī)則”，原語(yǔ)P1和P2均使用結(jié)構(gòu)相似的認(rèn)證消息項(xiàng)完成單向認(rèn)證，針對(duì)同一個(gè)會(huì)話中應(yīng)同時(shí)進(jìn)行的多個(gè)原語(yǔ)，為認(rèn)證消息項(xiàng)中的現(xiàn)時(shí)值添加一個(gè)唯一的索引值（或主體名稱）。修改后的原語(yǔ)P11和P21如下:

3）根據(jù)“認(rèn)證性可組合規(guī)則1”，原語(yǔ)P11和P21的消息項(xiàng)結(jié)構(gòu)滿足不可構(gòu)造性；根據(jù)“認(rèn)證性可組合規(guī)則2”，兩次單向認(rèn)證不能使用相同的現(xiàn)時(shí)值，修改原語(yǔ)P12如下:

同理，得到原語(yǔ)P22如下:

4）根據(jù)“保密性可組合規(guī)則”，由于原語(yǔ)P1和P2中的現(xiàn)時(shí)值用于單向認(rèn)證，不作為交換的秘密，也未將長(zhǎng)期密鑰用作現(xiàn)時(shí)值或短期秘密，因此無(wú)需對(duì)消息項(xiàng)進(jìn)行修改。

（3）原語(yǔ)組合設(shè)計(jì)

1）根據(jù)事件組合順序規(guī)則，確定時(shí)間組合順序。

首先注明原語(yǔ)P12和P22中的各事件:

確定事件順序?yàn)?

2）根據(jù)“消息合并規(guī)則”，令P＝P12P22。

首先合并不同原語(yǔ)的多個(gè)協(xié)議步:

然后將同一協(xié)議步中采用相同加密體制和密鑰的加密消息項(xiàng)合并:

3）根據(jù)“冗余信息消除規(guī)則”，消減同一步協(xié)議中內(nèi)容或功能重復(fù)的消息項(xiàng)，替換不同協(xié)議步中功能重復(fù)的消息項(xiàng)，可得非對(duì)稱密鑰體制下兩方認(rèn)證協(xié)議如下:

為增加可讀性，可將索引替換為主體名稱:

4.2 對(duì)稱密鑰體制下帶有可信第三方的兩方認(rèn)證且密鑰建立協(xié)議的組合設(shè)計(jì)

（1）對(duì)稱密鑰體制下帶有可信第三方的單向認(rèn)證且密鑰建立原語(yǔ)的自動(dòng)設(shè)計(jì)

使用協(xié)議自動(dòng)生成工具設(shè)計(jì)對(duì)稱密鑰體制下帶有可信第三方的單向認(rèn)證且密鑰建立原語(yǔ)可得:

轉(zhuǎn)化為標(biāo)準(zhǔn)協(xié)議工程符號(hào)形式，得到原語(yǔ)P1如下:

（2）對(duì)稱密鑰體制下帶有可信第三方的單向認(rèn)證原語(yǔ)的自動(dòng)設(shè)計(jì)

使用協(xié)議自動(dòng)生成工具設(shè)計(jì)對(duì)稱密鑰體制下帶有可信第三方的單向認(rèn)證原語(yǔ)可得:

轉(zhuǎn)化為標(biāo)準(zhǔn)協(xié)議工程符號(hào)形式，得到原語(yǔ)P2如下:

（3）可組合元素附加

同理，為使原語(yǔ)P1和P2具備可組合性，需要添加可組合元素:

1）根據(jù)“參與方－秘密項(xiàng)綁定規(guī)則”，在原語(yǔ)P1包含秘密kAB的加密項(xiàng)中，分別添加kAB的綁定組βSA＝（S，A）和βSB＝（S，B），修改后的原語(yǔ)P11如下:

由于原語(yǔ)P2中的現(xiàn)時(shí)值用于單向認(rèn)證，不作為交換秘密，因此無(wú)需在加密消息項(xiàng)中添加針對(duì)秘密的綁定組信息。

2）根據(jù)“多回合抗干擾規(guī)則”，針對(duì)同一個(gè)會(huì)話中應(yīng)同時(shí)進(jìn)行的多個(gè)原語(yǔ)，為所有的結(jié)構(gòu)相似的消息添加一個(gè)唯一的索引值，修改后的兩個(gè)原語(yǔ)如下:

3）根據(jù)“認(rèn)證性可組合規(guī)則1”，原語(yǔ)P12和P21的消息項(xiàng)結(jié)構(gòu)滿足不可構(gòu)造性；根據(jù)“認(rèn)證性可組合規(guī)則2”，原語(yǔ)P12和P21的消息項(xiàng)結(jié)構(gòu)滿足不可破壞性。因此無(wú)需修改原語(yǔ)的消息項(xiàng)。

4）根據(jù)“保密性可組合規(guī)則”，由于原語(yǔ)P12中的現(xiàn)時(shí)值用于單向認(rèn)證，不作為交換的秘密，且對(duì)稱密鑰kAB的保護(hù)域Sx與I是兼容的，因此無(wú)需對(duì)消息項(xiàng)進(jìn)行修改；由于原語(yǔ)P21中的現(xiàn)時(shí)值用于單向認(rèn)證，不作為交換的秘密，也未將長(zhǎng)期密鑰用作現(xiàn)時(shí)值或短期秘密，因此無(wú)需對(duì)消息項(xiàng)進(jìn)行修改。

（4）原語(yǔ)組合設(shè)計(jì)

1）根據(jù)事件組合順序規(guī)則，確定時(shí)間組合順序。

首先注明原語(yǔ)P12和P21中的各事件:

確定事件順序?yàn)?

由于協(xié)議的設(shè)計(jì)目標(biāo)是在完成雙向認(rèn)證后建立密鑰，因此有:

2）根據(jù)“消息合并規(guī)則”，令P＝P12P21。

首先合并不同原語(yǔ)的多個(gè)協(xié)議步:

然后將同一協(xié)議步中采用相同加密體制和密鑰的加密消息項(xiàng)合并:

3）由于組合設(shè)計(jì)過(guò)程中，某些消息項(xiàng)結(jié)構(gòu)發(fā)生改變，通過(guò)合并加密消息項(xiàng)避免了相似消息項(xiàng)結(jié)構(gòu)帶來(lái)的多回合干擾問(wèn)題，因此索引信息成為冗余。

根據(jù)“冗余信息消除規(guī)則”，消減同一步協(xié)議中內(nèi)容或功能重復(fù)的消息項(xiàng)，替換不同協(xié)議步中功能重復(fù)的消息項(xiàng)，可得對(duì)稱密鑰體制下帶有可信第三方的兩方認(rèn)證且密鑰建立協(xié)議:

4.3 應(yīng)用效果分析

以下從安全性、設(shè)計(jì)效率和復(fù)雜度的角度，分析新策略的應(yīng)用效果。

（1）安全性分析

組合設(shè)計(jì)得到的安全協(xié)議，其安全性依賴于單獨(dú)原語(yǔ)的安全屬性和組合設(shè)計(jì)過(guò)程的安全性:單獨(dú)原語(yǔ)均通過(guò)協(xié)議自動(dòng)生成工具產(chǎn)生，其安全性得到串空間協(xié)議驗(yàn)證技術(shù)［9，10］的證明；組合設(shè)計(jì)過(guò)程的安全性已經(jīng)在安全協(xié)議組合設(shè)計(jì)與分析理論［11，12］中得到證明。

（2）設(shè)計(jì)效率分析

正確的原語(yǔ)是組合設(shè)計(jì)的基礎(chǔ)，而傳統(tǒng)的手動(dòng)設(shè)計(jì)過(guò)程較為復(fù)雜且容易出錯(cuò)。通過(guò)利用自動(dòng)生成工具，原語(yǔ)設(shè)計(jì)具備較高的質(zhì)量和效率。以非對(duì)稱密鑰體制下單向認(rèn)證原語(yǔ)、對(duì)稱密鑰體制下帶有可信第三方的單向認(rèn)證且密鑰建立原語(yǔ)、對(duì)稱密鑰體制下帶有可信第三方的單向認(rèn)證原語(yǔ)等3個(gè)原語(yǔ)的設(shè)計(jì)為例，效率數(shù)據(jù)見(jiàn)表1。

表1 效率數(shù)據(jù)

得到正確的原語(yǔ)后，可根據(jù)4類原語(yǔ)可組合元素附加規(guī)則和3類組合設(shè)計(jì)規(guī)則，較為便捷地完成復(fù)合協(xié)議設(shè)計(jì)，整個(gè)過(guò)程具備較高的效率。

（3）復(fù)雜度分析

原語(yǔ)的設(shè)計(jì)通過(guò)自動(dòng)工具完成，只需在設(shè)計(jì)前選中相應(yīng)的安全需求，即可從自動(dòng)生成的正確結(jié)果中選取合適的原語(yǔ)；接下來(lái)通過(guò)修改消息項(xiàng)的結(jié)構(gòu)，添加可組合元素，使簡(jiǎn)單原語(yǔ)可用作組合設(shè)計(jì)復(fù)合協(xié)議的基本元素；然后，由于原語(yǔ)已經(jīng)具備了可組合性，組合設(shè)計(jì)的復(fù)雜度得到較大降低，只需遵循3條簡(jiǎn)單的組合設(shè)計(jì)規(guī)則，即可獲得正確的復(fù)合協(xié)議。整個(gè)設(shè)計(jì)過(guò)程便捷可行。

實(shí)踐分析結(jié)果表明，新策略同時(shí)具備自動(dòng)設(shè)計(jì)正確高效以及組合設(shè)計(jì)簡(jiǎn)便易行的優(yōu)點(diǎn)，是一種較為可行的、適用于復(fù)合協(xié)議設(shè)計(jì)的策略。

5 結(jié)束語(yǔ)

提出了一種基于原語(yǔ)自動(dòng)生成的安全協(xié)議組合設(shè)計(jì)新策略，為較大規(guī)模安全協(xié)議的組合設(shè)計(jì)提供了新的思路，但也存在需要進(jìn)一步完善的地方。特別是在自動(dòng)設(shè)計(jì)階段，由于受到計(jì)算量爆炸和篩選規(guī)則的限制，得到的原語(yǔ)種類有限，主要限于認(rèn)證、秘密傳遞、密鑰建立等，限制了新策略的應(yīng)用范圍。若能進(jìn)一步將原語(yǔ)種類擴(kuò)展至不可否認(rèn)性、公平性、可追究性等方面，則可在復(fù)合協(xié)議（尤其是電子商務(wù)協(xié)議）的設(shè)計(jì)領(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é)議的自動(dòng)化設(shè)計(jì)［J］.計(jì)算機(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é)議自動(dòng)生成方法［J］.電子學(xué)報(bào)，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）.［李曉樂(lè)，董榮勝，吳光偉.基于組合設(shè)計(jì)方法的安全支付協(xié)議的設(shè)計(jì)與驗(yàn)證［J］.廣西科學(xué)院學(xué)報(bào)，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é)報(bào)，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）.［熊偉建，李曉樂(lè)，羅擁軍.教務(wù)管理系統(tǒng)中信息傳輸安全協(xié)議的設(shè)計(jì)與驗(yàn)證［J］.計(jì)算機(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è)計(jì)安全協(xié)議［J］.計(jì)算機(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è)計(jì)普適計(jì)算網(wǎng)絡(luò)安全協(xié)議［J］.計(jì)算機(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é)議主體密鑰在測(cè)試組件構(gòu)造上的性質(zhì)分析［J］.計(jì)算機(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é)議自動(dòng)化分析方法［J］.計(jì)算機(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é)議自動(dòng)化驗(yàn)證算法［J］.計(jì)算機(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é)報(bào)（理學(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é)報(bào)，2009，31（7）:1571－1575.］