共查询到20条相似文献，搜索用时 149 毫秒
1.
随着计算机网络的不断发展,全球信息化已成为社会发展的必然趋势。在网络的应用服务中,信息安全是至关重要的环节。而安全协议是保障信息安全最基本内容之一,已广泛应用在计算机通信网和分布系统中。这样,高效准确的安全协议的形式化分析是必不可少的。所以形式化方法分析安全协议已成为目前研究的重点。本文以H.530协议为例给出其形式化分析与模型检测。 相似文献
2.
频发的网络信息安全事件使得解决网络信息安全投资问题迫在眉睫.在企业投资成本和利润不同的情况下,应用博弈理论计算了网络信息安全的投资过程,提出了相互依赖的信息安全投资风险模型.用风险评估方法对企业信息安全风险进行量化,提出安全风险量化模型,通过适当投资提高系统的安全稳健性.该方法为信息安全的风险管理提供了新思路,为企业确定自身的投资策略提供了依据. 相似文献
3.
孙淮宁 《淮南师范学院学报》2009,11(3):37-39
从需求角度出发定义了操作系统的简洁模型,提出以系统的运行活动实体为核心满足操作需求的概念,然后以此概念为引申,采用ADT方法详细地定义和讨论了计算机系统、作业、服务、系统调度和资源的形式化实体结构模型,最后建立了形式化的操作系统基础模型,从而解决了操作系统形式化基础模型缺乏的问题. 相似文献
4.
为了实现随需应变、动态组合的跨组织协作业务流程模型,将pi-演算理论引入业务流程建模与验证中,应用pi-演算理论建立了多角色、多维度、多集成性的业务流程跨组织协同的模型.新的业务流程模型为M×N多维度网状关系,同时兼顾了以往单一的线性顺序关系模型,并分别从横向与纵向对该协作业务流程模型进行了形式化描述.最后依据pi-演算理论对样例模型的死锁、活锁以及同步性进行了验证,确保了模型的正确性和可行性.跨组织动态协作业务流程模型具有稳固的理论基础,为跨部门、跨区域分布式信息交互提供了新的思路和方法. 相似文献
5.
基于认证测试的鲁棒电子邮件协议形式化分析(英文) 总被引：1，自引：0，他引：1
基于认证测试方法及strand space模型,形式化分析了具有完美前向机密性的鲁棒电子邮件协议,指出该协议存在安全缺陷.同时给出了针对该协议的中间人攻击方法,即攻击者在协议的接收阶段通过伪造消息即可欺骗通信双方,使通信双方与其共享错误的会话密钥,由此使得协议的完美前向机密性得不到保证,针对协议的上述缺陷,提出一种改进方案,即通过在协议的接收阶段加入相应的签名信息,以保证改进协议能够克服中间人攻击并且提供完美前向机密性.最后,基于认证测试方法及strand space模型,形式化证明了改进协议在发起者、接收者及服务器之间的安全认证,确保了改进协议具备真正的完美前向机密性. 相似文献
6.
形式化方法在程序验证、模型检测的研究有着重要作用,集成形式化方法是形式化方法发展的一个方向.BCCS模型是集成B方法和进程代数CCS构建的一个混成模型,模型中给出了一个轻量级的描述语言,但缺少语义的支持.为了保证这个描述语言的完备性和一致性,本文则在传值CCS操作语义的基础上,结合B方法对抽象数据结构的定义、系统的限制以及功能处理,给出了BCCS的操作语义,进一步刻画BCCS模型. 相似文献
7.
就刻画安全的本质而言,基于非演绎信息流安全模型较之与基于访问控制的安全模型更为确切。文章在基于迹语义对非演绎信息流安全模型进行分析的基础上,给出了基于扩展Petri网的非演绎模型的形式化描述,进一步基于Petri网的形式化描述给出非演绎模型的验证算法且开发相应的验证工具,最后通过实例说明该算法的正确性和验证工具的方便适用性。 相似文献
8.
统一建模语言UML在面向对象的建模技术中得到了广泛应用。但是UML模型缺乏形式化语义,难以使用数学方式对模型进行分析和验证。B方法作为一种建立在严格数学机理上的形式化方法,将可视化UML模型转换为B形式化规范,可以对模型进行形式化描述和分析,确保模型的可靠性。通过研究从UML状态图到B形式规范的转换规则,提出了一种基于XMI的状态图到B形式化规范的自动转换方法,并使用Java语言实现了自动转换工具UML2B。 相似文献
9.
论文以一个销售管理系统形式化建模为例,考察了采用形式化方法的适用性原则并探讨了存在的问题。通过遵循试验证明,所提议的规则可以促进模型的简化、强化抽象概念的提取和明确抽象模型与具体模型的区别。在下一步工作中,需要讨论开发过程多阶段的形式化描述以及如何关联多阶段模型。 相似文献
10.
为了获取词语在文章中的语义权重,解决词语的同义、多义模糊问题,提升信息检索的效率,提出了一种基于概念的检索模型,模型中设计了一种形式化的文本内容表示框架,框架由2部分构成:文章的“领域”以及“情景与背景”信息,并由概念(形式化语义)加以表示.同时,提出了提取该概念框架的方法,给出了用于框架与检索要求间匹配的两阶段平滑算法.实验表明,在TREC6提供的小规模语料集下,采用所提出方法的信息检索模型与传统模型相比,平均召回准确率提升了约10%,效果显著,充分说明了基于本文描述方法构建的、以概念作为处理中介的信息检索系统的有效性和可行性. 相似文献
11.
攻击者建模是安全协议验证工作的一个重要部分,直接影响到验证的效率与质量,但目前却还没有一个可遵循的形式化框架,影响了建模工作的准确性与客观性。针对这一问题,通过对在安全协议验证中具有广泛影响的DY模型进行形式化,建立了一个DY模型的构建框架,刻画了攻击者的构成要素、行为规则以及行为模式,从而保证了攻击者具有合理的行为与能力,并能在攻击过程中获取新的知识,不断增强攻击能力。最后,将该工作运用到Otway Rees协议的验证中,找出了该协议中所存在的漏洞,从而证明了该构建框架的有效性。 相似文献
12.
阐述了安全电子商务协议的安全属性,介绍了重要的安全电子商务协议,总结了近年来安全电子商务协议形式化分析方法的研究进展情况。文章最后对该领域主要的研究方向进行了展望。 相似文献
13.
为了对网络安全进行综合评价,根据网络安全评价指标体系,建立了网络安全的综合评价模型.先利用灰色聚类方法对网络安全指标的原始数据进行等级评价分类,根据待识别样本与各类类中心的距离,确定待评价样本等级;再利用层次分析法对每类分别排序.结果表明,该模型能够有效地对网络安全进行综合评价. 相似文献
14.
空间方向关系形式化模型是判定空间关系的基础,为了提高模型的可靠性,提出了一种基于F直方图的空间方向关系形式化模型。首先给出了基本的F直方图算法,然后提出了基于F直方图的空间方向关系判定方法。采用人工图片作为算例进行实验的结果表明该模型是可行的。 相似文献
15.
三井庙重修事件展示了一个自发性宗教组织资源动员的图景。一个形式化低功能的老人协会是这个自发性组织得以形成的外部环境;受到现代正式组织制度和理念规制,秉承了传统社会中公共意识,具有一定民间信仰的退休精英的存在和作为,成为该组织成长的重要契机;现代社会的福利保障也让该组织成员免于后顾之忧。此外,坚定的信仰、民众的信任也是其资源动员的主要动力。 相似文献
16.
网格计算是一门新兴的技术,它能够为用户和应用提供对资源和大量IT功能的无缝访问.安全问题是网格计算成败的关键.通过分析网格计算的基本特点和安全要求,结合网格安全策略和安全体系模型,给出了该模型的一种实现方法. 相似文献
17.
龙启平 《钦州师范高等专科学校学报》2006,21(3):61-65
ClickOnce部署是基于.NET 2.0智能客户端的新一代部署技术,它是以前所用的部署模式的自然发展,集成了B/S和C/S两种部署方式的优点,具有可靠性、安全性和灵活性等特点,为Smart Client提供了一种简单、可靠和安全部署的解决方案. 相似文献
18.
李少伟 《信阳师范学院学报(哲学社会科学版)》2007,27(6):18-22
委托与信托从概念上和形式上有着许多共同点,但信托与委托代理仍有很大区别。信托隐含了四个独特的法律原理:所有权与利益分离、信托财产的独立性、有限责任、信托管理的连续性,信托是一种特殊的委托。现行社保基金资产投资均采用委托模式,这种模式在法律上有诸多风险,而信托模式可以规避其中的某些风险,但是信托本身的缺陷也不可忽视。无论采用委托代理模式还是信托模式,都难以规避资本市场的系统风险及其自身的非系统风险。因此只有依靠有效而严格的监管才能克服这些缺陷,同时,也只有政府、中介组织、基金、从各自的层面共同努力,才能将风险控制在最低程度。 相似文献
19.
C lickOnce部署是基于.NET 2.0智能客户端的新一代部署技术,它是以前所用的部署模式的自然发展,集成了B/S和C/S两种部署方式的优点,具有可靠性、安全性和灵活性等特点,为Sm art C lient提供了一种简单、可靠和安全部署的解决方案. 相似文献
20.
基于个体趋利避害和事务逻辑完整的社会智能特征,提出了一种语义web的安全集成框架.该框架对语义web模型进行了扩展,控制语义web服务信任、逻辑、推理等方面的动态安全.该框架包括4个层次:信任入口层、社会智能层、事务层和TCP/IP安全协议层.信任层处理用户的信任特征,社会智能层控制语义web的逻辑问题,事务层负责事务推理,TCP/IP安全协议层则保证安全通信.这些安全层协同构建了具有不同安全等级的安全环.该安全集成框架为语义web提供一种安全集成方法,为不同技术的安全协同提供了通用的安全解决框架. 相似文献