共查询到20条相似文献,搜索用时 125 毫秒
1.
2.
BRP协议是为不可靠信道上传送大数据包文件设计的工业协议。该协议的正确性依赖于各部件实时方面的假设。本文主要阐述了使用时序规约语言TLA+对BRP协议进行规约和验证的过程。首先通过自然语言非形式化地描述BRP协议的基本原理和需求,在此基础上建立了BRP的形式化模型,利用TLA+先对不考虑实时要求的BRP进行规约,然后添加实时约束获得BRP完整的规约,最后使用模型检验器TLC验证BRP协议的各种性质。 相似文献
3.
由于无线传感器网络(WSN)带来的新特点,需要开发更多区别于传统网络的路由协议。形式化方法Object—Z是建立在严密数学基础之上的开发方法,其形式化规约语言的测试和设计工作可以同时开始,适用于新网络、新算法的研究开发。文章提出了运用形式化方法Object—Z对flooding算法建模的方法。建模结果表明Object--Z适用于无线传感器网络的路由协议,并可实现对flooding算法的描述和验证。 相似文献
4.
形式化方法概貌 总被引:1,自引:0,他引:1
形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明:其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性. 相似文献
5.
基于组件的软件开发能够有效提高软件开发的质量与效率.但在一些安全关键的领域,由于形式化模型与方法的缺乏,使得基于组件的开发方法不能成功应用.为了得到一套完整的形式化模型用于描述软件组件及其组成的系统,首先必须对软件组件的形式化语意进行定义.文中提出了一种基于共代数概念的语意,使得满足接口和组件规约的组件对应于一个具体的共代数,并由此推导出了接口和组件的功能契约的形式语意以及接口依赖的共代数语意.通过对一个简单的堆栈进行规约,体现了这种方法的可应用性. 相似文献
6.
讨论在通信协议安全分析中形式描述技术的使用方法。重点研究在协议模型的基础上建立层次化的协议攻击行为模型的方法,对所建模型进行形式化验证和脆弱性分析,根据验证和分析结果提出防护措施,设计安全方案。给出Petri网建模实例,提出形式描述技术在通信协议安全分析中的一些其他应用。 相似文献
7.
安全协议的设计和分析是复杂而且容易出错的。使用形式化的语言有利于安全协议的正确性和完整性。现有的安全协议的描述方法大多很复杂而且容易导致二义,从而导致协议隐含着种种的安全隐患。引入了基于构造类别代数的形式化规范语言来规范安全协议,通过规则集合和公理集合对安全协议进行精确地描述,有利于协议设计地规范化和协议漏洞地发现,同时对Needham-Sehroeder协议进行了形式化规范以进一步说明该形式化语言地使用。 相似文献
8.
9.
10.
志愿计算模型形式化方法 总被引:1,自引:0,他引:1
旨在从形式化抽象的角度来认识移动计算的本质特点.分析了志愿计算平台的特征,提出并分析了志愿计算中的3种角色以及志愿计算中资源和构件的概念,介绍了一种关于志愿计算的形式化模型和方法.对系统中的基本元素和交互关系进行了形式化的描述,并通过集合理论和操作规约,又以志愿计算平台XtremWeb为例,描述了构件化的志愿计算形式模型和方法,为系统地研究志愿计算形式化理论打下了基础. 相似文献
11.
无线射频识别(RFID)是物联网中的一种非接触式的自动识别技术,被广泛运用于构建物物互联的RFID系统。RCIA是一种超轻量级RFID双向认证协议,提供高安全性并声称能抵御去同步攻击。形式化方法是安全协议分析的有力手段。运用模型检测工具SPIN对RCIA协议的认证性及一致性进行验证,结果表明RCIA协议存在去同步攻击漏洞。针对此漏洞,提出基于密钥同步机制的修补方案,对RCIA协议进行了改进。对改进后的协议进行形式化分析与验证,结果表明改进后的RCIA协议具有更高的安全性。提出的协议抽象建模方法对此类超轻量级RFID双向认证协议形式化分析具有重要借鉴意义;提出的基于密钥同步机制的漏洞修补方案,被证明能有效抵御去同步漏洞,可适用于此类超轻量级RFID双向认证协议的设计和分析。 相似文献
12.
13.
14.
15.
在无线传感器网络路由协议的研究中,对现有协议的分析和验证具有重要意义.形式化建模是分析验证网络协议的一种有效方法.使用形式化工具有色Petri网对无线传感器网络中的SPIN路由协议进行形式化描述,并使用CPN Tools分析和验证了该协议的活性、可达性、有界性等特性. 相似文献
16.
随着安全协议形式化分析技术的不断发展,利用工具自动验证虽已得到实现,但建模环节仍需依赖专业人员手工建模,难度大且成本高,限制了此技术的进一步推广。为了提高建模的自动化程度,提出了依据安全协议代码进行形式化模型辅助生成的方案。首先,使用污点分析获取协议的通信流程,并且记录密码学原语操作;然后,根据通信流程之间的序列关系构建协议通信状态机;最终,根据目前主流的安全协议形式化分析工具Tamarin的模型语法生成形式化模型。实验结果表明,此方案可以生成形式化模型中的关键部分,提高了形式化建模的自动化程度,为形式化分析技术的推广作出贡献。 相似文献
17.
认证协议的形式化描述及其安全性分析是安全协议形式化分析的关键问题之一.为了解决以往分析方法中协议规范形式化描述存在的问题,提出了一种协议规范有向图描述方法,并在此基础上提出了协议消息构造的逆向搜索算法.用该算法分析Woo-Lam认证协议,找到了该协议一种新的攻击方法及其攻击路径. 相似文献
18.
一种电子商务协议形式化分析方法 总被引:15,自引:0,他引:15
提出了一种新颖的形式化方法,可以用于分析电子商务协议的安全性质,例如可追究性和公平性.与以前的工作相比较,主要贡献在于:(1)对协议主体的拥有集合给出了形式化定义,且主体的初始拥有集合只依赖于环境;(2)将协议的初始状态假设集合分为3类:基本假设集合、可信假设集合和协议理解假设集合,避免了因非形式化的初始假设而产生的分析错误;(3)对可信假设作细粒度的形式化规范,揭示协议的内涵;(4)建立公理系统,使新方法更为严格与合理. 相似文献
19.
采用形式化方法分析安全协议是协议分析的有效手段,近年来,出现了众多的研究方法。串空间模型是一种新兴的密码协议形式化分析工具。文章基于串空间模型,扩展了认证测试方法,使之能够描述和分析电子商务协议。并用该方法对一个具体的协议进行了形式化分析,得到了与以往文献相同的结论。 相似文献