基于UPPAAL的NS密码协议模型检测分析

形式化分析方法是目前密码协议分析的主流方法。然而,典型的密码协议形式化验证方法没有考虑时间因素,这个选择使得分析简单化。本文提出了运用基于时间自动机的模型检测工具UPPAAL分析密码协议的方法,并对著名的Needham—Schroeder协议（简称NS协议）的简单版本进行了分析。在对NS协议进行建模时,考虑消息实际传输需花费时间,引入消息的时间信息,从而构建NS协议的时间自动机模型。该方法利用UPPAAL的检查引擎所用的先进技术使其克服了一般时间自动机应用存在的状态空间爆炸问题。实验结果UPPAAL给出了NS协议认证失败的一种可能之一。分析结果表明,入侵者可以轻松地对NS公钥协议进行有效攻击。从而证明UPPAAL工具可以成功检测出NS协议的缺陷。     

一种P2P层叠网维护协议的稳定性分析

对一种P2P层叠网维护协议“基本叶集协议”进行稳定性分析,通过对基本叶集协议行为的细致分析,证明了该协议运行有限时间后,P2P层叠网拓扑总能到达稳定状态,并且层叠网最终的拓扑只有3种类型：环态、多圈态和分离态。验证了基本叶集协议的实验结果。     

H3C中PPP协议的配置

本文对PPP协议进行了阐述,对PPP协议的特点以及PPP协议的会话过程进行了简单介绍,详述了PPP协议的两种验证方式及其在H3C路由器上的实际配置,并对两种验证方式进行了对比。     

ITS专用短程通信的协议验证

针对专用短程通信(DSRC)协议的复杂性以及协议本身由自然语言承载、存在模糊性和二义性的特点,采用协议工程方法来保证协议的完整性、正确性、安全性、可移植性和标准化,并采用SDL对DSRC协议进行形式化描述,在此基础上提出了DSRC协议验证的步骤和实现方法,并对所开发的协议SDL模型进行验证,结果表明了协议的逻辑正确性．     

安全协议的形式化验证技术研究

对安全协议形式化验证方法所应用的技术进行了研究，总结了当前安全协议的各种形式化验证方法的特点，指出今后一段时期内安全协议形式化验证技术的研究方向．     

基于模型检测的SSL协议形式化验证

针对传统的测试方法无法对网络安全协议的逻辑本身进行验证等问题,提出了一套基于形式化分析和SPIN模型检测的验证方法.该方法首先以BAN逻辑对目标协议进行形式化分析,然后推断目标协议存在的问题缺陷,并通过Promela语言对其构建SPIN模型,最后通过SPIN软件验证推断的正确性.并以SSL协议作为具体实例予以论证,结果表明所提方法具可行性.     

基于着色petri网的安全协议验证方法

设计安全协议时，协议的安全性验证是消除安全协议脆弱性和不精确性的关键步骤，验证安全协议的模型和工具有很多．提出了一种基于着色petri网的安全协议验证方法．通过采用该方法对一个STS协议进行了分析，证明了这种方法的有效性，并根据分析结果给出了改进后的STS协议．     

基于WIA-PA协议的时间同步算法的研究与实现

基于时分多址的WIA-PA(wireless networks for industrial automation-process automation)网络中,高精度的时间同步是保证系统可靠、安全、无误、实时地传输的重要条件。通过分析WIA-PA协议以及现有经典时间同步算法的特点,提出了一种适用于WIA-PA协议的时间同步算法。该算法在WIA-PA协议单向时间同步方式的基础上,引入了延迟时间同步算法作为具体的同步算法,通过修改标记时间戳的位置和加入线性回归补偿对其进行改进,从而减少了不确定性因素的影响。在CC2530上得到实现验证,实验结果表明,该同步算法在满足WIA-PA协议规范的情况下,能达到较高的时间同步精度。     

新的三方密钥交换协议

针对基于口令认证机制的密钥交换协议容易遭受口令猜测和服务器假冒等多种攻击的缺点,提出了基于验证值认证机制的新的三方密钥交换协议.新协议中的验证值是基于口令的变换,并代替口令被保存在服务器端.服务器不仅以验证值来认证用户的身份,并且要通过验证值协助用户之间协商出会话密钥.而口令则作为私钥由用户自己保存.对新协议的安全进行分析,表明该协议可以抵御多种攻击,说明协议是安全的,同时对协议的效率评估还表明该协议具有较高的效率.     

NetBill协议的形式化描述及分析

通过对安全协议验证的形式化需求分析,论证了形式化描述和分析是描述电子商务协议并验证它们属性的有效方法.介绍了一个扩展的BAN逻辑,基于这个逻辑对一种电子交易协议NetBill协议进行形式化描述,并在有入侵的情况下对该协议所期望的属性(安全、原子、隐私)进行了正确的分析,证明了该协议在有入侵者的情况下能够满足安全、原子和隐私等要求.     

基于UPPAAL的简单网络支付协议形式化验证

分析简单支付协议中不同银行间的交易行为和各主体的超时约束,建立消费者、商家、银行和超时计时器的时间自动机模型,并用UPPAAL工具验证其是否满足商品原子性。新模型在原模型的基础上,增加了超时计时器进程来负责接收来自其它进程的超时信息,在各主体的计时器触发超时之后,计时器将发送超时信息,再通过外部的仲裁程序来解决纠纷。新模型能够满足货币原子性和商品原子性,并且比原模型更加符合协议运行的实际环境。     

结合多尺度特征和多维注意力的人脸风格转换

针对StarGANv2模型生成的人脸图像存在风格重建效果不佳、人脸纹理不够自然等现象,该文提出结合多尺度特征和多维注意力的人脸风格转换模型.1)将多尺度特征融合模块PSConv嵌入StarGANv2生成器内,提高了模型对图像特征的提取能力;2)提出了多维注意力模块MDConv,并将该模块嵌入StarGANv2判别器内,从而提高了模型对真假人脸图像的判别能力.与StarGANv2方法在CelebA-HQ数据集上进行对比实验的结果表明：该方法生成的人脸图像风格更美观,纹理细节更自然,学习感知图像相似度(LPIPS)的值也得到了提升.     

一种基于UPPAAL的智能合约属性形式化验证方法

针对智能合约的属性验证问题,该文提出了一种基于UPPAAL的智能合约属性形式化验证方法.首先定义了Solidity基本语句的操作语义及其到时间自动机的转换,将智能合约转换成时间自动机网络模型;然后定义并描述智能合约常见的安全性和活性,再使用模型检测工具UPPAAL验证智能合约的属性;最后对购物合约进行了建模与验证,验证了该方法的有效性.     

PC与单片机串行通信的协议策略研究及应用

通信协议是串行通信系统正常运行的关键.通过对PC机与单片机多机串行通信协议中常见问题进行分析,提出了一种通信协议的制定策略.最后以某国际机场LED显示系统为例,完成了系统的通信协议制定和软件实现,验证了此策略在多机串行通信中的可靠性.     

快速公交智能系统通信协议标准研究

对快速公交(BRT)智能系统通信标准发展的国内外现状及需求进行了分析,基于研发实践总结出快速公交智能系统的构成和通信协议体系的构成,并提出了快速公交智能系统通信标准的制定原则、通信协议分层模型及其通信协议的构成内容,总结了基于通信协议标准的系统集成内容.所提出的通信协议标准已在相关工程实践中予以应用,取得了良好效果.     

基于层次时间自动机的移动授权的建模与验证

基于通信的列车运行控制(communication based train control,CBTC)系统以其安全、可靠等性能优点在城市轨道交通的运营中得到广泛关注。它通过其核心功能,即为每一列通信列车提供移动授权(movement authority,MA),来实现列车安全间隔运行。针对功能安全和实时性等方面的不足,首先,建立移动授权的层次时间自动机(hierarchical time automaton,HTA)模型,其中嵌入了列车管理、安全位置、遍历障碍物和列车筛选模块,并对模块间的交互信息进行分析;其次,采用巴科斯范式(Backus-Naur form,BNF)语法对其特性进行描述;最后,利用UPPAAL对各特性验证。结果表明,移动授权模型满足实时性、顽健性、可用性、完整性、安全性5项需求,层次时间自动机理论适用于系统需求规范的验证。     

一种有保证实时通信协议的设计

通过研究实时系统中的报文特点和报文延迟的规律，探讨了有保证实时通信协议的特征，分析了ＭＡＣ层的通信协议在实时通信中的关键作用，据此设计了一种在ＭＡＣ层的有保证实时通信协议——虚拟令牌协议（ＶＴＯＫＥＮ），并与改进型的Ｗｉｎｄｏｗ协议、ＴＤＭＡ协议及令牌协议就报文丢失率与报文生成率的关系进行了模拟对比．模拟对比的结果表明：ＶＴＯＫＥＮ更适合实时通信     

高效类HDLC异步串行通信协议的实现

提出一种高效、 面向字节传送的类似HDLC通信协议的异步串行通信协议AHDLC及其算法的实现, 分析了AHDLC协议的变换效率. 该协议算法简单、 变换效率高, 比用ASCⅡ码方式传送效率提高48.7%, 该协议适用于维护终端及监控终端等需要自己定义通信协议的场合.     

一种基于时间自动机网络的实时系统形式化验证方法

介绍了时间自动机形式模型,在此基础上给出了时间自动机网络的形式语法和语义,然后给出一种基于时间自动机网络的实时系统形式化验证方法,并采用基于时间自动机网络的模型检测工具UPPAAL对一个经典的实时系统实例进行了验证．