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

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

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

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

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

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

基于广义随机Petri 网的供应链建模与分析

考察了基于广义随机Petri网的供应链建模与分析技术,在总结Petri网建立供应链模型优势的基础上,将广义随机Petri网(GSPN)的基本理论应用于供应链系统的建模和性能分析,利用GSPN与马尔可夫链的同构关系,采用Petri网与马尔可夫链理论相结合的供应链性能分析方法,为供应链性能的有效评估提供了理论依据,并通过实例验证,该方法可用于分析供应链模型的时间性能和运作效率,为供应链决策层提供参考.     

着色Petri网的结构展开方法

为提升着色Petri网的设计分析与模型检验能力,讨论了着色Petri网的结构化展开技术.以着色Petri网的令牌单元和绑定单元为基元,通过对着色Petri网展开为普通Petri网的等价性证明,提出了基于着色Petri网关联矩阵和标准元语言的展开规则和规范化步骤.研究结果为着色Petri网到普通Petri网的自动转换过程和着色Petri网验证提供了有力支持.     

基于Petri网的强制访问控制模型及其安全分析

强制访问控制模型(MAC)是一种重要的安全模型.在多级安全的格模型和Bell-LaPadula安全模型的基础上,对MAC安全模型进行了形式化描述,并给出了与其等价的着色Petri网模型.在Petri网状态可达图的基础上,对MAC模型的有关安全属性,如主体访问客体的时序关系,主体访问的可达性,因主体的动态安全级访问而存在的安全隐患以及因主体对客体的间接访问而导致敏感信息的可推测性等进行了较为详细地分析.通过对一个安全模型的范例分析,结果表明基于Petri网的安全模型的分析方法可以充分利用现有的可达图的分析方法来对系统安全模型的有关性质进行分析和验证,能够在安全模型的设计和实现阶段有效地改善系统的总体安全策略.     

基于CPN的排队网模型分析方法

提出一种新的排队网模型分析方法,将排队网络按照一定的规则转化为层次着色Petri网,利用着色Petri网的分析工具CPN-TOOLS在模型中加入Monitor监视器监视网络状态,在仿真过程中收集状态数据进行性能评价.这种方法在分析过程中不会对系统结构进行限制,可以对系统的任何方面进行评价,具有很大的灵活性;层次化模型不限制网络规模,不涉及状态空间问题可以更好的用来求解大规模的排队网络.     

基于广义随机Petri网的SIP的验证和性能分析

在给出会话初始化协议（SIP）的服务工作过程的基础上,建立了SIP的广义随机Petri网模型（GSPN）,利用广义随机Petri网坚实的数学基础和分析技术完成对会话初始化协议的分析验证和性能分析。通过可达性分析、S_不变量分析和T_不变量分析验证了会话初始化协议的有界性、活性、守恒性和循环性。并且构造出与广义随机Petri模型同构的马尔可夫链,基于马尔可夫链的稳定状态概率进行系统性能分析。对会话初始化协议相关研究以及解决实际问题具有一定的理论价值。     

内网安全文件系统的设计与实现

针对内网海量数据存储安全问题,设计了多协议安全文件系统(MPSFS).一方面,MPSFS支持不同协议用户的访问,为不同用户提供统一的访问接口,实现用户高效和快速的访问;另一方面,MPSFS与身份认证和安全算法相结合充分保证内网存储系统中数据的安全性.实验结果显示,MPSFS在保证信息存储安全性的同时,对内网I/O性能影响在实际中是可以接受的.     

云制造系统用户认证和服务间协同高效可信安全技术

针对云制造系统不同安全域之间信任关系孤立导致的用户跨域访问重复进行身份认证和云服务跨域协同被拒绝的问题, 设计了一种面向云制造系统的域间互信过程模型, 提出了基于域间互信的用户认证和服务跨域协同高效可信安全优化技术, 实现了用户可信身份跨域传递和云制造服务跨域协同, 并在企业进行了应用验证, 给出了所提方法与传统方式的对比分析。分析结果表明, 提出的高效可信安全技术能够在提升云制造系统认证和服务跨域协同效率的同时不降低现有安全机制的防护强度。     

Formal Specifications and Verification of a Secure Communication Protocol Model

1 .INTRODUCTIONAlongwiththerapiddevelopmentofthecomputernetwork,theinformationtransferredthroughthenetworkhasbeenontheincrease ,accordingly ,thesecurityofcommunicationhasbecomeapopulartop ic .Communicationprotocol,theessenceofcomputernetworkanddatacommunication ,referstoapropercommunicatingbehaviorcarriedoutbyasetofproto colentitiesundercertaincommunicationrules.Itistheimperfectcommunicationprotocolthatcausestheinsecurityofnetworkcommunication .Inthispaper,asecurecommunicationprotocolmode…     

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

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

利用量子计算语言进行量子通信仿真

量子通信是利用量子位进行信息传送的一种绝对安全的通信方式。将一种用于量子计算仿真的量子计算语言引入量子通信的研究中,实现了一种典型的量子安全直接通信协议的正确性、安全性仿真验证,并得到各种性能指标。仿真结果与理论分析结果的一致性验证了利用量子计算语言进行量子通信协议仿真的可行性。量子计算语言的引入,为量子通信的研究提供了一种强大、简便、通用的工具。     

基于组件的安全主动网络仿真模型

分析了主动网络中存在的安全问题,提出了一种增强主动网安全性的方法:通过对数据信源格式的扩充,即为主动信包增加安全域的方式来增加主动网络的安全性。建立了基于组件结构的仿真模型,并通过J-Sim仿真软件对具体实例进行了仿真研究。模型可以研究不同的协议部署方式、不同的拓扑结构、不同的安全策略以及不同的网络性能参数对主动网络性能的影响。     

IPTV数字内容版权保护安全协议的设计

针对IPTV流媒体应用的特点,提出适应IPTV流媒体应用特点的适用于动态的、分布的、异构的、开放的网络环境下的数字版权保护协议,对网络中动态出现的内容服务提供了完善的数字版权保护功能,并具有跨网络安全域的特点。该协议在满足数字版权保护协议基本要求的同时,引入了版权中心和服务网关,以便更好地保证协议抗攻击的能力和内容提供者和消费者在版权方面的公平性。利用PETRI网的分析方法,对协议中各种变迁及状态变迁进行了分析。分析结果表明协议结果具有教强的安全性。     

冲突避免的水声网络拓扑发现协议

当水声网络的所有节点完成在目标区域的部署后,每个节点除了自己的节点ID已知外,对新网络的信息一无所知,而这些信息是网络顺利运行的必要前提。因此,一个能够完成网络中所有节点和链路发现的网络拓扑发现协议是非常必要和重要的。水声拓扑发现协议完成的效率,往往依赖于信道接入策略的选择,但它不能完全使用已有的水声多路访问控制(multiple access control, MAC)协议,因为在网络建立的初始阶段拓扑未知,已有传统水声MAC协议不能完成拓扑发现,所以需要根据这一阶段的特殊状态来设计拓扑发现协议。基于此问题,提出了一种高效的冲突避免的水声网络拓扑发现(简称为CFVE)协议,该协议利用网络中节点ID的唯一性,在其特定时隙接入信道,节点无冲突地发现控制分组的交换,最终实现网络中所有链路和节点的发现。仿真结果表明, CFVE协议可以以较低的发现时延和能耗完成全网拓扑的发现,是一种适合于多跳水声网络的拓扑发现协议。     

基于SMC的分布式隐私保护数据发布研究

针对垂直分布式存储结构的隐私保护数据发布问题,基于元组等价群的概念给出全局k-匿名化的定义和充要条件,采用集合多项式表示方法求解出全局元组ID等价群;并基于多方安全计算的同态加密协议构建了具有隐私性、准确性和公平性的分布式隐私保护k-匿名模型,从而实现了各微数据提供方不泄露本地隐私信息的前提下由半可信第三发布方发布出可供统计分析和数据挖掘等需求的真实有效数据集。实验结果表明,该模型具有很好的安全性、准确性和适用性。     

可证明安全的基于RSA的远程用户口令认证协议

身份认证是确保信息系统安全的基本手段,基于RSA的认证协议由于实用性较强而成为近期研究热点.讨论了Xie等提出的一个基于RSA的双因子远程用户认证协议,指出该协议不能抵抗重放攻击和密钥泄露仿冒攻击,无法实现所声称的安全性,并且存在用户隐私泄露和可修复性差问题,不适于实际应用.给出一个改进方案,在随机预言机模型下,基于RSA假设证明了改进方案的安全性.与现有的基于RSA的同类协议相比,改进协议在保持较高效率的同时,首次实现了可证明安全性,适用于安全需求较高的移动应用环境.     

基于FSM的通信协议形式描述与验证技术

本文主要研讨基于有限状态机(FSM)的通信协议形式描述与验证技术。文中先论述了基本FSM形式描述与验证技术,给出了访问确认协议的FSM描述与验证实例,研讨了基于FSM验证方法的形式数学基础——全局状态矩阵的特征和性质;接着讨论了基于FSM的有关改进形式技术;最后给出了有关结论。