基于原语自动生成的安全协议组合设计策略及应用研究

李晓乐，翁 鸣，罗应机，文 英

（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.］