网格计算中虚拟组织的授权机制

分析了网格计算系统中虚拟组织管理的授权需求,提出使用门限闭包作为网格计算系统中面向虚拟组织的授权服务机制。既分析了门限闭包的适用性,也指出了它在具体实施时所存在的局限性,在此基础上提出一种新的授权服务体系,设计了基于公钥基础设施PKI的访问控制工作协议,并结合现有网格计算系统的安全基础设施设计了相应的授权服务系统架构。该体系通过分离门限闭包策略和实现机制,既保证了对复杂授权策略的处理效率和处理能力,也充分利用了现有网格安全基础设施。     

电子支付协议可追究性的Petri网建模与分析

可追究性是电子支付协议必须满足的安全属性之一,针对电子支付协议,建立了支持支付协议可追究性分析的分层有色Petri网模型,并基于此提出一种对支付协议可追究性分析的一般性方法.Kungpisdan等人曾提出一种可追究性逻辑,证明一个典型的移动支付协议KSL协议满足可追究性.但使用上述所提方法对该协议建模并进行可追究性分析,发现了可追究性逻辑未发现的漏洞,分析例证结果表明了所提方法的有效性.     

基于AKB-OTS的传感器网络广播认证协议

现有的基于一次性签名的传感器网络广播认证协议因存储开销较大,较难适用于大规模尤其是多广播节点网络.提出基于辅助密钥的一次性签名方案(assistant-key based-onetime signature,AKB-OTS),引入辅助密钥和Merkle树机制对HORS进行改进,降低其公钥和私钥尺寸.提出基于AKB-OTS的多广播节点传感器网络广播认证协议.分析和验证表明,本协议存储、通信和计算开销低,能够抵抗穷举、选择明文、DoS等攻击,适用于大规模多广播节点传感器网络.     

不可否认协议形式化分析的Petri网方法

Petri网是一种描述及分析并发行为的工具,在安全协议的形式化分析中得到了广泛的应用,但目前还没有人使用Petri网来分析不可否认协议.本文以一般安全协议的Petri网分析方法为基础,提出了使用Petri网分析不可否认协议的建模及分析方法,该方法可以描述并分析一些其它形式化方法无法描述的协议性质.使用该方法分析J. Zhou和D. Gollmann的公平不可否认协议发现了它议的一个许多其它形式化方法不能发现的已知缺陷.     

基于模型检测的TLS协议实现库安全性分析

针对传统模糊测试方法虽能发现传输层安全性(transport layer security,TLS)协议实现库内存漏洞,但无法找到其中逻辑漏洞的问题,基于模型检测的方法,提取TLS协议实现库的状态机模型,建立协议安全属性模型,寻找协议实现中可能存在的异常行为,实现对协议实现库的自动化和系统化的分析.对利用测试用例生成的...     

基于身份的域间认证及密钥协商协议

基于Shamir的秘密共享思想,提出了一种基于身份的域间认证及密钥协商协议。该协议要求域内节点共同参与共享密钥的生成,解决了现有的两方密钥协商方法用于域间认证,及密钥协商时不能保障代表节点可靠性和普通节点参与度的问题。协议的正确性和安全性分析说明,该协议不仅满足密钥协商的基本安全属性,而且还满足数据保密性、数据完整性、抵抗代表节点假冒和欺骗等安全性要求。与使用现有的两方密钥协商协议进行域间认证及密钥协商相比较,本协议具有更低的通信量和计算量,同时,提高了域内普通节点在密钥协商过程中的参与度。     

BitTorrent协议的Petri网建模方法研究

BitTorrent协议被大规模文件共享、视频点播等P2P应用所广泛采用,但其交互行为复杂且并发度高,难以构建规模适度的形式模型以支持高效可行的协议功能行为分析。基于着色Petri网提出一种BitTorrent协议分层建模方法,给出协议的着色Petn网层次模型,集戍模拟、状态空间分析与模型检验等方法对模型的不同抽象层进行分析。确认协议模型有效性,并验证协议行为满足协议需求。BitTorrent协议的着色Petri网层次模型不但为协议开发提供准确、直观的形式规范说明,而且便于协议行为模拟和协议属性分析,有效缓解大规模系统建模分析过程中存在的状态爆炸问题。     

基于有色Petri网的安全协议安全性仿真

如何验证安全协议的安全性是一项非常重要的工作。提出了一种基于有色Petri网的安全协议形式化描述与安全性仿真验证方法。给出协议的有色Petri网模型,分析协议运行过程中可能出现的不安全状态,利用Petri网的状态可达性判断这些不安全状态是否可达从而验证协议的安全性。针对Diffie-Hellman协议给出了具体的仿真分析过程,证明了这种方法的有效性。     

卫星网络密钥管理模型设计与仿真

密钥管理系统为网络中的各节点提供密钥的分配和更新服务,是实施网络安全服务,保证信息安全的基础.针对卫星网络的结构和通信特点,设计了一种新的包含会话密钥、主密钥和公钥的密钥管理模型.首先,设计了公钥更新协议,并对其安全性进行了分析;其次,通过对比分析,对会话密钥更新和主密钥更新的策略进行了设计,并对其安全性以及效率进行了详细分析.最后,在卫星网络仿真环境下实现了密钥更新过程.结合仿真测试数据,与IBM混合密钥管理模型进行比较,并给出了设计密钥更新策略时的重要参考依据.     

Directed Diffusion协议的安全性分析及改进

针对现有无线传感器网络路由协议存在的安全问题,提出了一种改进的Directed Diffusion路由协议。该协议采用对称加密、消息完整性校验码和短签名技术来实现对协议消息分组的保密性、新鲜性和完整性等安全属性,因而能够在存在主动或被动攻击者的情况下,具有对虚假路由信息、Sybil、确认欺骗等常见路由攻击的抵抗能力。通过增强无线传感器网络路由协议Directed Diffusion的安全性,可以有效地节约网络节点的能量,维持网络服务的持续可用性。通过比较和分析,所提的改进的Directed Diffusion协议是一个有效的安全路由协议,能够在仅增加少量通信和计算复杂度的情况下实现安全路由建立过程。     

Dynamic random channel reservation protocol

1.INTRODUCTION DemandassignmentMACprotocolshavebeenusedin severalstandardizedwirelessnetworks.Itcaneffec tivelyutilizewirelessbandwidthofradiochannelsand supportlargenumbersofstations[1].Priorityaccess withshortdelayispreferredformultimediaapplica tions,suchasvoiceandvideotraffic.Longdelays andpoorservicequalitycouldoccurifthereisnopri oritybetweendifferenttypesoftraffic.Thepriority schemeinthereservationphaseofdemandassign mentMACprotocolisneeded,itcanhelprequestsof multimediatraffict…     

Self Fault-Tolerance of Protocols: A Case Study

1. INTRODUCTIONWith the rapid developmellt of high-speed networks, multimedia communication networks andmobile computer networks, the researching issue related to communication protocol design hasattracted more extensive attention worldwide. Since communication protocols deal with thecomplex issues related to distribution such as communication, concurrency, synchronizationof multimedia and harmonization of processes, their development needs to be tackled byusing sophisticated formal method…     

基于MapInfo电子地图的Paramics仿真基础路网构建

研究了利用Mapinfo电子地图自动提取构建微观交通仿真软件Paramics基础路网的方法。首先利用MapInfo提供的二次开发工具MapX提取出代表路网几何和拓扑的特征点信息,然后对原始的特征点集进行精简近距离点、精简同一直线上点以及精简同一弧上点的操作,最后生成Paramics的路网存储文件和基础路网。根据此方法提高了Paramics基础路网建模的效率,生成的路网与原地图一致,满足微观交通仿真要求。     

基于PES的Petri网可执行模型生成方法

针对体系结构验证评估中可执行模型生成缺乏灵活性和扩展性的问题,提出了一种基于体系结构物理交换规范(physical exchange specification,PES)的Petri网可执行模型生成方法。该方法基于DoDAF 2.0提出的体系结构PES和支持对象化的扩展Petri网标记语言(Petri net markup language,PNML)规范,构建了基于PES的Petri网可执行模型生成框架,通过体系结构模型数据含义与Petri网模型元素之间的语义映射,建立了PES与扩展PNML之间的数据映射规则,并以作战活动模型为例详细说明了数据映射规则和转换算法;最后,以民间海上搜救体系结构为例,验证了所提方法的有效性。该方法实现了灵活、自动化的Petri网可执行模型生成,打破了体现结构建模语言和Petri网模型类型的限制。     

具有语言评价信息的指派问题的求解方法

针对解决具有语言评价信息的多目标指派问题，提出了一种新的求解方法．该方法是采用近年来最新发展的二元语义概念对语言评价信息进行处理和运算．首先，将专家给出的具有语言评价信息的效率矩阵转化为二元语义形式，然后采用二元语义集结算子计算得到综合效率矩阵，通过建立指派问题数学模型并根据二元语义自身特点借助传统指派问题的求解方法得到最优解．该方法具有计算简单和语言信息处理结果准确等特点．最后给出了一个算例．     

The Algorithms for Achieving Global States and Self-Stabilization for Communication Protocols

1.INTRODUCTIONWiththerapiddevelopmentofhigh--speedlletworks,multimediacommunicatiollnetworksandmobilecomputernetworks,theissuerelatedtocommunicationprotocoldesignhasbeenmoreextensivelyattentionbymanypeople.Becausecommunicationprotocolsdealwithcomplexissuesrelatedtodistributionsucllascommllnication,concurrency,syllchronizationofmultimediaandcooperationofprocesses,theirdevelopmentneedstobetackledusingsophisticatedformalmethod[l,2].Whellaprotocolisexecuted,thecooperationofdifferentprocessesin…     

基于三阶累积量奇异值分解的雷达目标识别

基于一维距离像三阶累积量矩阵的奇异值分解 ,由非零奇异值构成奇异值矢量作为正则子空间法的输入 ,提出一种雷达目标一维距离像识别方法 ,对目标进行分类识别。该方法一方面利用三阶累积量提高了抗噪性能 ,同时又使用非零奇异值矢量减少了存储量与运算量。仿真实验结果表明 :在低信噪比 ,该方法的识别率高于特征子空间法     

A QUANTIFIER-ELIMINATION BASED HEURISTIC FOR AUTOMATICALLY GENERATING INDUCTIVE ASSERTIONS FOR PROGRAMS

A method using quantifier-elimination is proposed for automatically generating programinvariants/inductive assertions.Given a program,inductive assertions,hypothesized as parameterizedformulas in a theory,are associated with program locations.Parameters in inductive assertions arediscovered by generating constraints on parameters by ensuring that an inductive assertion is indeedpreserved by all execution paths leading to the associated location of the program.The method can beused to discover loop invariants-properties of variables that remain invariant at the entry of a loop.Theparameterized formula can be successively refined by considering execution paths one by one;heuristicscan be developed for determining the order in which the paths are considered.Initialization of programvariables as well as the precondition and postcondition,if available,can also be used to further refinethe hypothesized invariant.The method does not depend on the availability of the precondition andpostcondition of a program.Constraints on parameters generated in this way are solved for possiblevalues of parameters.If no solution is possible,this means that an invariant of the hypothesizedform is not likely to exist for the loop under the assumptions/approximations made to generate theassociated verification condition.Otherwise,if the parametric constraints are solvable,then undercertain conditions on methods for generating these constraints,the strongest possible invariant of thehypothesized form can be generated from most general solutions of the parametric constraints.Theapproach is illustrated using the logical languages of conjunction of polynomial equations as well asPresburger arithmetic for expressing assertions.