面向远程证明的安全协议设计方法.doc

第10期余荣威等：面向远程证明的安全协议设计方法25面向远程证明的安全协议设计方法余荣威1，王丽娜1, 2，匡波1（1. 武汉大学 计算机学院，湖北 武汉 430072；2. 武汉大学 空天信息安全与可信计算教育部重点实验室，湖北 武汉 430072）摘 要：通过引入优胜劣汰的自然规律，提出了改进的基于演化计算的密码协议自动化设计方法。该方法采用模态逻辑作为描述协议的基本工具，重点改进了衡量安全协议个体性能的评估函数，以求获得全局最优解。实验结果显示，该方法能保证所设计协议的正确性和安全性，具有较强的可行性和适用性。关键词：远程证明；认证协议；演化计算；BAN逻辑中图分类号：TP309 文献标识码：A 文章编号：1000-436X(2008)10-0019-06Method of designing security protocol for remote attestationYU Rong-wei1, WANG Li-na1, 2, KUANG Bo1(1. School of Computer, Wuhan University, Wuhan 430072, China;2. Key Laboratory of Aerospace Information Security and Trust Computing，Ministry of Education, Wuhan University, Wuhan 430072, China)Abstract: By the introduction of the natural law of survival of the fittest, an improved method of automatically designing cryptographic protocols was proposed. This method regards BAN-like logic as a basic tool to describe them, construct a fitness function to assess the performance of individuals systematically in order to reach the best solutions. The result shows the method can assure correctness and security of the designed protocol. Furthermore, it has a strong feasibility and applicability.Key words: remote attestation; verification protocol; evolution computing; BAN-like logic1 引言近年来，信息安全事件仍呈上升趋势，形势尤为严峻。据“2007年度全国信息网络安全状况暨计算机病毒疫情调查”调查结果显示1：我国信息网络安全事件发生比例连续3年呈上升趋势，其中2007年达到65.7%，较2006年上升11.7%。信息安全事关国家安全和社会稳定，必须采取综合措施确保信息网络安全。收稿日期：2008-06-21；修回日期：2008-09-25基金项目：国家自然科学基金资助项目（90718006，60743003）；国家高技术研究发展计划（“863”计划）基金资助项目（2008AA01Z404）；国家重点基础研究发展计划（“973”计划）基金资助项目（2007CB310801）Foundation Items: The National Natural Science Foundation of China ( 90718006,60743003); The National High Technology Research and Development Program of China(863 Program)( 2008AA01Z404); The National Basic Research Program of China (973 Program) ( 2007CB310801)可信计算旨在从源头上保证新型计算所基于的网络节点的安全性，即确保终端计算平台的可信问题。TCG用实体行为的预期性给出了可信的解释，其定义为：如果一个实体的行为总是以预期的方式并朝着预期的目标运行，则认为该实体是可信的2。其基本思路是3：通过引入信任根，建立一条信任链，一级测量认证一级，一级信任一级，把信任关系扩大到整个计算机系统，从而确保计算机系统的可信。远程证明机制是实现可信网络连接并使信任能够在网络环境下传递及构建新一代高可信网络的方法，一直是学术界和工业界关注的焦点。文献4认为一个可信的网络应该是网络系统的行为及结果是可以预期的，能够做到行为状态可监测、行为结果可评估、异常行为可控制。TCG5提出了可信网络连接的技术规范；思科公司提出了网络接入控制方案；微软公司也提出了网络接入保护方案；许多研究机构对远程证明也做了大量研究，其中较为典型的有IBM的远程证明系统6；基于属性的证明7，达特茅斯大学的Enforcer/Bear隔离证明方案8；卡内基梅隆大学的基于软件的证明；斯坦福大学的Terra体系结构下基于可信虚拟机监控器的应用程序证明9；中国科学院的验证方主导的远程证明方案10；沈昌祥院士11提出了基于系统行为的计算平台可信证明方案。密码协议是实现远程证明的基础。鉴于自动化设计方法的高效性和正确性等优点，国内外已有一些初步研究。文献12介绍了基于经典迭代深化搜索算法的方法来设计安全协议，该方法使用穷尽搜索，效率太低，候选协议空间非常巨大，且其中大多数候选协议是无意义的,通常只能生成一些简单类型的协议；文献13介绍了基于人工智能规划的方法来设计安全协议，该方法不考虑原子性等性质；文献14采用了超启发式搜索技术，搜索和收敛速度较快，生成的协议效率较高、冗余性较小。国内学者在这方面的工作主要有：武汉大学张焕国等人在Clark和Jacob1518提出的启发式算法基础上，将安全协议的设计划分为2个阶段；中国科技大学的毛晨晓19提出了一种基于协同进化的安全协议生成算法，但是仍然存在演化算子选择和对个体的评估策略单一、评估函数有待优化等问题。针对现有方法演化算子及评估策略的单一，不利于得出协议最优解。本文提出一种改进的基于演化计算的安全协议自动设计方法，采用从安全效率等方面度量演化个体的性能，并同时应用遗传、交叉和变异操作算子设计协议，避免陷入局部最优解。实验结果显示：该方法具有较强的可行性和适用性。2 远程证明远程证明是可信计算中最重要的特性之一，证明方通过可信平台模块（TPM, trusted platform module）的身份密钥，向验证方证明其身份和平台状况。基本原理是：可信计算平台借助可信度量功能对系统平台配置进行度量，并将度量结果保存在PCR中，系统平台通过系统配置向远程通信方证明自身运行环境安全可信。其证明方与验证方的证明流程如图1所示。图1 基于完整性的远程证明流程不妨作如下假定：Attester： 证明方；Verifier：验证方；Sigmsk：表示私钥对消息m的签名；AIK （attestation identity key）:为TPM的身份密钥；SML：存储度量日志（storage measurement log）。故此，基本原理可形式化描述如下。Step1 Verifier：生成一个160bit的随机数Nonce；Step2 Verifier Attester: Nonce；Step3 Attester Verifier: SigPCR, NonceAIK , SML, Cert ( AIKpub )；Step4 Verifier：首先验证Cert ( AIKpub )，其次验证Sig PCR, Nonce AIK，最后检验Nonce的新鲜性并通过PCR值验证SML的一致性。3 基于演化计算的生成算法3.1 协议的描述和验证方法本文采用基于知识和信念的模态逻辑20来描述和验证协议。模态逻辑能够准确地描述安全协议需求，也容易描述协议本身。模态逻辑方法比较成熟、严谨、直观、简洁且易于使用，容易实现自动化，它处于较高层次，能有效降低安全协议生成问题的复杂度。首先，BAN类逻辑将协议理想化为逻辑公式和术语，每个主体都有一个包含有术语集合和逻辑公式集合的状态列表。协议执行过程中，当主体收到一条消息，将消息解码后应用BAN逻辑推理规则进行推理，得到新的术语或逻辑公式，更新它的状态列表。协议执行完毕后，如果主体经更新的状态列表中包含有目标术语和公式，则认为协议能够达成安全目标，即认为协议是安全的。BAN逻辑的语法、语义和我们所使用的主要逻辑推理规则如下：3.1.1 语法语义1) ：主体P相信公式X是真的。2) ：主体P接收到了包含X的消息，即存在某主体向P发送了包含X的消息。3) ：主体P曾经发送过包含X 的消息。4) ：主体P对X有管辖权。5) ：X是新鲜的，即X没有在当前回合前作为某消息的一部分被发送过，这里X一般为临时值。6) ：是P和之间的共享密钥，除P和以及他们相信的主体之外，其他主体都不知道。7) ：为P的公钥，且除了P和他相信的主体之外，其他主体都不知道相应的私钥。8) ：用密钥K加密X后得到的密文。3.1.2 推理规则1) 消息含义规则(message-meaning rule)其含义是：如果P相信K为P和Q之间的共享密钥，且P收到用K加密X的消息XK，则P相信Q发送过消息X。利用消息含义规则，主体P可以从加密消息所使用的密钥或消息中包含的其他秘密来推断消息发送者的身份。对于公钥情形有类似的推理规则，表示如下：2) 临时值验证规则(nonce-verification rule)其含义是，如果P相信消息X是新的，且P相信Q曾发送过X，则P相信Q相信X。利用临时值验证规则，主体P可以从其他主体发送过的消息来推知其他主体的信念，是惟一由“说过”推出“相信”的规则，要求X必须为明文。在对每条消息自动更新信念集合时，应该首先使用消息含义规则，解密后再使用临时值验证规则。3) 管辖权规则(jurisdiction rule)其含义是：如果P相信对消息X有管辖权，且P相信Q信X，则P相信X。利用管辖权规则，主体P可以从其他主体的信念来推知自己的信念。3.2 生成算法流程本文采用演化计算21对生成的候选协议空间进行搜索。下面给出算法流程、染色体编码方案以及适应度函数的选取。其安全协议演化生成算法流程如图2所示。图2 安全协议演化生成流程不妨假定InitialSeed为初始种群，Father为父代种群，Son为子代种群，Cross为交叉算子，Mutate为变异算子。故生成算法具体步骤为：Step1 确定初始假设和安全目标；Step2 根据BAN类逻辑描述初始化假设和安全目标；Step3 随机或选取用来演化的初始协议种群；Step4 ；Step5 使用交叉和变异算子对种群进行演化操作，即 Step6 将变异后的个体与父代中个个体组成子代种群Step7 对生成的子代个体进行适应度评估；Step8 根据适应度值，选择适应度高的组成下一轮父代个体；Step9 判断是否满足终止条件，如满足则输出，否则继续Step5。3.3 染色体编码方案安全协议由一个消息序列构成，每条消息包含发送者、接收者以及消息内容3个部分，其中消息内容部分由若干信念组成。那么，根据所要设计的安全协议的参与方的多少和协议的规模，可以对通信方进行编码。比如，设有N个通信方，则分别对应于整数0到N-1；设每个通信方有T个信念，则分别对应于整数0到T-1。这样就从逻辑上用整数对应了消息的每个成分。然后，对每个消息成分，将整数转化为二进制位串，那么安全协议空间就映射到二进制编码空间了，可以方便地对二进制编码空间进行演化，给出的编码方案如图3所示。图3 染色体编码方案染色体的长度位。对于设计一般的简单安全协议，参与方不多，可以取n =4。每条消息发送的信念数目不宜过大或过小，过大则冗余度高，过小则难以达成安全目标。对染色体进行解码并验证的过程如下：1) 初始化主体的术语和公式集合，设置协议的目标集合。2) 依次对每条消息进行解码，得到发送方、接收方以及消息内容（信念），然后通过BAN逻辑推理规则进行推理，更新接收主体信念状态列表。第i条消息处理完毕后，检查各个主体信念状态集合中协议目标达成数。3.4 评估函数评估函数用来评价演化过程中个体的好坏，是算法的关键。评价协议的好坏应考虑安全性、效率以及冗余度等因素，其中安全性是重点，即协议必须达到所有安全目标。为更好地评价协议的好坏，给出以下形式的评估函数：(1)其中，用来评价协议的安全性，计算公式为： (2)其中，是常数，是根据第条消息安全目标达成的情况给定的常数，两者之和构成一个权重值，是第条消息处理完毕后安全目标达成数。用来评价协议的效率，计算公式为：(3)这里(4)(5)其中，和k均取负数，为协议的消息数，为协议中进行的加密次数，表示当协议含有过多消息时进行惩罚，表示协议中加密操作过多则进行惩罚。直观上来说，通常协议越短，加密操作越少则协议效率越高，通信代价越小。用来评价协议的冗余度，计算公式为：(6)其中，是整个协议有效的信念总量，是协议消息数，是协议消息的有效信念平均数，bi是第条消息的有效信念含量，表示协议消息数。当某条消息发送了重复的信念时，取负值，即对协议进行惩罚。安全性是安全协议最重要的性质，因此，对协议进行评价的重点在于安全性。对于式(2)，可以设计不同的策略来给定权重值。是常数，可以不变，可以递增，可以递减，也可以根据解码第条消息后安全目标达成的数目给定，比如说达成一个安全目标为500。3.5 操作算子使用交叉和变异两种演化操作，交叉操作的作用是在个体之间交换遗传信息，以产生更加优良的个体；变异操作的作用是保持群体中个体的多样性，克服有可能限于局部解的弊病。4 实验结果与分析本实验基于以上理论，生成一种改进的经典认证协议，检验该方法的可行性。现分别给出初始假设以及以期最终达到的安全目标如下。1) 初始假设 2) 安全目标3) 实验结果与安全分析安全协议生成算法主要有迭代深化搜索算法、人工智能规划算法和标准进化算法，三类算法各有优缺点，生成效率相当。通常情况下，本实验方法与基于标准遗传算法的方法已进行过相关参数比较19，种群越大则越可能得到全局最优解。成功率是衡量算法效率的重要标准，反映出最终成功生成协议数与演化次数的比值关系。为了得出和对协议生成成功率的影响，本实验选取种群规模为，最大演化代数为200。实验结果如表1所示。表1实验结果pml/m2345670.002 50.380.470.360.300.480.360.0050.780.720.610.760.710.650.0100.250.940.920.870.870.430.0150.180.970.990.990.950.970.0200.080.590.960.981.000.97通过以上实验数据，可以得出：当且，有很高的成功率。基于以上结论，设定协议长度是6，每条消息最多包含4个信念，种群规模为200，变异概率，交叉概率，演化达到500代时算法结束。成功生成的认证协议的形式化描述如下：，由此可知，该协议在自动化设计时是通过安全协议验证逻辑（模态逻辑）进行描述的，而模态逻辑是一种专用于安全协议形式化验证的有效方法。每一代都通过评估函数对安全性规则进行评估，从而保证最终生成协议是最优解。因此，在生成过程中，同时进行了协议的安全验证，可以很好地保证所涉及协议的正确性和安全性。5 结束语远程证明作为可信计算的重要特征，是将信任链延展到网络上从而构建高可信网络环境的有效方法。面向远程证明的认证协议设计是实现这一目标的前提基础。本文利用演化计算的方法进行安全协议自动化设计。首先，使用形式化方法描述协议，避免协议描述的无二义性；其次，分别从安全性、效率和冗余多方面入手，重点改进了衡量安全协议个体性能的评估函数；然后，同时选用变异和交叉算子进行演化，避免陷入局部最优解；最后，基于其理论的实验结果表明,该方法是现实有效的。参考文献：1国家计算机病毒应急处理中心. 2007年度全国信息网络安全状况暨计算机病毒疫情调查EB/OL. http:/www.antivirus-china. / content/diaocha2007.htm, 2007.National Computer Virus Emergency Response Center. 2007 national investigation information and network security and the situation of computer virusEB/OL. /content/ diaocha2007.htm, 2007.2Trusted Computing Group. TCG specification architecture overviewEB/OL. http: / /groups/ TCG_ 1_4_Architecture_Overview.pdf,2007.3沈昌祥,张焕国,冯登国等. 信息安全综述J. 中国科学(E辑), 2007,37(2):129-150.SHEN C X, ZHANG H G, FENG D G, et al. Overview of information securityJ. Science in China(Series E:Information Sciences), 2007, 37(2): 129-150. 4林闯, 彭雪海. 可信网络研究J. 计算机学报, 2005, 28(5): 2-9.LIN C, PENG X H. Research on trustworthy networksJ. Chinese Journal of Computers, 2005, 28(5): 2-9.5Trusted Computing Group. TCG trusted network connect TNC architecture for interoperability specification version 1.2 revision 4EB/OL. http: //specs/ TNC/,2007. 6SAILER R, ZHANG X L, JAEGER T, et al. Design and implementation of a TCG-based integrity measurement architectureA. The 13th Usenix Security SymposiumC. San Diego, California, 2004.223-238.7SADEGHI A, STIIBLE C. Property-based attestation for computing platforms: caring about properties, not mechanismsA. New Security Paradigms WorkshopC. Nova Scotia, Canada, 2004. 67-77.8SMITH S W. Trusted Computing Platforms: Design and ApplicationsM. New York: Springer, 2005.9SESHADRI A, PERRIG A, DOOM L, et al. SWATT: software based attestation for embedded devicesA. IEEE Conference of Security & PrivacyC. Oakland CA, 2004. 272-282.10秦宇, 冯登国. 验证方主导的远程证明方案J. 计算机研究与发展, 2006,43 (增刊):87-93.QIN Y, FENG D G. Remote attestation sponsored by verifierJ. Journal of Computer Research and Development, 2006, 43(suppl): 87-93.11李晓勇, 左晓栋, 沈昌祥. 基于系统行为的计算平台可信证明J. 电子学报, 2007,35(7): 20-25.LI X Y, ZUO X D, SHEN C X. System behavior based trustworthiness attestation for computing platformJ. Acta Electronica Sinica, 2007, 35(7): 20-25.12ADRIAN P, DAWN S. A first step towards the automatic generation of security protocolsA. Proceeding of Network and Distributed System SecurityC. 2000.73-83.13RANDY H. Automatic Design of Network Security ProtocolsD. Ann Arbor:University of Michigan, 2002.14CLARK J A, JACOB J L. Searching for a solution: engineering tradeoffs and the evolution of provably secure protocolsA. Proceedings of IEEE Symposium on Research in Security and PrivacyC. 2000. 82-95.15CLARK J A, JACOB J L. Protocols are programs too: the meta-heuristicsearch for security protocolsJ. Information and Software