首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到17条相似文献,搜索用时 171 毫秒
1.
分析了模型检测技术和逻辑推证技术的优点与不足,并在此基础上提出了一种混合的形式化分析技术的说明,该技术可提供更为完全的安全协议形式化分析.  相似文献   

2.
给出了应用于不同系统的不变式的概述, 分析了彼此之间的关系, 进行了分类, 并探讨了其未来发展趋势.密码协议的形式化分析日渐引起人们的广泛关注.这导致了不变式生成与描述技术的发展.不变式是对入侵者可知和不可知消息的定义, 可用于协议认证和秘密性的证明, 从而成为许多协议形式化分析工具和技术的核心  相似文献   

3.
介绍了抽象状态机(ASM),建立了基于这种形式化方法的协议描述于验证的环境,并建立了一般意义上的入侵者模型.作为应用实例,给出了 Helsinki协议的 ASM规约,说明利用这个规约可以直观的演绎 Horng-Hsu攻击.  相似文献   

4.
给出用PVS对密码协议进行形式化规范的一种方法.该方法以高阶逻辑为规范语言,利用trace模型来描述协议的行为,并假设系统中存在强攻击者和理想加密系统.重要的结构如消息、事件、协议规则等都通过语义编码方式定义.  相似文献   

5.
为π演算建立具有安全级别的简单类型系统,并证明该类型系统在规约语义下的类型可靠性.此类型系统使得π演算成为安全系统、安全协议分析与规范的普适形式化工具.  相似文献   

6.
高校体验式思想政治教育具有极其重要的价值和意义.但部分高校在"体验式"教育中忽略学生的主体性和教育过程,造成思想政治教育形式化.本文基于高校体验式思想政治教育形式化的现象及原因分析,提出方法和对策,为高校进一步推进体验式思想政治教育提供依据.  相似文献   

7.
提出了一种基于形式化B方法的软件构件模型,分基于检索的部分、基于学习的部分和基于组装与演化的部分来依次展现构件信息,并结合实例给出了使用B语言来描述构件的具体功能和行为规约的具体运用。  相似文献   

8.
主要使用运行模式法对简化的SSL30基本握手协议进行了形式化分析.通过分析,找到了3种不同的攻击形式,并且对这3种攻击形式进行了深入研究,发现这3种攻击虽然从表面上看都是由于允许不同版本共存的漏洞引起的,但是经过仔细分析攻击的形式,发现这3种攻击是存在差异的.主要是角色欺骗不相同,而这又可能会造成潜在攻击.最后对这个协议进行了改进,从而有效避免了以上3种攻击,提高了协议的安全性  相似文献   

9.
随着互联网的应用和发展,各种类型的安全协议,包括具有多个角色、多种密码运算的复杂密码协议,已广泛应用于分布式系统中解决各种安全需求.在大规模分布式网络环境下,参与协议运行的主体是大数量的甚至是动态的,密码协议运行环境极为复杂,这使得密码协议的安全性描述和分析变得非常复杂.引入了一个新的代数系统刻画具有多种密码运算的消息代数,并提出了一个新的密码协议模型,描述了无边界网络中的攻击模式,通过建立形式语言规范了无边界网络环境下密码协议的运行环境和安全性质 该协议模型描述了一种“协同攻击”模式,并讨论了密码协议的安全性分析约简技术,给出一个新的安全自动分析过程的简要描述.  相似文献   

10.
提出一个基于混合密码体制的抗否认密码协议 :可以运行在不安全信道上实现交易的公平性与通信双方的不可否认性;在通常情况下只需通信双方进行 3次信息的交互,且保证传递数据的机密性与收发方交易的隐私权;避免了可信第三方可能成为系统瓶颈的问题.最后给出该协议的形式化分析,证明了它的公平性、安全性与可行性.  相似文献   

11.
基于BAN逻辑的协议分析往往容易忽略密码协议潜在的“重放攻击”漏洞,为解决这一问题,对BAN逻辑分析的新消息判断法则逻辑公设作了一点改进.从而降低了BAN逻辑分析的误导性.  相似文献   

12.
我国竞技运动员保障体系现状分析与构建思考   总被引:14,自引:0,他引:14  
采用文献资料法、专家访问法,分析了我国现行运动员保障体系及存在的主要问题,在此基础上提出了我国新型运动员保障体系应由三部分构成:社会保障、商业保障、自我保障,进而讨论了自我保障体系的作用并重点提出了关于如何构建自我保障体系的设想。  相似文献   

13.
针对TPM访问控制机制无法直接应用于虚拟计算、云计算等环境的问题,重点分析TPM内部对象间依赖关系,并结合虚拟域的安全需求,建立TPM虚拟域安全模型.该模型对TPM对象的访问请求增加了虚拟域的完整性、机密性等安全约束,解决了多虚拟域环境下的TPM对象的创建、使用、销毁等问题.还进一步对该模型的安全规则进行了相关逻辑分析,并通过实际原型系统的测试,证明了TPM虚拟域安全模型的实施对可信虚拟平台的性能影响非常小.  相似文献   

14.
本文先对网络安全的目标、网络安全问题的来源和应对策略进行了介绍,指出校园网不同于一教网络的特点和问题,针对校固网这一小型网络的需求,分析其方案设计及安全隐患,并介绍了较团网网络安全实施的具体方法和网络安全紧急响应体系等.  相似文献   

15.
"形式逻辑"与"普通逻辑"这两个术语,在我国直至20世纪70年代末的逻辑教学中,都是作为"传统逻辑"的同义语,表达着同一种逻辑,即以亚里士多德逻辑为主的十九世纪中叶以前的逻辑。1979年,随着国门的打开,"形式逻辑现代化"和"普通逻辑课程现代化"的提出并实施,"形式逻辑"有了传统与现代之分;普通逻辑已不再是传统逻辑的同义语,而是一门吸收了大量数理逻辑知识但仍以传统逻辑为主的普通高等院校逻辑基础课程。  相似文献   

16.
摘要:通过文献调查与归纳演绎,分析了我国体育教育信息化应用研究33年来发展特征和经历的阶段,对体育教育信息化发展成熟度进行了定位,分析了目前所遇到的问题及未来的发展趋势。在信息技术及体育教育信息化应用呈现多样化的背景之下,从体育教育信息化建设工作者的角度,解决相应的工程学涉及需求分析的方法内容零散,种类繁多,组合不定选择困难的问题。论文归纳总结组合了一套具有适用泛型的方法组合,并且基于以内容表现方法为核心,根据内容表现需求选择信息技术的思路,从服务于体育教学的角度,对体育教育信息化的需求分析方法展开探讨。明确了体育教育信息化需求分析的7个重要组成部分,其中,背景及现状分析的主要内容是政策、社会和技术背景分析、应用历史与现状分析;系统规划方法需要多样化;系统目标描述包括组织目标描述,包括交互、应用、数据及其3个层面的传递方式的系统描述;系统功能描述的有效方法是用例分析;信息技术需求要关注技术的优缺点、软件和策略需要;数据库设计使用实体和属性的概念;界面设计包括功能设计、美观设计2个方面的描述内容。  相似文献   

17.
形态是事物的表现形式,它所体现的是客观形状和人的主观对形状所产生的一种情态知觉。本文通过对图形设计中点的形态美所引起的活动分析,对点在图形设计中的应用过程作一些基本的探讨。  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号