802.11i双向认证协议的模型检查

确保安全协议的正确性对于保证Internet上安全敏感的业务非常重要。采用形式化方法建模和验证安全协议可以检测到传统测试手段难以发现的错误。模型检查作为形式化验证方法的一种,有着自动化和提供反例等诸多优点。使用模型检查工具SPIN对802.11i双向认证协议EAP-TLS进行验证,提取出包含协议设计重要细节的形式化模型,对协议安全属性采用线性时态逻辑抽象,并验证协议模型是否满足安全属性。提出了一种使用PROMELA建模认证协议的方法。     

关于秘密共享方案在应用Pi演算中的实现

针对秘密共享方案的自动化验证问题,提出一种基于等值理论的秘密共享方案自动化验证方法。首先通过等值理论在应用Pi演算中对可验证的多秘密共享方案的密码学语义进行了形式化定义。在此基础上,进一步提出了一种用于将所提出等值理论转化为自动化协议验证器ProVerif中重写机制的编码方法,在ProVerif中实现了关于可验证的多秘密共享方案的自动化验证。通过证明给出了关于可验证的多秘密共享方案形式化分析结果的健壮性结论：如果自动化协议验证器ProVerif中可验证的多秘密共享方案的形式化分析结果满足特定安全属性,则其能够归约证明应用Pi演算模型中针对可验证的多秘密共享方案所建立的现实敌手可以“模拟”ProVerif验证器中的理想敌手,其意味着现实敌手与理想敌手是不可区分的。     

基于RGPS服务本体交互建模分析与验证

在动态、异构和自治的互联网服务环境中,对WEB服务组合的形式化分析与验证是保证按需服务应用的有效途径,寻找有效的形式化分析方法和工具是热点领域.针对现有研究主要是集中于服务组合流程和静态结构方面,而在动态反映用户需求的服务组合及支持服务的动态耦合存在不足.本文从服务本体的语义层面,通过对OWL-S进行RGPS属性扩充,研究SOA架构模型映射到Pi演算的进程模型,对动态耦合的按需服务组合进行形式化分析并用Pi演算验证工具MWB进行验证.实验结果表明方法的可行性,为按需动态服务组合的有效性分析提供了一种验证方法.     

一种自动化模型检测ANSI-C程序的实用方法

模型检测是一种验证有限状态系统的时序逻辑属性的形式化方法。为了利用模型检测技术,通常的办法是手工构建一个抽象模型,然而这个方法存在一些不足,如成本过高、易引入建模错误等。本文提出了一种自动化模型检测ANSI-C程序的方法,并开发了模型提取工具C2Spin,它能够分析ANSI-C源代码,并生成对应的PROMELA验证模型,从而显著降低了建模的开销。利用C2Spin,模型检测工具SPIN可以自动地检测使用C语言编写的应用程序中的多种错误,如死锁等。在初步实验中,依靠C2Spin生成的模型,我们发现了SPIN4.3.0的一个语义错误,以及Holzmann对两个经典互斥算法的实现程序中的活锁错误。这些结果表明,C2Spin能够帮助人们更加快速有效地测试C程序。     

SPI演算规范的建模、实现验证研究

针对安全协议安全属性是否满足，缺乏有效性能评价方法的现状，大都使用SPI演算或相近的进程代数方法进行建模。利用这种方法不仅能够有效地形式化描述安全协议，并且能够对安全协议进行多方面的系统评价，但基本上没有说明怎么样寻找设计合适的验证工具，验证其安全属性实现的正确性。本文引入基于SPI演算的验证工具SPRITE来保证建模过程正确性，并设计给出实现映射的具体方法。本方法通过对典型的WOO-LAM单向认证协议予以说明，最后SPRITE产生的具体JAVA代码，给出了安全协议的安全属性，使形式化描述的协议的安全属性是否满足更接近于人的理解而不仅只是机器的解释。     

SPVT:一个有效的安全协议验证工具

描述了基于Objective Caml开发的一个安全协议验证工具SPVT(security protocol verifying tool).在SPVT中,以扩展附加项的类(演算作为安全协议描述语言,以扩展附加项的Horn逻辑规则描述协议攻击者的Dolev-Yao模型,通过一组抽象规则将安全协议的类(演算模型转换为逻辑程序模型,基于安全协议逻辑程序的不动点计算验证安全性质,从安全协议逻辑程序的不动点计算和安全性质的验证过程中构造不满足安全性质的安全协议反例.以简化的Needham-Schroeder公钥认证协议为例,描述了使用SPVT自动验证安全协议的过程,表明了SPVT用于安全协议验证的有效性.     

基于安全协议代码的形式化辅助建模研究

随着安全协议形式化分析技术的不断发展,利用工具自动验证虽已得到实现,但建模环节仍需依赖专业人员手工建模,难度大且成本高,限制了此技术的进一步推广。为了提高建模的自动化程度,提出了依据安全协议代码进行形式化模型辅助生成的方案。首先,使用污点分析获取协议的通信流程,并且记录密码学原语操作;然后,根据通信流程之间的序列关系构建协议通信状态机;最终,根据目前主流的安全协议形式化分析工具Tamarin的模型语法生成形式化模型。实验结果表明,此方案可以生成形式化模型中的关键部分,提高了形式化建模的自动化程度,为形式化分析技术的推广作出贡献。     

基于Pi演算的OWl-s的Web服务的自动组合

Web服务组合研究领域的一个重要的问题是如何形式化描述Web服务组合,如何验证服务组合的正确性。Web服务组合的形式化模型可以用来检查、验证Web服务组合以保证组合的正确性。针对目前最主要的一种语义Web服务组合的规范WEB本体论语言(Ontology Web Langage-Semantic,简称OWL-S),给出基于Pi演算的形式化描述,定义了Pi演算和OWl-S之间的概念映射,并给出了OWl-S的基于Pi演算的形式化模型,最后通过一个案例给出了模型验证的方法。     

基于环境敏感互模拟的Kerberos协议形式化分析

进程演算通常用来研究交互式反应系统,其中的互模拟方法是用来形式化验证系统属性的重要途径.首先扩展了进程演算中的Spi演算,并将其应用于形式化描述网络安全协议--Kerberos协议的安全属性.为了验证该协议所声称的安全属性,引入了Spi演算中环境敏感互模拟的方法,即两个系统与环境发生交互过程中是否互模拟.通过采用该互模拟关系对Kerberos协议两个安全属性--可认证性和保密性--的证明,发现其可认证性是可靠的,而保密性存在一个可能的漏洞.最后,指出了基于互模拟的安全协议形式化验证方法今后值得进一步研究的方向.     

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

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

基于Pi-演算的Web服务组合的描述和验证

形式化方法对于建模和验证软件系统是一种有效的方法,所以对Web服务的形式化描述和验证是一个重要的研究方向．对于Web服务及其组合来说,保证其组合正确性以实现其服务增值是十分必要的．Pi-演算是一种移动进程代数,可用于对并发和动态变化的系统进行建模．该文基于Pi-演算对Web服务及其组合进行形式化描述和建模．文中说明了Pi-演算与以前形式化方法的不同之处,分析了Pi-演算应用于Web服务组合需要解决的问题．讨论了Pi-演算与Web服务协议栈的对应关系,说明了利用Pi-演算建立Web服务组合模型的规则,指出了如何寻找代理和通道．最后建立了一个实际的模型,并利用形式化工具对建立的组合模型是否正确以及是否满足需求进行了验证．     

利用类型推理验证Ad Hoc安全路由协议

提出一种基于类型推理的移动Ad-Hoc网络安全路由协议的形式化验证方法.定义了一种邻域限制通信演算NCCC(neighborhood-constrained communication calculus),包括演算的语法和基于规约的操作语义,在类型系统中描述了移动Ad-Hoc网络路由协议的安全属性,定义了近似攻击消息集用以精简Dolev-Yao攻击模型.还给出了该方法的一个协议验证实例.基于类型推理,该方法不仅能够验证协议的安全性,也可以得出针对协议的攻击手段.因为攻击集的精简,有效地缩减了推理空间.     

源程序语义检测的稳定模型分析方法

基于逻辑程序及其稳定模型的理论,提出一种源程序语义检测的稳定模型分析方法。该方法从源程序中提取关键语句图,将安全知识规则转换为一个逻辑程序,再用关键语句图去实例化该逻辑程序,最后求解其稳定模型得到源程序的安全性评价。该方法体现了源程序丰富的语义,具有较好的可扩展性。     

模型学习与符号执行结合的安全协议代码分析技术

符号执行技术从理论上可以全面分析程序执行空间,但对安全协议这样的大型程序,路径空间爆炸和约束求解困难的局限性导致其在实践上不可行。结合安全协议程序自身特点,提出用模型学习得到的协议状态机信息指导安全协议代码符号执行思路;同时,通过将协议代码中的密码学逻辑与协议交互逻辑相分离,避免了因密码逻辑的复杂性导致路径约束无法求解的问题。在SSH协议开源项目Dropbear上的成功实践表明了所提方法的可行性;通过与 Dropbear 自带的模糊测试套件对比,验证了所提方法在代码覆盖率与错误点发现上均具有一定优势。     

基于π演算的工作流模型检验

为保证工作流模型语义的正确性,提出一种基于π演算的工作流模型语义性质检验方法。采用π演算的一个子集πN演算描述工作流模型,证明该模型的反应关系能够终止,构造有限反应迁移图算法,利用NuSMV检验工作流模型是否满足线性时序逻辑性质。实验结果证明了该检验方法的有效性。     

基于Pi演算的Android App权限提升攻击检测

针对Android App权限提升攻击的问题,基于Pi演算构建了一个形式化的权限提升攻击检测模型。利用扩展后的Pi演算对Android App及其运行时环境进行建模,得到形式化的行为模型;通过将权限安全策略形式化的表示为包含进程表达式的IF-THEN规则,并利用Pi演算的性质进行进程演算和迁移,构建了检测模型,并给出了权限提升攻击检测的方法。理论分析和实验表明,该方法具有线性的时间和空间复杂度,并可以非常容易地将现有的权限安全策略应用在该模型中,保证了模型的精确性。相比其他方法,该方法在提高检测精确性的同时并没有牺牲检测的效率。     

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

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

Otway-Rees协议并行攻击的SG逻辑分析

网络信息安全很大程度上取决于密码协议的安全，重放攻击和并行攻击是对密码协议的常见攻击，能够分析并行攻击的形式化分析方法并不多见。该文介绍了一种分析密码协议并行攻击和重放攻击的逻辑方法——SG逻辑，应用它对改进版的Otway-Rees协议进行了分析，找出了BAN类逻辑所不能分析出来的缺陷，针对该缺陷给出了协议的进一步改进，并推证了改进后的协议对SG逻辑的分析是安全的。     

Semantic interpretation of Compositional Logic in Instantiation Space

The formal methods for security protocols guarantee the security properties of protocols. Instantiation Space Logic is a new security protocol logic, which has a strong expressive power. Compositional Logic is also a useful security protocol logic. This paper analyzes the relationship between these two logics, and interprets the semantics of Compositional Logic in Instantiation Space model. Through our work, the interpreted Compositional Logic can be extended more easily. Moreover, those security protocols described in Compositional Logic can be automatically verified by the verifier of Instantiation Space. The paper also proves that the expressive power of Instantiation Space Logic, which can not be completely interpreted by Compositional Logic, is stronger than Compositional Logic.