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

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

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

伴随着网络和通信的迅速发展,安全已经成为一个备受关注的问题,为确保不同系统的安全,出现了许多的安全协议.文中描述了安全协议验证的形式化需求,并且详细阐述了目前流行的几种形式化的验证技术及各自的优缺点,探讨了形式化验证技术所面临的挑战,指出目前在这方面所做的工作以及有待发展的方向.     

安全协议认证的形式化方法研究

安全协议认证是网络安全领域中重大课题之一。形式化方法多种多样。该文首先论述了模型检测技术及其在安全协议验证中的应用,然后介绍了各种定理证明方法和定理证明工具,接着讨论其它形式化验证方法,最后论述形式化方法的一些研究方向。     

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

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

电子商务中安全协议的验证方法

该文简述了电子商务中的安全协议验证技术,对目前的一些重要的研究方法进行了分析和比较,重点针对形式化的方法在电子商务中的安全协议验证中的优势和不足,结合实际,提出了一些可能的发展趋势。     

大型复杂协议的形式化分析方法研究

大型复杂协议的形式化分析是目前研究的一个热点和难点.根据所采用技术的特点,将大型复杂协议的形式化分析方法分为基于逻辑推理的方法、基于模型检测的方法、基于定理证明的方法和基于进程代数的方法,并简要介绍了各类方法的代表性方法及验证器,最后对各类方法的特点进行分析和比较.指出迭式大型复杂协议的形式化分析方法未来的一个研究重点,修改原有方法或设计一种新的方法,使其既易自动化实现,又能用于复合协议的分析和验证.     

安全协议的形式化验证方法概述

安全协议验证是网络安全领域中重大课题之一,目前对安全协议进行分析的主流方法是形式化方法。该文对现在常用的几种形式化验证方法进行了概述和分析,最后针对形式化技术在该领域的发展前景提出了自己的见解。     

基于Spin的安全协议形式化验证技术

针对安全协议的形式化验证问题,运用模型检测方法,以一种改进的入侵者Promela语义模型,对双方密钥分配中心协议进行Spin模型检测,验证发现其不满足线性时序逻辑（ LTL）公式描述的安全性,得到了原协议的安全漏洞。针对该漏洞,提出了一种协议改进方案,并针对改进后的协议,给出新的Promela语义模型的建模方法。改进的入侵者模型建模方法比起原方法：模型检测过程中的存储状态数减少,使模型复杂度降低约40';迁移状态数减少,使验证效率提升约44'。     

操作系统形式化设计与验证综述

对操作系统的形式化设计和验证的概念进行介绍,描述其框架和基本方法。比较和分析操作系统宏内核和微内核结构,调查多个设计和验证项目,阐述项目的验证目标、方法、优缺点和进展情况。在总结研究现状的基础上,分析和展望操作系统形式化设计和验证的发展趋势,从操作系统模型设计、验证工具、代码实现和验证重用等方面给出形式化设计和验证的思路。     

基于进程代数的TCG远程证明协议的形式化验证

可信计算组织(Trusted Computing Group,TCG)的远程证明协议是最早提出的远程证明的解决方案,其协议的形式化验证对于工程实施具有重要意义.分析了TCG远程证明协议的两种形式——直接证明协议和借助可信第三方的证明协议,对它们进行了抽象处理,得到了两种协议形式的抽象模型.在抽象模型的基础上,给出了基于进程代数的形式化描述,并分别进行了形式化验证,验证结果表明两种协议形式的并行系统均展示了期望的外部行为.     

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

伴随着网络和通信的迅速发展，安全已经成为一个备受关注的问题，为确保不同系统的安全，出现了许多的安全协议。文中描述了安全协议验证的形式化需求，并且详细阐述了目前流行的几种形式化的验证技术及各自的优缺点，探讨了形式化验证技术所面临的挑战，指出目前在这方面所做的工作以及有待发展的方向。     

在形式验证和ATPG中的布尔可满足性问题

介绍布尔可满足性(SAT)求解程序在测试向量自动生成、符号模型检查、组合等价性检查和RTL电路设计验证等电子设计自动化领域中的应用．着重阐述如何在算法中有机地结合电路拓扑结构及其与特定应用相关的信息，以便提高问题求解效率．最后给出下一步可能的研究方向。     

混成系统形式化验证

混成系统是实时嵌入式系统的一种重要子类,其行为中广泛存在离散控制逻辑跳转与连续实时行为交织混杂的情况,因此行为复杂,难以掌握与控制.由于此类系统广泛出现在工控、国防、交通等与国计民生密切相关的安全攸关的领域,因此,如何对相关系统进行有效的分析与理解,从而保障系统安全运营,是一项具有重要意义的工作.常规的系统安全性分析手段,如测试、仿真等仅能在一定输入的情况下运行系统来观测系统行为,无法穷尽地检测复杂混成系统在所有可能输入下的行为,因此并不足以保证系统的安全性.区别于测试等方法,形式化方法通过求解系统模型状态取值范围等方法来确认系统模型中一定不会出现相关错误.因此,其对于保障安全攸关混成系统的安全性具有十分重要的意义.形式化方法由形式化规约与形式化验证两个方面构成.因此从以上两个角度分别对形式化规约方向上现有混成系统建模语言、关注性质以及形式化验证方向的混成系统模型检验、定理证明的现有主要技术与方法进行了综述性的回顾与总结.在此基础上,针对现阶段实时嵌入式系统复杂化、网络化的特性,对混成系统形式化验证的重要关注问题与研究方向进行了探索与讨论.     

Formal Verification of a Consensus Algorithm in the Heard-Of ModelReal-Time Embedded Systems Using VDM

Distributed algorithms are subtle and error-prone. Still, very few of them have been formally verified, most algorithm designers only giving rough and informal sketches of proofs. We believe that this unsatisfactory situation is due to a scalability problem of current formal methods and that a simpler model is needed to reason about distributed algorithms. We consider formal verification of algorithms expressed in the Heard-Of model recently introduced by Charron-Bost and Schiper. As a concrete case study, we report on the formal verification of a non-trivial Consensus algorithm using the proof assistant Isabelle/HOL.     

Formal Verification of Square Root Algorithms

We discuss the formal verification of some low-level mathematical software for the Intel® Itanium® architecture. A number of important algorithms have been proven correct using the HOL Light theorem prover. After briefly surveying some of our formal verification work, we discuss in more detail the verification of a square root algorithm, which helps to illustrate why some features of HOL Light, in particular programmability, make it especially suitable for these applications.     

面向特征编程范式的形式化验证技术研究综述

以面向对象编程范式开发软件经常面临类(Class)与用户需求项无法直接对应的尴尬,面向特征编程范式(FOP)旨在解决这个问题,因此具有重要意义。本文首先简介了FOP编程范式的思想,它与面向方面编程范式的异同,以及它给相应的形式化验证技术带来的挑战;然后综述了现有的FOP形式化验证方法以及我们所做的相关工作,比较了它们的优缺点;最后讨论了FOP形式化验证今后可能的研究方向。     

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

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