一种基于虚拟组织的网格安全协议形式化验证方法new

《一种基于虚拟组织的网格安全协议形式化验证方法new》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、http://www.paper.edu.cn1一种基于虚拟组织的网格安全协议形式化验证方法赵辉大连理工大学软件学院（116620）E-mail：ZhaoHui_SSdut@Yahoo.com.cn摘要：虚拟组织是网格计算的基本管理单元,而协同计算组是虚拟组织形成的基础.对应于网格计算的复杂性,网格安全协议的分析与证明十分复杂.本文通过引入网格计算信道的概念,在传统StrandSpace理论的基础上提出了一种基于虚拟组织的网格安全协议形式化验证方法,实现了网格环境下多用户协同计算安全协议的分析与证明。关键词：网格;协同计算;形式化分析;虚拟组织;StrandSpace理论

2、1.引言网格是一个继承的计算与资源环境，它协调分布式资源协同使用，使用标准的、开放的、通用的协议和接口并且能够提供非平凡的服务质量。今天的网格遵循新的网格技术规范[1]WSRF(WebServiceResourceFramework)，在WebService的永久无状态服务基础上加入有状态的资源。网格环境下多用户参与的协同计算是网格一个重要的应用方向。在网格环境中，特别是网格多用户协同计算中，安全协议是保证安全性的一种重要手[2]段。对应于网格计算的复杂性，网格环境下安全协议的分析与证明极为复杂。本文提出了一种基于虚拟组织的网格安全协议形式化验证方法，实现了网格环境下多用

3、户协同计算安全协议的分析与证明。在讨论网格安全协议形式化验证方法之前，先介绍虚拟组织。网格通过整合分布在局域网或广域网的资源，使之成为一个巨大的虚拟计算机系统，目的是在大量个体、机构组织等之间利用安全、协同式的资源共享，创建一个动态虚拟组[3]织(VO-VirtualOrganization)。基于这种虚拟动态组织的网格协同计算不仅跨地域，而且延伸到不同的组织、异构的软件硬件平台，为每一个连接到网格的用户提供一个无限的计算能力、沟通协作能力及信息获得能力。在网格协同计算环境下，采用基于虚拟组织的分布式管理模式，它使得作业实体从资源控制、任务调度和管理的复杂工作中解脱出来。

4、为了获得充分而必需的资源，各个VO可以通过使用标准的、开放的、通用的接口进行交互信息，并根据这些信息来协调各自的资源使用策略，避免系统的盲目查找和不合理远程调用的现象，以此大大提高了网格计算的智能性。在地域上分布的异构网格计算环境下能自主地将计算任务从一计算节点迁移到另一计算节点，并可与其它VO组织或资源交互以实现作业和资源的管理和自适应。2.相关工作进展2.1安全协议的形式化分析方法安全协议提供安全服务，是保证系统安全性的基础。但是，设计一个符合系统安全目标的安全协议是十分困难的。因此我们必须借助形式化的方法，对安全协议进行设计和分析。[28]自20世纪70年代末期Do

5、lev-Yao模型被提出以来，安全协议的研究已经成为一个热点，有众多的形式化研究方法涌现出来，其中主要有：(1)基于知识与信念推理的模态逻辑方法模态逻辑方法是分析安全协议最直接最简单的一种方法。它们由一些命题和推理规则组1本课题得到国家自然科学基金的资助。-1-http://www.paper.edu.cn成,命题表示主体的知识或信念，而应用推理规则可以从已知的知识和信念推导出新的知识和信念。[4][5][6][7]在这类方法中,比较有名的有：BAN逻辑，GNY逻辑，AT逻辑，VO逻辑及SVO[8][9][10][11][12]逻辑，Bieber逻辑，Syverson逻辑

6、，Rangan逻辑，Moser逻辑，Yahalom，Klein[13]][14]和Beth的YHK逻辑以及Kessler和Wedel的AUTOLOG逻辑等。(2)基于定理证明的分析方法这种方法可以分为两类，一类是推理构造方法，另一类是证明构造方法。[15]推理构造方法主要包括：Meadows的NRL协议分析器方法，Cervesato等学者的基于[16][17]线性逻辑的协议验证方法，Millen等学者的基于逻辑规则的协议验证方法。[18]Kemmerer等学者研制的InaJo和ITP是证明构造方法的典型代表。这一领域的另一项[19,20]重要工作是Paulson的基于归纳

7、的定理证明方法。他研制的定理证明器Isabelle可以应用归纳方法分析安全协议。(3)Spi演算方法[21]这种方法根据Dolev-Yao模型，假定协议执行的每一步都可能与攻击者的执行步骤交叉。Pi演算是并发计算的基础，它引入了通道和作用域的概念。由于作用域之外的进程不能访问通道，在一定程度上保证了通道通信的安全性。Spi演算对pi演算进行了增强与扩充，增加了支持密码系统的原语，使Spi演算可以描述基于密码系统的安全协议。2.2StrandSpace理论[22-24]StrandSpace理论是由Thaye、Herzog和Gu