基于进程代数安全协议验证的研究综述

安全协议用于实现开放互联网络的通信安全，进程代数是一类使用代数方法研究通信并发系统理论的泛称，基于进程代数的安全协议验证是以进程代数作为安全协议描述语言的安全协议形式化验证方法．描述了基于进程代数的安全协议验证研究的4种主要方法：基于踪迹语义的方法；基于互模拟验证的方法；基于类型理论的方法；基于逻辑程序的方法．并给出了基于进程代数的安全协议验证进一步的研究方向．  

龙芯2号微处理器的功能验证

开发龙芯2号这样的高性能通用处理器是一项极其复杂的艰巨任务．龙芯2号处理器的设计规模和复杂度比龙芯1号增加了许多倍，如何保证设计的正确性是一个重大挑战．简单的系统级测试已经不能满足设计的需要，这就要求采用多种有效的、先进的验证方法和工具帮助设计者尽可能早的发现和改正设计错误．主要介绍了在龙芯2号处理器的设计开发过程中采用的功能验证流程和主要验证方法．模拟仿真是主要的验证手段，新的形式化验证方法也应用到了验证流程当中．  

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

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

一个安全、原子的电子商务协议及其形式化验证

电子商务的普及与接受主要取决于下述属性的解决：安全、原子、隐私与匿名，形式化描述和分析是描述电子商务协议并验证它各性的有效方法，面向物理商品交易的电子商务协议需要具备３个属性：安全、原子和隐私，介绍了一个安全、可靠的电子商务协议ＢＥＡＲＣＡＴ及其形式化描述，并龙有人侵者的情况下，通过用ＢＡＮ类型的逻辑证明所期望的属性的方式对协议的强度和正确性作形式化分析。  

基于串空间的安全协议形式化验证模型及算法

网络安全在信息时代非常重要，而网络安全的关键问题之一是安全协议。首先介绍了当前安全协议形式化验证的前沿方向－－串空间理论，随后阐述了基于该理论设计的自动验证模型－－T模型，给出了该模型的算法及描述，并通过验证改进前后的Needham-Schroeder协议来说明T模型的优势。  

一种基于扩展有限自动机验证组合Web服务的方法

为简化并自动化组合Web服务验证,提出一种基于扩展有限自动机(extended deterministic finite automata,简称EDFA)验证组合Web服务的方法.使用EDFA可以准确地描述Web服务:EDFA的状态表达Web服务在与用户交互的过程中维护的状态;EDFA的状态转移及其标注描述Web服务与用户间的消息交换.EDFA给出Web服务交互过程的所有消息交换序列,刻画出Web服务的动态行为.使用基于EDFA的组合Web服务验证方法不但可以验证组合Web服务是否满足系统需求,还可以验证组合Web服务运行过程是否有逻辑错误.与其他方法相比,该方法更适于验证开放式环境下的组合Web服务.  

安全协议的扩展Horn逻辑模型及其验证方法

分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法，针对它们构造不满足安全性质的安全协议反例的不足，提出了安全协议的扩展Horn逻辑模型和修改版本的安全协议验证方法，使得能够从安全协议的扩展Horn逻辑模型和修改版本的安全协议验证过程中自动构造不满足安全性质的安全协议反例．在基于函数式编程语言Objective Carol开发的安全协议验证工具SPVT中，实现了上述算法，验证了算法的正确性．  

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

对标准Spi演算的语法及语义进行了合理扩展，并利用扩展后的Spi演算对大型复杂协议SSL V3.0的安全性进行了形式化分析，得出了与其他分析方法相同的结论。  

并发和实时系统的模型检验技术

模型检验是一种重要的自动验证技术，通过显式状态搜索或隐式不动点计算来验证并发或实时系统的模态／命题性质，以保证通信协议、数字电路等设计的正确性。详细阐述了模型检验技术的发展与研究现状。首先描述了并发系统分别基于自动机理论和符号化的两种主要模型检验策略，并给出解决状态爆炸问题的主要方法；然后介绍了针对实时系统以及面向对象设计的模型检验方法；对每种方法都介绍了相应的典型工具，最后分析了模型检验面临的困难以及今后的发展趋势。  

模型检测中状态爆炸问题研究综述

模型检测已成为保证软件系统正确性和可靠性的重要手段,但随着软件功能日益强大,其规模和复杂度也越来越大,在模型检测过程中容易产生状态爆炸问题。如何解决模型检测中的状态爆炸,已成为工业界和理论界无法回避的重要课题。系统地综述模型检测领域解决状态爆炸问题的关键技术和主要方法,并提出该领域的最新研究进展与方向。