形式化分析

摘要： 对于5G移动通信网络,3GPP组织标准化了5G AKA等协议,用于身份认证和密钥协商.本文使用安全协议验证工具Tamarin对5G AKA协议进行了形式化分析.首先基于3GPP TS33.501 v17.0.0版本,完成了对5G AKA协议及期望其满足的安全性质的形式化建模.安全性质考虑了保密性质和Lowe鉴权性质,保密性质包括安全锚点密钥KSEAF和长期共享密钥K的保密性,鉴权性质包括协议参与实体之间在参数SUPI、SNID、KSEAF上的非单射一致性,以及在KSEAF上的单射一致性.然后本文在Tamarin中验证了5G AKA协议是否满足相关安全性质,发现保密性质全部得到满足,鉴权性质一共验证了36种情况,其中有23种情况没有得到满足.最后针对协议不满足的鉴权性质,本文采用了三种修改方法来对协议模型进行改进,并对改进前后的验证结果进行了分析总结.

摘要： 形式化技术是系统开发过程中提高可靠性的一种行之有效的途径,随着形式化技术的发展与普及,它在系统软硬件设计方面得到了一定的应用。以某超短波监测系统中的数字信号处理模块软硬件开发为例,介绍了信号处理模块的硬件设计,描述了该模块的软件设计及使用形式化分析技术在软件开发过程中的应用步骤,为形式化技术在类似产品的开发过程中的应用提供了一定的借鉴。

摘要： 群组密钥协商协议应用于物联网、无线通信、区块链、视频会议等领域,是当前的一个研究热点。该协议的交互消息较多,且消息认证、加密所使用的密码算法也复杂,这就给密码协议的形式化描述与安全性分析带来一定的困难。文章基于串空间理论,提出了相关概念以及基于事件的形式化分析方法。该方法直观、简洁、有效,易于对复杂的密码协议进行形式化描述,并能简化密码协议的安全性分析过程。文章基于事件的形式化分析方法对簇间非对称群组密钥协商协议进行形式化描述和分析,发现该协议不能满足一致性,即不能认证参与协议交互节点的身份。通过对该协议的分析,也证明了文章所提形式化分析方法的有效性与正确性。

摘要： 应用内第三方支付具有便捷实用的特点,使得众多的移动应用选择嵌入第三方支付功能,但其安全性缺乏系统全面的分析,导致支付安全难以保证.为此,对基于Android平台的五种第三方支付协议的协议流程、安全假设和安全目标进行形式化建模,并采用ProVerif对协议进行分析,分析结果表明,协议在Android平台上的实现难以抵御订单篡改、订单替换和通知伪造等攻击;其次,在测试了210个采用应用内第三方支付的App后,发现近13.8%的App均能被成功攻击;最后,为抵御上述攻击,对第三方支付协议的实现提出了具体的建议.

摘要： 不可否认协议必须满足存活性、不可否认性、公平性和时限性,但当前大多数形式化方法只能分析该类协议的部分性质,证明或证伪协议逻辑的部分正确性.本文通过向ZQZ逻辑添加时间表达式,提出了一种适用于不可否认协议建模与分析的扩展ZQZ逻辑方法,包括推理规则和安全性质模型.展示新方法的应用时,使用其分析了ZG和KPB这两个局部逻辑正确性已知的两方不可否认协议,以及YLL这个逻辑正确性尚在讨论的基于区块链的多方不可否认协议.实验显示,对前两个协议的分析结果与既有事实相符,对第三个协议的分析发现其无法为收方提供设计者所宣称的时限性.以上结论从逆向工程角度佐证了扩展ZQZ逻辑方法是一种行之有效的不可否认协议分析新方法.

摘要： 为了提高无人机集群战术通信链路传输的连贯和安全,针对当今无人机自组链路网络的不足,提出了一种中继式无人机自组网安全协议。该协议将无人机集群划分为普通节点和中继节点,中继节点担任空间网络环境信息采集和分析的作用,并作为无人机集群协同化中心通过获得的信息为整个集群规划路径,此时新加入的无人机节点不会影响整个战术通信链路,保证了整个自组链路网络的安全可靠。

摘要： 在5G网络中,物联终端接入方式主要是无线接入。针对在海量接入场景下高昂的认证成本,该文提出了一种适用于电力5G终端二次认证的基于聚合签密的二次认证方法,该方法在保证安全性的同时,具有计算量和存储空间消耗少、运行效率高的特点,同时避免了传统公钥密码系统中的证书管理问题和基于身份的公钥密码系统中的密钥托管问题。该文对于适用于该方法的5G EAP-TLS鉴权协议进行研究。5G EAP-TLS协议主要用于5G专网或IoT场景下的鉴权和密钥协商,该文基于TS 33.501文档构建5G EAP-TLS协议模型,采用ProVerif验证工具验证协议的安全属性,并提出了修正方案。

摘要： 为解决Kerberos身份认证协议易遭受口令猜测攻击和重放攻击等局限和不足,提出一种基于物理不可克隆函数(physical unclonable function,PUF)的Kerberos改进协议。该协议的优势在于利用物理不可克隆函数生成的激励响应对代替原协议中的密钥,降低密钥存储开销和密钥泄露的风险;使用随机数与用户口令相结合生成会话密钥,用于抵抗口令猜测攻击;在抗重放攻击方面,采用随机数代替时间戳的方式减少同步需求。使用Scyther形式化分析工具分析该协议的安全性,验证了该协议可以抵抗口令攻击、重放攻击等威胁。

摘要： 针对当前UE在gNB间的切换认证与密钥协商过程存在的仅有两跳前向安全性和易受拒绝服务攻击等问题,提出了一种基于中国剩余定理(CRT)的切换认证与密钥协商协议。该协议利用秘密共享原理,令源gNB和所有可能的目标gNB构成一个群体,把真实的参数作为“秘密”在源gNB和唯一的目标gNB间共享,使得关键参数NH和NCC能在源gNB和目标gNB间安全传输。实验结果表明,该协议是安全的,相比同类的改进协议具有效率优势。

摘要： 本文介绍了基于静态分析的密码协议业务逻辑缺陷检测的具体方法,从检测框架出发,引出了方法实现的三个关键问题,然后对模型代码解析、协议代码信息抽取以及映射关系建立这三个关键问题进行了详细的分析论述。对密码协议进行形式化分析,从协议业务逻辑层面上证明密码协议的安全或者是找出协议逻辑层面的缺陷,一旦发现协议的缺陷,协议规范需要重新修订,并且协议代码也要做相应的修改[1]。

摘要： 针对现有复合型支付协议AECPP的单向身份认证中易受匿名攻击,支付子协议的完整性不能有效保证这些不足,提出了一种新的复合型电子支付协议.新协议实现了用户与服务供应商之间的双向认证,通过引入Hash函数和经由第三方信息的转发进一步提高了支付子协议的完整性和保密性.通过SVO逻辑和Kailar逻辑形式化分析验证可知,新的复合电子支付协议满足双向认证性、可追究性和公平性.

摘要： 随着航空航天领域软件系统对可靠性及安全性要求的日益提高,形式化分析方法逐渐得到越来越多的重视.模型驱动开发过程中,在模型分析阶段,采用先进分析工具对系统模型进行形式化分析已成为研究热点,而模型转换成为模型形式化分析研究中的关键问题.本篇论文基于航空航天领域的一个实际的工业界应用系统,GNC应用系统的遥测子系统TSG,介绍在模型驱动开发过程中对AADL模型的形式化分析方法的实例研究.首先对于TSG系统进行AADL系统建模.第二步针对TSG系统的AADL行为模型进行形式化分析及验证:(1)介绍AADL建模语言及行为附件.(2)介绍形式化分析的关键步骤——模型转换,首先给出目标模型CSP的概述,然后通过实例介绍转换规则.(3)在TSG的形式化模型基础上进行特定属性的安全分析.整个TSG系统的模型的构建过程是在AADL模型驱动开发集成环境SZIDE上实现的,TSG系统的形式化分析在PAT工具中实现.

摘要： 目前,对量子认证协议的安全性分析方法计算过程复杂且效率低下.如果将形式化分析方法应用于量子认证协议中,那么就能大大提高分析效率.BAN逻辑作为形式化分析方法之一,是一种简洁的协议分析工具.本文提出了使用BAN逻辑对量子认证协议进行安全性分析方法,并以基于纠缠对的量子认证协议为例进行了安全性分析.结果表明，在协议的初始阶段，成功地在Alice与信息中心、B ob与信息中心之间建立了量子信道，并且在合法通信方Alice和B ob之问安全地分配了一个共享密钥;在认证阶段，合法通信方Alice与B ob之间建立了安全的量子信道，互相认证了对方的身份，而且获得了量子密钥。由此可知，协议安全地完成了量子密钥分配功能和身份认证功能。

摘要： 对认证测试方法在安全协议形式化分析中的应用进行了深入研究,应用认证测试方法对Needham-Schroeder协议进行了分析,指出Needharm-Schroeder协议存在中间人攻击和类型错误攻击,对Needham-Schroeder协议进行了改进并采用认证测试方法证实了改进的协议可以满足协议的安全目标。

摘要： 大规模系统的模型状态空间生成过程由于状态空间的规模没有预先估计而不可控,形式化分析有利于解决这一问题。本文针对复杂串联系统的特殊结构,采用形式化方法分析研究了它的状态空间生成规律,从而达到快速预估模型状态空间规模的目的。

摘要： 针对特殊任务航天器的高可靠性和高安全性要求,提出了一种基于并行通道配合计算机交联(Computer Cross Talk)的导航制导与控制分系统(GNC分系统)体系结构.该体系结构使用1553B数据总线和TTP(Time Triggered Protocol)数据总线,配合拜占庭交联模式的GNC控制器,通过数据交换和数据比对满足系统故障检测和故障容错的要求.使用SCADE系统设计工具软件对该系统进行正常情况和故障情况建模,并对系统的故障容错特性进行形式化验证,验证结果表明,系统可以容忍任意一重故障且不损失任何性能,并具备实时现场恢复的能力。

摘要： 致力于普适计算下的动态更新的研究，首先分析了普适计算下动态更新的场景，针对普适环境的动态性，我们提出了区别于传统更新方式的路径更新；通过分析集中式更新模型的局限性，提出了适合普适环境的分布武更新模型；最后使用类型与效果系统为更新模型做形式化分析。

摘要： 本文基于形式化建模的思想，分别建立源节点、中间节点和目的节点的有限状态机(FSM)模型，描述AODV协议的路由行为及算法思想，分析影响AODV协议性能的可能性因素后，利用NS2对AODV协议进行仿真，以指导对协议算法的改进及其下一步研究方向，使其更好地适应Ad hoc网络特点。

摘要： 在介绍传统电子数据固定方法的基础上,针对可信取证理念,给出电子数据静态属性可信的支撑框架和可信固定方法.运用DSA数字签名、时间戳技术,并结合基于让实数字签名的第3方保证方案,研究电子数据具体的可信固定算法.通过形式化分析,定义并描述电子数据静态属性可信的约束规则,为电子数据可信固定提供支持.结合取证实例,运用已总结的公理和规则进行可信取证的形式化分析.结果表明,该方法能对电子证据进行可信固定.

摘要： 《中华人民共和国电子签名法》第十三条规定,电子签名同时符合下列条件的,视为可靠的电子签名。相对于一般的电子签名,交互型电子签名在生成电子签名的过程中增加了签名人和制作数据方交互确认的环节,有助于确证“签署时电子签名制作数据仅由电子签名人控制”,使其更接近法律意义上的“可靠的电子签名”.在JR/T0068-2012、JR/T0114-2015等金融行业标准的推动下,交互型电子签名在金融领域,特别是网上银行得到了广泛应用,手机银行也在普及推广.与此同时,多种关于交互型电子签名的方案被人们提出.

摘要： 本发明公开了一种对时间敏感网络的调度及流量整形机制进行形式化分析的方法，包括：确定TSN调度及流量整形机制的组成部分；根据确定的各组成部分，抽象出简单的调度及流量整形模型；根据抽象模型，确定模型的精化方案；对精化模型进行形式化分析以及时间性能分析。本发明中，通过对TSN的调度和流量整形机制进行形式化建模，不仅可以通过推理验证来保证最终的协议标准是否满足时间敏感性的需求，确保协议标准的正确性和可靠性；而且，对抽象模型的改进代价较低，对于协议标准的开发和后续扩展能够提供一定的帮助，能够节省开发时间和成本；并且提供了可量化的指标来比较不同调度机制的异同点及优缺点。

摘要： 本发明公开了一种基于TMSVL的C语言实时系统运行形式化分析方法，所述方法使用TMSVL语言来描述C语言实时系统的性质，即描述待验证性质变量在特定时间的值，同时在C语言实时系统源代码中加入断言语句，通过执行加入断言语句后的C语言实时系统来获得待验证性质变量的信息，最终完成对C语言实时系统的运行形式化分析。本发明使得TMSVL验证C语言实时系统的性质更加容易，克服了人工建模工作量大、难度大以及容易出错的问题，同时相比于自动建模，本发明不需要建立复杂的转换器，提高了C语言实时系统形式化分析的效率。

摘要： 本发明涉及一种机械臂运动学形式化分析方法，包括如下步骤：步骤一，确定机械臂机构的结构参数；步骤二，用高阶逻辑语言建立机械臂机构运动学逻辑模型；步骤三，用逻辑公式描述需要验证的运动学约束或属性；步骤四，将机械臂机构运动学逻辑模型和需要验证的运动学约束或属性组成一个逻辑命题；步骤五，利用逻辑推理引擎证明所述逻辑命题是否成立，成立表明所述模型满足所述的约束或者具备所述的属性，否则，不成立表明所述模型不满足所述的约束或者不具备所述的属性。本发明中的形式化验证根据系统形式规范或属性，使用数学方法证明系统的正确性，对所验证的性质而言是精确和完备的。

摘要： 本发明公开了一种基于Coq的超大规模集成电路RTL漏洞形式化分析方法，包括：S1、词法语法分析，主要是分析集成电路硬件描述语言生成抽象语法树；S2、数据流转化，获取集成电路的数据流信息；S3、获取方程描述，从数据流信息的插桩函数中，获取数据流的方程描述；S4、抽象函数模型抽取，从方程描述中获取函数表示形式的抽象函数模型；S5、形式数据模型抽取和精简化，从抽象函数模型中抽取形式数据模型并进一步精简；S6、漏洞分析，使用Coq定理证明器进行证明并分析结果，证伪时，则该集成电路设计存在漏洞。本发明将安全漏洞产生条件定义为数学定理，推导判定漏洞定理是被证明或证伪，从而判断集成电路RTL漏洞是否存在。

摘要： 本发明涉及一种自动化协议形式化分析方法，可以适用于多种协议的安全分析。协议作为安全分析的基本手段，可以利用形式化分析模型对某种协议进行数据建模，填充字段，设计工作流程，再用自动化脚本工具进行测试。形式化分析工具可以发现协议中存在的基础性漏洞，这些漏洞往往会造成设备、系统的重大安全问题。

摘要： 本公开实施例公开了一种机械臂稳定性形式化分析方法、装置、设备及存储介质，所述方法包括：根据机械臂状态方程构造李雅普诺夫函数；立机械臂平衡状态稳定性分析的形式化模型；将所述李雅普诺夫函数的性质与所述形式化模型组成逻辑命题；基于定理证明器证明所述逻辑命题，根据证明结果分析所述机械臂的稳定性。该技术方案根据机械臂状态方程构造李雅普诺夫函数，并在定理证明器中建立机械臂平衡状态稳定性分析的形式化模型，通过定理证明器证明李雅普诺夫函数的性质与所述形式化模型组成逻辑命题成立，实现了用数学方法验证机械臂平衡状态的稳定性，适用于分析高度非线性的机械臂的稳定性，对所验证的机械臂而言是精确完备的。

摘要： 本发明公开了一种对时间敏感网络的调度及流量整形机制进行形式化分析的方法，包括：确定TSN调度及流量整形机制的组成部分；根据确定的各组成部分，抽象出简单的调度及流量整形模型；根据抽象模型，确定模型的精化方案；对精化模型进行形式化分析以及时间性能分析。本发明中，通过对TSN的调度和流量整形机制进行形式化建模，不仅可以通过推理验证来保证最终的协议标准是否满足时间敏感性的需求，确保协议标准的正确性和可靠性；而且，对抽象模型的改进代价较低，对于协议标准的开发和后续扩展能够提供一定的帮助，能够节省开发时间和成本；并且提供了可量化的指标来比较不同调度机制的异同点及优缺点。

摘要： 本发明公开了一种实时协议的形式化分析及验证方法，包括：数学建模步骤，用于利用进程代数建模，对实时协议进行形式化表示，建立实时协议模型，并对协议需求进行形式化表示；代码生成步骤，根据所述实时协议模型生成高级语言代码；仿真验证步骤，根据进程代数描述语言的语义对所述实时协议模型进行仿真执行，并根据数学建模步骤所输出的实时协议的形式化表示和协议需求的形式化表示，对所述实时协议模型所满足的需求性质进行分析与验证；验证结果处理步骤，对仿真验证步骤所输出的分析与验证结果进行统计及分类，并提供协议性质的评估。该方法提供不满足协议需求的协议执行过程，并提供协议性质的整体评估，提高了开发人员优化协议的效率。

摘要： 本发明公开了一种基于嵌入式操作系统微内核原型的进程间通信安全性形式化分析验证系统，包括：原型预处理模块，其包含形式化分析验证系统的系统入口，并且以嵌入式操作系统微内核原型为输入，经过微内核模块分类提取器处理从中提取出待验证的IPC模块，生成IPC功能相关的集合作为各模块输入的待验证数据；可数状态特定属性验证模块，用于验证有穷状态下特定属性的IPC安全性质，可有针对性地对待验证的IPC故障行为进行建模分析；无穷状态及泛化属性验证模块，用于验证无穷状态或非特定属性的IPC安全性质、验证由规范化数据结构抽象出的IPC外在性质、及基于已有抽象性质针对各兴趣点深入抽象且进一步生成不同的模型并精化验证。

摘要： 本发明公开了一种基于共形几何代数的机械臂运动规划的形式化分析方法和系统。所述方法其包括：基于共形几何代数理论对机器人的基本构件、运动规划约束构建对应的几何模型，再用高阶逻辑语言描述所建立的几何模型，形成机器人的基本几何逻辑模型系统；确定机器人的具体结构参数和运动规划参数；基于基本几何逻辑模型系统对具体机器人运动过程的形式化建模，得到具体机器人运动过程的几何关系逻辑模型；用逻辑公式描述需要验证的机器人运动过程的约束或属性；将具体机器人运动过程的所述几何关系逻辑模型和待验证的运动过程的约束或属性组成一个逻辑命题；利用逻辑推理引擎证明所述逻辑命题是否成立。