形式化工具Scyther优化与实例分析

当前安全协议形式化分析工具发展迅速,针对不同的安全协议、不同的安全模型挑选合适的工具进行分析,不仅可以提高分析结果的可信度和准确性,还可以大大提高协议分析的效率.为此,对当前主流的9种形式化分析工具的性能进行梳理,从使用界面、分析效率、安全模型等综合角度来看,Scyther工具有着较大的优势;为方便国内协议分析者使用和研究,剖析Scyther的底层算法,将其交互界面进行汉化,并增添了时间计算功能,对分析时间进行计算和输出;最后以网络安全协议TLS为例,利用优化后的Scyther工具分别在Delov-Yao模型和强安全模型下对其进行形式化分析.对研究工作者准确、有效地选择和使用形式化分析工具有着理论意义和实践价值.

TFSP:一种分布式实时系统的形式化描述工具

分布式实时系统在宇航、核反应、军事和工业等部门应用极为广泛,这些领域对系统本身的安全性和可靠性要求极高,因此如何开发出正确的分布式实时应用系统是一个关键问题.为了对分布式实时系统进行建模,我们提出了TFSP(Timed Finite State Processes),即时间有限状态进程.TFSP扩展了Magee等人提出的FSP(Finite State Processes)[1].

基于Web的形式化方法工具RRTChecker的研究与设计

形式化方法工具通常是在UNIX/Linux系统下设计开发的,难于使用阻碍了形式化方法的进一步推广。本文针对形式化方法RAISE,提出了一种研究和开发基于Web的工具的方法。该方法以原有的RAISE工具为基础,通过Shell管道拦截技术、ASP技术、ActiveX DLL技术及路径重写技术,将工具的所有功能集成整合到统一的、用户友好的Web界面上,用户可通过鼠标在浏览器中进行不同的操作。原有的RAISE工具的所有功能,在基于浏览器的集成化工具中得到全面支持。该方法也为开发其它形式化方法基于Web的工具提供了新思路。

安全协议形式化分析工具比较研究

形式化分析方法已经成为协议分析的主流方法之一.目前,国内针对形式化分析工具的研究很少,工具之间的比较研究也不够充分.一方面,当前比较研究存在参比工具较少以及参比性能不全面的问题,另一方面,大部分比较研究仅停留在理论比较,并没有提供实验数据.因此,本文首先对AVISPA、Pro Verif、Maude-NPA、Scyther、Tamarin等当前主流形式化分析工具的背景、工具性能、应用范围等方面进行介绍,然后以SSH协议为目标协议,利用不同的形式化工具对SSH协议进行分析.根据实验分析结果,对比研究工具在运行性能、运行效率、底层算法、使用界面、安全模型等方面的优势和劣势.在对比研究结果的基础上,从形式化分析工具的使用和开发两方面进行讨论:在工具使用方面,通过工具比较研究,用户可以根据目标协议特性挑选合适的工具,对协议实现准确高效的分析;在工具开发方面,通过工具比较研究,指出代数性质扩展以及状态空间的限制和搜索算法是当前工具性能提升的重点和难点,突出了工具开发者需要掌握的用户需求,为工具开发提供理论基础.

基于即时验证的软件验证工具改进设计与实现

基于设计模型的分析技术是现代复杂嵌入式软件系统高可靠性的重要保障手段。基于即时验证(On-the-flyverification)方法对一个构件化嵌入式软件设计模型原型验证工具T-CBESD进行了改进设计与实现。集成Topcased和JFLAP扩展了T-CBESD图形化建模接口;设计并实现了相关输入处理与转换;重新设计并实现了状态空间数据结构,包括功能、非功能行为(实时、资源、能耗等)验证问题在内的多个基于路径的一致性即时验证算法。给出了改进工具在火灾预警系统中的应用实例与分析。

FDT与FDT工具及其研究

叙述形式化方法的基本概念，研讨了国际上标准的以及目前使用的应用于描述顺序软件、并发软件和基于图形的形式化描述，同时论述了支持形式化描述技术的工具的任务、作用和分类。

一种前向安全的联邦学习环境下密钥协商协议

联邦学习是一种新的机器学习模式,解决了数据孤岛及信息安全问题。近年来,联邦学习环境下密钥协商协议安全性的研究逐渐增多,横向联邦学习环境认证密钥协商协议不满足前向安全性同时也不能抵抗密钥泄露伪装攻击。提出了一种联邦学习环境下密钥协商协议,通过安全性证明和形式化分析,证明了该协议满足完善前向安全、抗密钥泄露伪装攻击、已知密钥安全等安全属性。

面向模型检测的LTL语句自动生成方法

为优化线性时态逻辑语句的生成过程,减少模型检测的时间,提出一种面向模型检测的基于自然语言处理生成线性时态逻辑验证语句的方法。对需求文档提取关键词,将文档中的数据和可以代表模型中状态的名词进行提取,注释UML模型,对UML模型中的状态进行归类,将模型中的状态分为数据属性类和调用操作类,利用配对的线性时态逻辑格式生成线性时态逻辑,用于软件模型一致性验证。实验结果表明,该方法与ST模型相比可以提高模型检测的效率。

类型系统的构造、实现及其在程序设计语言中的应用

类型系统是一种设计和研究程序设计语言的形式化方法和工具 ,既可在语言设计之初构造 ,便于严格、准确、正确地设计实现语言 ;也可在语言实现后构造 ,为研究语言的语义及其它性质建立模型 .详细讨论了类型系统的基本构造和实现 ,通过基于图重写的函数式语言SClean的类型系统 。

两个认证密钥协商协议的前向安全性分析

目前,网络安全及隐私受到广泛关注。前向安全性是Günther在1989年提出的一种认证密钥协商协议(AKA)的安全属性(doi:10.1007/3-540-46885-4_5),该性质经过30年的蓬勃发展已经成为研究领域的热点之一。该文主要分析了MZK20和VSR20两个AKA协议。首先在启发式分析的基础上,利用BAN逻辑分析了MZK20协议不具有弱前向安全性;其次利用启发式分析和Scyther工具证明了VSR20协议不具备前向安全性。最后,在分析VSR20协议设计缺陷的基础上,提出了改进方案,并在eCK模型下证明了改进后协议的安全性;并且,结合Scyther软件证明了改进VSR20协议与VSR20协议相比明显提高了安全性。

Web服务语言BPEL到接口自动机的转换

在目前对于服务组合的研究中,对于用业务流程执行语言(BPEL)和WSCL等标准语言来描述的服务来说,语言本身缺乏对组合正确性进行检验的支持,必须借助相关的形式化工具来完成对服务组合的检验.为了解决BPEL对检验支持的不足,基于接口自动机这一形式化工具,对BPEL中主要语言元素到接口自动机进行转换,转换的目的是为了下一步应用基于接口自动机的行为获取方法来对服务的组合进行验证,最后通过一个实例证明了转换方法的有效性.

eXtended Triple Diffie-Hellman协议的安全性分析

针对X3DH(eXtended Triple Diffie-Hellman)协议安全性的问题,使用形式化分析工具OFMC(On-the-Fly Model-Checker)和协议建模语言AnB对协议进行验证。首先,在Types部分对协议涉及到的通信实体进行了建模;然后,在Knowlegde部分规定了各通信实体的先验知识;其次,在Actions部分对协议的协商流程进行了建模;最后,在Goals部分对协议的机密性、完整性、双向鉴别性等安全目标进行了建模。实验结果表明,X3DH协议作为Signal协议的核心,实现了密钥协商协议所要求的机密性、完整性、双向鉴别性等安全目标,并且形式化分析工具既可以减少工作量,又可以发现人工不易发现的协议漏洞,从而更加全面、高效地验证协议的安全性。