基于赋时颜色Petri网的NSSK协议建模

随着对计算机网络应用的不断深入,对网络协议的安全性进行分析和研究已经成为信息安全领域的一个十分重要的研究方向.设计安全协议时,协议的安全性验证是消除安全协议脆弱性和不精确性的关键步骤.验证安全协议的模型和工具有很多,主要应用赋时颜色Petri网分析了安全协议中著名的NSSK协议,应用赋时颜色Petri网的变迁为导向的建模方法,成功地对NSSK协议进行了建模,并验证了协议运行过程中的有效性.为下一步利用颜色Petri网协议针对NSSK协议的安全性进行分析打下了良好的基础.     

CCITT X.509协议的形式化分析及其改进

串空间模型是一种新兴的密码协议形式化分析工具,基于串空间模型的协议认证分析方法是比较常用的验证方法。概述了串空间模型理论和基于串空间模型的认证测试理论,并利用此理论对CCITT X.509协议进行了形式化的分析。该协议存在缺陷并对此进行了改进。     

串空间和认证测试在协议分析中的应用

串空间模型是一种新兴的密码协议形式化分析工具.分别采用串空间模型争认证测试这两种前沿的形式化分析方法对X.509协议的认证性进行了分析,指出了该协议在认证正确性方面存在的缺陷.然后针对分析结论提出了改进协议,并使用认证测试方法证明了改进的协议能够实现认证的正确性.通过比较发现应用认证测试方法分析安全协议,比单纯应用串空间模型更为简洁和直观.     

改进型Helsinki协议的串空间模型分析

Helsinki协议是ISO/IEC DIS 11770-3 中提出的重要认证协议,由于协议受到来自内部的攻击,Mithcell-Yeun对其进行了改进.但改进后协议的安全性仍未得到确认,为了验证改进协议是否满足其安全目标,利用串空间模型对协议进行了建模和分析.通过分析极小元所在串与其它串的关系说明协议的一致性,通过对理想的分析说明协议的保密性.结果表明改进型协议满足其安全要求,原协议存在安全缺陷的原因是最小元可能存在M1串上,这为 Mithcell-Yeun的改进提供了理论的证明与依据.     

一个双向认证协议的分析与改进

运用安全协议形式化分析方法中的串空间模型理论,对Natalia Miloslavskaya等人提出的一个双向认证协议进行了分析,发现该协议在认证方面存在缺陷,并对该协议进行了改进,同时用串空间理论证明了改进后的协议的认证正确性.     

基于带标记串空间模型的安全协议分析

在串空间理论基础上引入了标记模型,扩展了串空间理论.实现了具有类型缺陷的安全协议的分析.本文以RPC协议作为实例,证明改进后的RPC协议,能抵御类型攻击。     

基于串空间模型的Andrew RPC协议的分析与验证

本文首先介绍了当前安全协议形式化验证的前沿方向串空间理论,并运用串空间模型对改进后的Andrew secure RPC协议进行了形式化分析与验证,然后指出了安全缺陷。     

串空间模型对RPC协议机密性的验证

首先介绍了当前安全协议形式化验证的前沿方向串空间理论,并运用串空间模型对改进后的Andrew secure RPC协议的机密性进行了形式化分析与验证。     

Needham-Schroeder 协议的认证测试方法形式化分析

在安全协议的形式化分析方法中,串空间模型和基于串空间模型的认证测试方法是比较常用的验证方法。针对Needham- Schroeder协议存在中间人攻击的缺陷,提出对协议的改进并采用认证测试方法,验证了改进的协议可以满足协议的安全目标。     

Yahalom协议的分析及改进方案

Yahalom协议及BAN对Yahalom协议的改进协议都存在着安全缺陷.采用串空间模型,运用"理想"和"诚实"作为工具对Yahalom协议的安全性进行了分析并找出了该协议遭受攻击的主要原因,同时提出了Yahalom协议的一种改进方案.     

串空间模型中认证性测试方法的缺陷

指出了串空间模型中认证性测试方法存在的不足：1．分析认证性的过程中未考虑同一协议主体同时以不同身份参与协议运行的情况；2．分析认证性的过程中未考虑发生多轮协议同时运行的情况；3．认证性测试方法不能分析类型错误攻击。通过实例-——Needham-Schroeder协议分析了认证性测试方法存在不足的原因，并提出了改进方案。     

CTCT-4级安全通信协议的形式化建模与验证

CTCS-4级列车运行控制系统是基于无线通信GSM-R传输信息的系统,而GSM-R系统是一种开放传输系统,它不能满足列控系统这种安全苛求系统的需求。主要根据GSM-R系统现有的安全威胁和应该采取的安全措施,引用一种改进的NSSK安全协议来保障车载设备与RBC间安全通信,并利用形式化建模语言CSP和模型检测工具FDR对其建模和验证。     

一种移动分布式实时事务原子提交协议

介绍了移动分布式实时事务的工作模式,在此基础上提出了应用于移动分布式实时事务的实时原子交换协议:两层实时原子提交协议.通过引入改进的TCP三次握手协议,完成移动终端与固定数据库系统的交互.对协议的正确性进行了证明.两层实时原子提交协议能够有效避免由于网络故障或者移动终端故障引起的通信堵塞.     

基于串空间的安全协议自动化验证算法

以串空间模型为理论基础,提出安全协议自动化验证算法IVAP。对于有漏洞的协议,针对不安全属性逆向搜索主体串树,自动生成改进协议并对其进行验证,直至生成一个安全的改进协议。实验结果证明了该自动化验证算法的有效性,与AAAP算法相比,其协议验证效率更高。     

串空间模型的原理与应用

介绍了安全协议形式化分析方法串空间模型的基本概念,给出了检查消息机密性的定理的变形公式,形式化地证明了由未泄漏私钥签字的消息起源于诚实主体串,并利用上述结论检验了BAN修改后的CCITTX.509(3)协议的机密性和认证性。     

认证测试方法对TLS协议的分析及其应用

TLS(传输层安全)协议被广泛用来保证Web的安全,为了分析其安全性,用串空间模型对其进行形式化描述,并用认证测试方法分别对客户端和服务器端的认证性进行分析,证明协议存在中间人攻击,通过修改认证测试方法的测试元素对协议形式进行改进,并证明改进后协议的正确性.     

基于可视化技术的网络协议分析

研究TCP/UDP协议过程分析方法以及基于可视化技术的协议实现过程,实现一个基于Linux和GTK+的网络协议分析软件。通过对TCP/UDP协议的可视化分析,追溯网络数据的传输过程,将网络数据之间的关系和TCP/UDP协议的实现过程以可视化技术进行展现,并将数据转化为可读性强并易于理解的形式展现出来,有助于网络协议学习者更加直观地了解TCP协议的工作原理,从而更好地去分析并设计应用层的协议。     

基于模型检测的OpenFlow多交换机数据包转发协议的分析与验证

OpenFlow协议是SDN网络中控制平面与数据转发平面之间进行交互的规范与标准,其正确性将直接影响到整个网络功能的实现。通过模型检测技术实现一种验证OpenFlow协议正确性的形式化方法。首先提取OpenFlow协议的核心子协议,即OpenFlow多交换机数据包转发协议作为验证的实例;然后运用协议行为自动机对该子协议进行形式化建模,并且通过时态逻辑描述协议需要进行验证的性质;最后给出算法验证协议模型是否满足给定的性质要求,以此检测OpenFlow协议是否存在正确性漏洞,以便对其进行修正。