基于ProVerif的安全协议形式化分析与验证

形式化方法是分析与验证安全协议属性的强有力的工具.在对一阶定理证明器ProVerif深入研究的基础上,对简化的Needham-Schroeder认证协议进行了形式化分析.     

基于事件逻辑的改进Needham-Schroeder协议安全性证明

安全协议是现代网络安全的基础,密码协议的安全性证明是一个挑战性的问题。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于刻画安全协议的形式化描述,是定理证明的基础。用事件序语言、事件类和一个表示随机数、密钥、签名和密文的原子类,给出身份认证协议可以被形式化定义和强认证性证明理论。利用该理论对增加时间戳的Needham-Schroeder协议安全性进行证明,证明改进的Needham-Schroeder协议是安全的。此理论适用于类似复杂协议形式化分析与验证。     

基于树语言逼近的安全协议形式化分析

利用形式化方法或工具自动化分析实用安全协议十分必要,定理证明技术因其可解决无限状态系统的验证备受关注,但扩展其验证规模和自动化实现时仍然存在一些局限性。以定理证明和重写逼近理论为基础,以项重写形式化定义协议模型,以树自动机模拟协议攻击者知识集,给出攻击者知识集可达项逼近求解的算法,并根据上述模型讨论秘密性和认证性的验证方法,最后以Needham-Schroeder公钥认证协议为例验证模型的有效性,并指出下一步研究方向。     

SpaceWire译码电路在HOL4中的形式化验证

SpaceWire是在苛刻环境下的高速通信总线协议,译码电路是其接收端的关键电路,对该电路进行形式化验证具有重要的现实意义.形式化验证方法中的定理证明将需要分析的电路进行形式化建模,结合定理证明器,对模型的性质进行严格推理从而完成验证.本文运用定理证明的方法,在高阶逻辑证明工具HOL4中对SpaceWire总线的译码电路进行形式化验证.首先根据SpaceWire标准规范抽取相关性质,用高阶逻辑语言形式化描述;然后分析电路设计中的VHDL代码,依据代码实现的功能用相应的逻辑谓词建模;最后在HOL4中证明了译码电路设计的模型能满足所提取的性质.本文同时给出了形式化建模的方法和验证过程.     

基于Coq的软件安全性验证

针对数组越界、空指针应用和缓冲区溢出三类威胁软件安全的不规范操作,提出了一种基于Coq验证上述三类操作的形式化方法。首先编写三类安全问题的程序实例,并采用形式化方法进行标注;其次运用Frama-C和Why工具对标注程序进行解析,生成需要证明的定理;最后基于Coq集成开发环境证明定理,实现安全问题的验证。结果表明,该方法有效验证了软件安全中的三类问题,为形式化方法在软件安全性验证方面的应用奠定了基础。     

一种安全协议的形式化设计方法

文章以协议分析器为辅助工具,结合定理证明方法,给出了一个安全协议形式化设计方法。该方法首先根据协议规范构造全信息项及冗余协议,使用定理证明保证冗余协议的安全性。对冗余协议利用安全性保持约简规则和随机约简规则进行约简,从而得到最优约简协议。该方法实现了安全协议的自动设计,具有良好的扩展性,可以根据需求和协议的发展增加设计规则和约简规则。     

GJK算法的一种特殊情形的形式化验证和应用

计算几何算法经常用于机器人避碰运动规划等安全攸关领域,对这些算法进行正确性证明非常重要.用形式化方法对算法进行验证是一种十分有效的手段,尤其是定理证明的方法用严格的数学公理和定理推理证明逻辑模型的性质,对所验证的性质而言是完备的.基于GJK算法设计了计算空间两条线段间距离的算法,用定理证明器HOL4对其相关的定义和定理进行形式化定义和证明,进而基于霍尔逻辑完成形式化表示和证明,对该算法的正确性实现了形式化验证.最后,给出了这一经过验证的算法在双臂机器人无碰撞运动规划中的应用.     

C2P:基于Pi演算的协议C代码形式化抽象方法和工具

形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基于Pi演算模型对协议安全属性形式化验证.最后,给出了方案转换的正确性证明,并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合,能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.     

拟态路由器TCP代理设计实现与形式化验证研究CSCD

拟态路由器基于拟态防御的动态异构冗余架构进行设计,对于未知漏洞后门具有良好的防御能力。协议代理在拟态路由器中处于内外联络的枢纽位置,协议代理的安全性和功能正确性对于拟态路由器有着重要意义。本文设计实现了拟态路由器的TCP协议代理,并采用形式化方法,对其安全性和功能正确性进行了验证。TCP协议代理嗅探邻居和主执行体之间的TCP报文,模拟邻居和从执行体建立TCP连接,并向上层应用层协议代理提供程序接口。基于分离逻辑与组合思想,采用Verifast定理证明器,对TCP协议代理的低级属性,包括指针安全使用、无内存泄露、无死代码等,进行了验证;同时,还对TCP协议代理的各主要功能模块的部分高级属性进行了形式化验证。搭建了包含3个执行体的拟态路由器实验环境,对实现结果进行了实际测试,结果表明所实现的TCP代理实现了预期功能。TCP协议代理实现总计1611行C代码,其中形式化验证所需人工引导定理检查器书写的证明共计588行。实际开发过程中,书写代码实现与书写人工证明所需的时间约为1︰1。本文对TCP协议代理的实现与形式化验证工作证明了将形式化验证引入拟态路由器的关键组件开发中是确实可行的,且证明代价可以接受。     

拟态路由器TCP代理设计实现与形式化验证研究

拟态路由器基于拟态防御的动态异构冗余架构进行设计,对于未知漏洞后门具有良好的防御能力。协议代理在拟态路由器中处于内外联络的枢纽位置,协议代理的安全性和功能正确性对于拟态路由器有着重要意义。本文设计实现了拟态路由器的TCP协议代理,并采用形式化方法,对其安全性和功能正确性进行了验证。TCP协议代理嗅探邻居和主执行体之间的TCP报文,模拟邻居和从执行体建立TCP连接,并向上层应用层协议代理提供程序接口。基于分离逻辑与组合思想,采用Verifast定理证明器,对TCP协议代理的低级属性,包括指针安全使用、无内存泄露、无死代码等,进行了验证;同时,还对TCP协议代理的各主要功能模块的部分高级属性进行了形式化验证。搭建了包含3个执行体的拟态路由器实验环境,对实现结果进行了实际测试,结果表明所实现的TCP代理实现了预期功能。TCP协议代理实现总计1611行C代码,其中形式化验证所需人工引导定理检查器书写的证明共计588行。实际开发过程中,书写代码实现与书写人工证明所需的时间约为1:1。本文对TCP协议代理的实现与形式化验证工作证明了将形式化验证引入拟态路由器的关键组件开发中是确实可行的,且证明代价可以接受。     

基于GSPM的安全协议检验工具

介绍一个基于GSPM的安全协议验证的图形化工具。验证工具以GSPM模型为基础形式化地描述了安全协议,并引进线性时序逻辑刻画了安全协议的性质,用基于状态搜索的模型检测方法在安全协议的验证过程中找出漏洞。以简化的NSPK协议为例,描述了该工具如何验证安全协议,表明GSPM模型和验证算法的有效性和正确性。     

安全协议扩展Petri网模型及检测

协议安全性分析是网络安全的一个难题,运用形式方法对协议进行安全分析和检测,找出安全漏洞仍是该领域的研究热点。本文提出了一种新的基于扩展Petri网的安全协议建模方法,并且使用该方法对经典协议做了建摸、分析和检测,构造了攻击模型,证明了这种方法的有效性。     

基于Spi演算的SSL3.0安全协议仿真分析

安全协议中的错误和漏洞很难完全由人工来发现，借助形式化方法对其进行分析可以保证安全协议的正确件和完整性。目前安全协议的形式化分析和验证已成为网络安全的研究热点，其中基于Spi演算的模型验证方法足当前的一个重要研究领域。文章介绍了SSL3．0安全协议的握手过程和Spi演算的基本概念，包括基于spi演算认证性的验证方法。存此基础上，基于spi演算形式化地建立了SSL3．0安全协议的仿真模型，给出了分析SSL3．0安全协议的详细过程，最终验证了SSL3．0安令协议的认证性。仿真分析的结果表明，Spi演算能够为安全协议的分析和验证提供可靠和有效的支持。     

安全协议自动验证工具的状态空间剪枝

串空间模型是分析安全协议的一种实用、直观和严格的形式化方法。概述基于该模型结合使用定理证明和模型检测技术开发的安全协议验证工具AVSP的体系结构，提出一些剪枝规则对状态搜索空间进行剪枝。通过Needham-Schroeder安全协议的弱一致性认证属性验证过程来表明这些状态搜索空间剪枝规则可有效缩小状态搜索空间，防止状态空间爆炸。     

Identity-based deniable authentication for ad hoc networks

Deniable authentication is an important security requirement for ad hoc networks. However, all known identity-based deniable authentication (IBDA) protocols are lack of formal security proof which is very important for cryptographic protocol design. In this paper, we propose a non-interactive IBDA protocol using bilinear pairings. Our protocol admits formal security proof in the random oracle model under the bilinear Diffie-Hellman assumption. Our protocol is faster than all known IBDA protocols of its type. In addition, our protocol supports batch verification that can speed up the verification of authenticators. This characteristic makes our protocol useful in ad hoc networks.     

Kaman协议的形式化验证

Kaman协议是移动Ad Hoc网络安全认证机制,然而,协议设计者未对该协议的安全性作严格的形式化分析。协议复合逻辑PCL是验证协议安全属性的形式化方法,PCL逻辑能够简化协议安全分析过程。本文在协议复合逻辑PCL中描述Kaman协议并分析Kaman协议的安全属性,证明Kaman协议能够实现其安全目标。     

基于强化学习的安全协议形式化验证优化研究

使用形式化方法能够找到安全协议设计中存在的漏洞,但高效地对安全协议进行自动的形式化分析仍然是一个挑战。针对现有形式化自动验证工具无泛化性和效率低的不足,对基于强化学习的安全协议形式化验证框架smartVerif进行优化。使用无人工特征、完全进行自我学习的蒙特卡洛树搜索与深度神经网络相结合的强化学习框架,同时设计能够保留形式化数据结构信息的数据转换方法。实验结果表明,利用该优化方案训练的强化学习模型具有泛化性且能高效地验证安全协议。     

安全协议形式化验证方法的比较与分析

网络的飞速发展,使得安全问题日益突出,而身份认证协议则是安全性的基础。目前国际上的热点是安全协议的形式化验证。文章从两个角度介绍安全协议形式化验证的方法：证明与证伪。对其各自特点进行比较与分析。     

典型安全协议形式化分析工具比较

介绍了当前安全协议分析领域的典型形式化工具,阐述了其基本原理和在协议描述、归约、验证方面的研究现状,对它们的优缺点进行了综合比较,提出了如何在已有条件下开发协议分析工具的观点。     

Chosen-name Attacks: An Overlooked Class of Type-flaw Attacks

In the context of Dolev-Yao style analysis of security protocols, we consider the capability of an intruder to dynamically choose and assign names to agents. This capability has been overlooked in all significant protocol verification frameworks based on formal methods. We identify and classify new type-flaw attacks arising from this capability.Several examples of protocols that are vulnerable to this type of attack are given, including Lowe's modification of KSL. The consequences for automatic verification tools are discussed.