188宝金博页面版

收稿日期：2014-02-10；修回日期：2014-02-28。 基金项目：国家自然科学基金资助项目（11371003）；广西自然科学基金资助项目（2011GXNSFA018154，2012GXNSFGA060003）；广西区主席科技资金资助项目（10169-1）；广西188宝金博页面版厅科研资助项目（201012MS274）。 作者简介：冉俊轶（1989 - ），男，重庆人，硕士研究生，主要研究方向：形式化验证、网络化软件； 吴尽昭（1965 - ），男，黑龙江齐齐哈尔人，教授，博士生导师，主要研究方向：形式化验证、符号计算、自动化推理、逻辑程序设计。文章编号：1001-9081 （2014）S2-0085-06基于 Spin 的安全协议形式化验证技术冉俊轶 1，4* ，吴尽昭 2，3，4（1. 中国科学院 成都计算机应用研究所，成都 610041； 2. 广西混杂计算与集成电路设计分析重点实验室（广西民族大学），南宁 530000；3. 北京交通大学 计算机与信息技术学院，北京 100044； 4. 中国科学院大学，北京 100049）( *通信作者电子邮箱 rlr2008@163. com)摘 要：针对安全协议的形式化验证问题，运用模型检测方法，以一种改进的入侵者 Promela 语义模型，对双方密钥分配中心协议进行 Spin 模型检测，验证发现其不满足线性时序逻辑（LTL）公式描述的安全性，得到了原协议的安全漏洞。针对该漏洞，提出了一种协议改进方案，并针对改进后的协议，给出新的 Promela 语义模型的建模方法。改进的入侵者模型建模方法比起原方法：模型检测过程中的存储状态数减少，使模型复杂度降低约 40'；迁移状态数减少，使验证效率提升约 44'。关键词：安全协议；形式化验证；Spin 模型检测；Promela 语义模型；LTL 公式；密钥分配中心协议中图分类号：TP301. 2 文献标志码：AFormal verification technologis of security protocol based on SpinRAN Junyi 1, 4* , WU Jinzhao 2, 3, 4(1. Chengdu Institute of Computer Application, Chinese Academy of Sciences, Chengdu Sichuan 610041, China;2. Guangxi Key Labrotary of Hybrid Computation and IC Design Analysis ( Guangxi University for Nationalities) , Nanning Guangxi 530000, China;3. Beijing JiaoTong Unversity School of Computer and Information Technology, Beijing 100044, China;4. University of Chinese Academy of Science, Beijing 100049, China)Abstract: Aiming at the formal verification problem in security protocols, an improved Promela semantic intruder modelwas used to complete the model checking for key distribution center protocol, to find that it does' t meet the security propertydescribed by LTL ( Linear Temporal Logic) formula, and to get a protocol vulnerability. An improvement program againstvulnerability was proposed. A new Promela semantic modeling was put forward for the improved protocol. The improvedintruder modeling method reduces the number of states stored in the model checking, thus the model complexity reduces about40'; and reduces the number of transiations, thus the verification efficiency increases about 44'.Key words: security protocol; formal verification; Spin model checking; Promela semantic model; Linear Timing Logic( LTL) formula; key contribution center protocol0 引言随着计算机网络和通信技术的快速发展，电子政务、电子商务、网上银行等各种网络业务的兴起与发展，使得网络通信中使用的安全协议的设计面临更大挑战。安全 协 议［1 -2］（ Security Protocol）也 称 作 密 码 协 议（Cryptography Protocol），是一种以密码学为基础的协议，它运行在计算机网络或分布式系统中，借助于密码算法来达到密钥分配、身份认证等目标，实现保密性、匿名性、非否认性、公平性等。随着时代的发展、网络应用的升级以及频频出现的网络安全事件，人们对安全协议的安全性要求也日益增强。安全的安全协议是网络通信和应用必不可少的组件之一，它是构筑信息安全体系的基础。可是，实践证明，因为协议目标的难以确定、入侵者模型的复杂性、协议运行环境的复杂性、消息和主体的高并发等原因，使得安全协议的设计面临很大困难，很多协议在使用多年以后才发现攻击漏洞，一个典型的例子是：NSPK 协议［3］ 发表 17 年后，才被 Lowe ［4］ 于 1995 年利用模型检测技术发现一个新的攻击漏洞。很长时间之内，密码学家一直都是依赖经验性的指导原则来设计安全协议，而这种非形式化的方法很容易忽略协议中的一些漏洞，于是开始有了形式化的方法应用于协议的分析与设计过程。1 研究现状形式化方法是通过使用数学符号刻画描述系统性质，从而可以找出系统中的不一致性、歧义性和不完备性的一种方法。现有的一些形式化分析方法都有着各自的局限性，对于安全协议的形式化分析理论和技术还需不断探索。目前主要的安全协议形式化分析方法有 3 类：1）基于知识和信念的形式逻辑方法。该类方法的突出代表是，Burrows，Abadi 和 Needham 以逻辑形 式 方 法 提 出 的 BAN 逻 辑［5］ 。运 用 BAN 逻 辑，对Needham-Schroeder、Kerberos 等几个知名协议进行形式化分析，找出了以前已知和未知的漏洞。BAN 逻辑的设计思想是不追求完美，而注重简洁、实用。其直观性与简单性体现在：不区分看到和理解一条消息；其信念演化过程单调递增；不讨论“可信”和“知识”；假设协议中的主体遵守规则，即为诚实的；假设加密系统是完备的。但是Journal of Computer Applications计算机应用, 2014, 34( S2) : 85 -90 ISSN 1001-9081CODEN JYIIDU 2014-12-15http: / / www. joca. cn