基于原語自動生成的安全協議組合設計策略及應用研究

李曉樂，翁 鳴，羅應機，文 英

（1.廣西財經學院實驗教學中心，廣西南寧530003；2.中國移動通信集團廣西分公司，廣西南寧530022）

0 引 言

協議自動生成機制［1，2］能夠提高安全協議設計的效率和質量，但應用范圍有限，可以結合組合設計方法［3－5］進行復合協議的設計，但是必須確保各原語具備可組合性。針對此問題的研究有“應用環境相符”、“安全目標相容”、“避免符號重復”、“選擇無干擾性原語”、“規范符號描述”等規則［6，7］，屬于協議表示符號的規范性約束，不能保證原語本身的可組合性，若在組合設計過程中才進行原語的可組合性設計，必將增加設計過程的復雜度。

應該通過改進原語結構，比如添加可組合元素等方式，實現原語的可組合性，并有效降低針對多個原語組合設計過程的復雜度。因此構建了一種基于原語自動生成的安全協議組合設計的新策略，提出了新的可組合元素附加規則和組合設計規則，進行了應用研究，通過實例說明了策略的可行性；最后給出了總結和展望。

1 策略模型構建

該組合設計策略模型分為原語自動設計、可組合元素附加和原語組合設計3個模塊，如圖1所示。

圖1 策略模型

（1）原語自動設計:利用自動生成工具，首先將安全需求和系統規格輸入到生成器中；然后基于系統規格對原語空間進行搜索，產生候選原語和每個原語的驗證條件；最后對每個原語的驗證條件進行校驗并輸出正確結果。

（2）可組合元素附加:根據4類新的原語可組合元素附加規則（“參與方－秘密項綁定規則”、“多回合抗干擾規則”、“認證性可組合規則”、“保密性可組合規則”等），通過修改原語中消息的結構，添加可組合元素，使簡單原語可用作組合設計復合協議的基本元素，為后續的組合設計提供正確性保障并降低復雜度，也可驗證原語的可組合性。

（3）原語組合設計:根據針對可組合性原語的新組合設計規則，確定多事件組合順序、合并相似消息并消除冗余信息。

2 可組合元素附加規則

通過自動化設計工具，可以高效生成滿足單個安全目標的簡單原語。然而將多個簡單原語組合為復合協議時，必須考慮到原語組合可能造成不同原語的安全屬性互相影響甚至破壞。為保證原有的安全性，基于串空間和認證測試，提出了新的針對簡單原語的4類可組合元素附加規則，通過修改原語中項的結構，在原語中添加可組合元素，使簡單原語可用作組合設計復合協議的基本元素，為后續的組合設計過程提供正確性保障和降低復雜度。

2.1 參與方－秘密項綁定規則

為保障多原語組合設計的安全性，當原語中的參與者在一個協議回合中產生了一個秘密時，需要將這個秘密關聯到相應的參與者上。若參與者與秘密之間的綁定缺失，往往導致協議存在安全缺陷，遭到類似于針對NSPK協議的中間人攻擊:

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

參與方－秘密項綁定規則:若在加密信息中包含秘密x，則必須同時包含x的綁定組。

在該規則的保護下，協議中的發起者發送包含秘密及其綁定組的一則消息，然后收到一則來自響應者的消息，對項綁定進行確認。每則挑戰消息都明確發送者和接收者，不論響應者在何時創建了一個回復，都明確表達消息的含義。

2.2 多回合抗干擾規則

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

P1和P2在作為獨立的協議時不會互相影響，但是作為P的一部分組合在一起時，卻產生互相干擾。若A收到形如M2或N2的消息，那么該消息既可以解釋為原語P1的一個回合中的消息（在該回合中扮演發起者的角色），又可以解釋為原語P2的一個回合中的消息（在該回合中扮演響應者的角色）。干擾產生的原因是原語中存在相似的認證消息結構，導致組合產生的協議面臨剪切攻擊和粘貼攻擊的威脅。因此需要在認證消息項中添加索引或相關參與者名稱，用以區分不同的原語，如下所示:

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

多回合抗干擾規則:針對同一個會話中同時運行的多個原語，為所有的結構相似的認證消息項添加一個唯一的索引值或相關主體名稱。

在該規則的保護下，即使存在多條類似結構的認證消息，也可根據索引或參與者名稱標明不同的消息屬于哪個原語，避免相似消息間的混亂。為保證抗干擾的有效性，索引或參與者名稱需要插入到發生密碼學轉換的消息中。

2.3 認證性可組合規則

使認證可組合的兩個最重要的屬性是不可構造性和不可破壞性，因此分別從這兩個屬性出發建立規則，實現原語認證性的可組合。

2.3.1 不可構造性規則

采用一致性測試［8］作為認證機制后可以確保認證性的不可構造性，因此提出不可構造性規則如下:

認證性可組合規則1（不可構造性規則）:

（1）作為一個挑戰，以明文的形式發送現時值，在隨后以加密的形式收到，且加密密鑰為對稱密鑰體制下雙方共享的保密密鑰或非對稱密鑰體制下響應者獨有的簽名密鑰；

（2）在同一協議回合中，發起者與響應者的角色唯一對應且在與所有變量相關的數據值上達成一致。

2.3.2 不可破壞性規則

認證目標的不可破壞性與用于認證的長期值和短期值的保密性相關。但是同一個現時值的兩次使用也可能破壞認證性目標，不應在對超過一個參與者的認證中使用相同的現時值。因此提出不可破壞性規則如下。

認證性可組合規則2（不可破壞性規則）:確保長期密鑰安全，且同一個現時值不用于對兩個以上不同參與者認證。

2.3.3 保密性可組合規則

保密性可組合問題包括長期秘密和短期秘密的可組合。每一個協議回合中，參與者的長期秘密（如簽名密鑰和解密密鑰）和回合的短期秘密（如對稱密鑰和傳遞的秘密）都不能被入侵者分析得到，因此提出保密性可組合規則如下:

保密性可組合規則:不能將長期秘密用作現時值或短期秘密，且任何長期和短期秘密的保護域Sx都是I兼容的。

3 原語組合設計規則

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

3.1 事件組合順序規則

事件組合順序規則:

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

（2）不同原語相似事件的組合順序由主體在協議中扮演的角色決定，發起者事件的優先級高于響應者相似事件。

3.2 消息合并規則

消息合并規則:

（1）不同原語的多個協議步合并時，從第一個擁有相同的消息發送者和接收者的消息開始依次合并；

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

3.3 冗余信息消除規則

冗余信息消除規則:

（1）同一步協議中，內容或功能重復的項只保留一個；若某個明文字段在該消息項的加密字段中亦出現，則刪去該明文字段。

（2）不同協議步中，內容或功能重復的消息項可以互相替換。

4 策略應用研究

基于策略模型，進行了應用研究，分別設計出了非對稱密鑰體制下雙向認證協議和對稱密鑰體制下雙向認證及密鑰建立協議。實踐結果表明，該策略同時具備自動設計正確高效以及組合設計簡便易行的優點。

4.1 非對稱密鑰體制下兩方認證協議的組合設計

（1）非對稱密鑰體制下單向認證原語的自動設計

使用協議自動生成工具設計非對稱密鑰體制下單向認證原語可得:

轉化為標準協議工程符號形式，得到原語P1如下:

同理，得到原語P2如下:

（2）原語可組合元素附加

根據協議的設計目標和原語結構，為使原語P1和P2具備可組合性，需要根據“參與方－秘密綁定規則”、“多回合抗干擾規則”、“認證性可組合規則”、“保密性可組合規則”等新提出的4類原語可組合元素附加規則，修改某些消息項的結構，使原語具備可組合性:

1）根據“參與方－秘密項綁定規則”，由于原語P1和P2中的現時值用于單向認證，不作為交換的秘密，因此無需在加密消息項中添加針對秘密的綁定組信息。

2）根據“多回合抗干擾規則”，原語P1和P2均使用結構相似的認證消息項完成單向認證，針對同一個會話中應同時進行的多個原語，為認證消息項中的現時值添加一個唯一的索引值（或主體名稱）。修改后的原語P11和P21如下:

3）根據“認證性可組合規則1”，原語P11和P21的消息項結構滿足不可構造性；根據“認證性可組合規則2”，兩次單向認證不能使用相同的現時值，修改原語P12如下:

同理，得到原語P22如下:

4）根據“保密性可組合規則”，由于原語P1和P2中的現時值用于單向認證，不作為交換的秘密，也未將長期密鑰用作現時值或短期秘密，因此無需對消息項進行修改。

（3）原語組合設計

1）根據事件組合順序規則，確定時間組合順序。

首先注明原語P12和P22中的各事件:

確定事件順序為:

2）根據“消息合并規則”，令P＝P12P22。

首先合并不同原語的多個協議步:

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

3）根據“冗余信息消除規則”，消減同一步協議中內容或功能重復的消息項，替換不同協議步中功能重復的消息項，可得非對稱密鑰體制下兩方認證協議如下:

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

4.2 對稱密鑰體制下帶有可信第三方的兩方認證且密鑰建立協議的組合設計

（1）對稱密鑰體制下帶有可信第三方的單向認證且密鑰建立原語的自動設計

使用協議自動生成工具設計對稱密鑰體制下帶有可信第三方的單向認證且密鑰建立原語可得:

轉化為標準協議工程符號形式，得到原語P1如下:

（2）對稱密鑰體制下帶有可信第三方的單向認證原語的自動設計

使用協議自動生成工具設計對稱密鑰體制下帶有可信第三方的單向認證原語可得:

轉化為標準協議工程符號形式，得到原語P2如下:

（3）可組合元素附加

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

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

由于原語P2中的現時值用于單向認證，不作為交換秘密，因此無需在加密消息項中添加針對秘密的綁定組信息。

2）根據“多回合抗干擾規則”，針對同一個會話中應同時進行的多個原語，為所有的結構相似的消息添加一個唯一的索引值，修改后的兩個原語如下:

3）根據“認證性可組合規則1”，原語P12和P21的消息項結構滿足不可構造性；根據“認證性可組合規則2”，原語P12和P21的消息項結構滿足不可破壞性。因此無需修改原語的消息項。

4）根據“保密性可組合規則”，由于原語P12中的現時值用于單向認證，不作為交換的秘密，且對稱密鑰kAB的保護域Sx與I是兼容的，因此無需對消息項進行修改；由于原語P21中的現時值用于單向認證，不作為交換的秘密，也未將長期密鑰用作現時值或短期秘密，因此無需對消息項進行修改。

（4）原語組合設計

1）根據事件組合順序規則，確定時間組合順序。

首先注明原語P12和P21中的各事件:

確定事件順序為:

由于協議的設計目標是在完成雙向認證后建立密鑰，因此有:

2）根據“消息合并規則”，令P＝P12P21。

首先合并不同原語的多個協議步:

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

3）由于組合設計過程中，某些消息項結構發生改變，通過合并加密消息項避免了相似消息項結構帶來的多回合干擾問題，因此索引信息成為冗余。

根據“冗余信息消除規則”，消減同一步協議中內容或功能重復的消息項，替換不同協議步中功能重復的消息項，可得對稱密鑰體制下帶有可信第三方的兩方認證且密鑰建立協議:

4.3 應用效果分析

以下從安全性、設計效率和復雜度的角度，分析新策略的應用效果。

（1）安全性分析

組合設計得到的安全協議，其安全性依賴于單獨原語的安全屬性和組合設計過程的安全性:單獨原語均通過協議自動生成工具產生，其安全性得到串空間協議驗證技術［9，10］的證明；組合設計過程的安全性已經在安全協議組合設計與分析理論［11，12］中得到證明。

（2）設計效率分析

正確的原語是組合設計的基礎，而傳統的手動設計過程較為復雜且容易出錯。通過利用自動生成工具，原語設計具備較高的質量和效率。以非對稱密鑰體制下單向認證原語、對稱密鑰體制下帶有可信第三方的單向認證且密鑰建立原語、對稱密鑰體制下帶有可信第三方的單向認證原語等3個原語的設計為例，效率數據見表1。

表1 效率數據

得到正確的原語后，可根據4類原語可組合元素附加規則和3類組合設計規則，較為便捷地完成復合協議設計，整個過程具備較高的效率。

（3）復雜度分析

原語的設計通過自動工具完成，只需在設計前選中相應的安全需求，即可從自動生成的正確結果中選取合適的原語；接下來通過修改消息項的結構，添加可組合元素，使簡單原語可用作組合設計復合協議的基本元素；然后，由于原語已經具備了可組合性，組合設計的復雜度得到較大降低，只需遵循3條簡單的組合設計規則，即可獲得正確的復合協議。整個設計過程便捷可行。

實踐分析結果表明，新策略同時具備自動設計正確高效以及組合設計簡便易行的優點，是一種較為可行的、適用于復合協議設計的策略。

5 結束語

提出了一種基于原語自動生成的安全協議組合設計新策略，為較大規模安全協議的組合設計提供了新的思路，但也存在需要進一步完善的地方。特別是在自動設計階段，由于受到計算量爆炸和篩選規則的限制，得到的原語種類有限，主要限于認證、秘密傳遞、密鑰建立等，限制了新策略的應用范圍。若能進一步將原語種類擴展至不可否認性、公平性、可追究性等方面，則可在復合協議（尤其是電子商務協議）的設計領域發揮更大的作用。

［1］ZHOU Yajie，GUAN Huanmei，CHEN Ping，et al.Automatic design of security protocols［J］.Computer Engineering，2007，33（20）:137－138（in Chinese）.［周雅潔，關煥梅，陳萍，等.安全協議的自動化設計［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）.［劉冬梅，卿斯漢，侯玉文，等.一種基于適應度函數遺傳算法的公平交換協議自動生成方法［J］.電子學報，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）.［李曉樂，董榮勝，吳光偉.基于組合設計方法的安全支付協議的設計與驗證［J］.廣西科學院學報，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）.［謝鴻波，吳遠成，劉一靜，等.一種安全協議的組合分析模型研究［J］.電子學報，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）.［熊偉建，李曉樂，羅擁軍.教務管理系統中信息傳輸安全協議的設計與驗證［J］.計算機應用與軟件，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）.［鄧帆，鄧少鋒，李益發.應用組合方法設計安全協議［J］.計算機應用，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）.［楊帆，李彤，曹奇英.應用組合方法設計普適計算網絡安全協議［J］.計算機應用研究，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）.［余磊，魏仕民.協議主體密鑰在測試組件構造上的性質分析［J］.計算機工程與應用，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）.［毋曉英，周清雷.一種安全協議自動化分析方法［J］.計算機應用研究，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）.［張孝紅，李謝華.基于串空間的安全協議自動化驗證算法［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）.［王惠斌，祝躍飛，常青美.協議組合邏輯系統研究［J］.鄭州大學學報（理學版），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）.［賈洪勇，卿斯漢，谷利澤，等.通用可組合的組密鑰交換協議［J］.電子與信息學報，2009，31（7）:1571－1575.］