安全协议的可视化分析和设计研究

基于模态逻辑的安全协议形式化分析方法一直备受关注。本文在简述一个基于GNY逻辑实现的可视化集成工具的基础上，以SSL协议为例，详细阐述其自动分析过程。最后，就工具不能自动执行第三方信任逻辑的情况，提出了简单的可信第三方参与的扩展逻辑，为复杂安全协议的可视化分析和设计提供参考。     

安全协议20年研究进展

总结了安全协议的20年研究进展情况，指出形式化方法在安全协议的设计与分析中的重要应用．对安全协议的若干热点研究方向进行了归纳和展望．     

一个安全协议形式化分析工具的研究

介绍了安全协议形式化分析方法,给出了一个自动化分析集成工具。该工具基于模态逻辑实现自动推理,采用可视化框架描述协议体。重点分析了该软件的模块结构和工作原理,可为形式化分析工具的设计和开发提供参考。     

安全协议形式化混合分析技术的研究与应用

分析了模型检测技术和逻辑推证技术的优点与不足，介绍了两种形式化分析方法相结合的混合分析方法，并给出实例，证明混合分析技术在检测协议漏洞方面是更为完全的。该技术的效率大大高于一些起初的模型，且易于实现。     

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

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

不可否认协议时限性的形式化分析

虽然SVO逻辑由于其简单性在对不可否认协议的形式化分析中得到了广泛的应用,但它在时间描述能力上的不足使得它无法分析不可否认协议的时限性.通过向SVO逻辑添加一种简单的时间表达和分析方法扩展了SVO逻辑,并使用扩展后的逻辑对Zhou和Gollmann于1996年提出的一个公平不可否认协议及其一个改进协议进行了分析.分析结果表明,原协议不具有时限性,而改进协议具有时限性,因此也说明了扩展后的新逻辑能够分析不可否认协议的时限性.另外,新逻辑还能用来分析一般密码协议中的时间相关性质.     

安全协议形式化分析的研究现状及有关问题

本文主要概述了安全协议形式化分析的研究状况,分析了现有安全协议形式化分析工具所面临的挑战和问题.     

安全协议的关联性研究

关联性是安全协议的基本特征,该文提出了协议相关性的分析方法,从主体认证关联、消息间关联、消息内部关联 3个角度分析了协议的相关特征,阐述了相关性的概念和关联规则构建方法,构建了基于关联性的协议描述模型,为安全协议的形式化分析提供了新的思路。     

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

介绍了安全协议的形式化分析思路,阐述了安全协议形式化描述、需求、验证及设计四个方面的研究状况和它们的基本原理,并对常用的几种形式化验证技术的优缺点进行了分析,最后针对形式化技术在该领域的发展前景提出了自己的见解。     

基于结构化操作语义的安全协议分析框架研究

操作语义模型是一种用来分析安全协议的新模型,它以操作语义学为基础,结合了多种协议分析模型的优点,能直接分析多个协议的组合问题.本文在对安全协议操作语义模型进行研究的基础上,构建了一个基于结构化操作语义的安全协议分析框架,给出了该框架中的协议规格,协议运行,威胁模型和安全性质等形式化定义.最后,以经典的Needham Schroeder Lowe 协议为例,用该分析框架分析了其机密性和认证性.     

一种适用于嵌套加密协议分析的强认证测试方法

认证测试是一种新型的在串空间模型基础上提出来的用于分析协议认证属性的形式化方法,该方法因简单实用而受到学者的广泛关注,但其不能分析协议中认证测试组件嵌套加密的情况,这极大地限制了它的应用范围.而现存的针对该局限性的改进方案,由于没有从本质上对串空间模型中关于消息项结构关系方面的语义进行完善,很难彻底突破认证测试的局限性.为此,通过在串空间模型中引入等价类、类组件、安全加密元及安全包裹元等概念,提高了串空间刻画消息项之间及内部结构关系的能力,并结合实例来阐明引入这些概念的必要性.在此基础上,提出一种可以分析测试组件嵌套加密的通用的认证测试方法,并从形式化证明与实例分析两方面验证了新测试方法的正确性与有效性.     

一种基于语义的安全协议形式化模型

在分析实际网络环境中安全协议的运行特点之后,提出了安全协议建模分析的两点基本假设.在此基础上,提出了一种基于语义的安全协议形式化模型,具体包括基于角色事件的协议静态描述模型和基于运行状态的协议动态执行模型,给出了模型的基本语法及形式语义,明确了模型推理过程中涉及到的一些关键性概念,并以简化的NSL协议为例进行了说明,为实现自动化验证打下了必要的基础.     

一种新型的安全协议分析逻辑

提出了一种新的形式化分析逻辑 ,可用于分析协议的安全性 .它有 3个优点 :(1)能分析协议的可追究性 ,(2 )能分析协议的公平性 ,(3)能有效的分析协议能否抵御重放攻击 ,(4 )增加了密文理解规则 ,能够有效地分析包含有签过名的加密公式的消息     

一种分析密码协议的新逻辑

提出了一种分析密码协议的新逻辑。针对信息安全的需要,给出了一套与加解密、签名等密码学操作有关的构造和推理规则,举例说明此逻辑在分析密码协议中的应用,并讨论了需要进一步研究的问题。     

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

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

乐观公平交换协议的可追究性分析

可追究性是安全电子商务协议必须遵循的重要原则之一,乐观公平交换协议是一类重要的电子商务协议。目前没有针对乐观公平交换协议的可追究性进行形式化分析的具体方法。文章提出了一种分析乐观公平交换协议可追究性的形式化方法,该方法不再单独定义非否认证据,只是研究协议的目标设计是否能提供实现可追究性的证据,将可追究性证明与公平性等其它安全性质的证明分开讨论,这样不论协议是否满足其它安全性质,都可以讨论协议是否满足可追究性。     

ENDL: A Logical Framework for Verifying Secure Transaction Protocols

This paper proposes a new logic for verifying secure transaction protocols. We have named this logic the ENDL (extension of non-monotonic dynamic logic). In this logic, timestamps and signed certificates are used for protecting against replays of old keys or the substitution of bogus keys. The logic is useful for verifying the authentication properties of secure protocols, and especially for protecting data integrity. To evaluate the logic, three practical instances of secure protocols are illustrated. This evaluation demonstrates that the ENDL is effective and promising.     

改进的电子商务协议逻辑分析方法

在卿-周逻辑(软件学报,2001年第9期)的基础上提出一种改进的逻辑分析方法,用于分析电子商务协议的安全性,如可追究性、公平性和原子性。该方法通过引入消息新鲜性机制,使被重放的消息可以被识别,重新定义可追究性的实现条件,使得在发生重放攻击时能正确分析各方的责任性,给出原子性目标并增加对原子性分析的方法,以实现对协议原子性的分析。     

移动自组网安全路由协议性能分析

安全路由协议设计是移动自组网所面临的重大课题之一.针对移动自组网中3种典型的安全路由协议(ARAN,Ariadne,SEAD)进行了深入研究,对其性能与特点进行了细致的比较与分析.同时,在网络模拟器ns2中实现了上述协议并进行了性能测试.实验结果显示:尽管上述安全路由协议能在一定程度上提高安全性,但其性能及额外开销随网络拓扑的动态变化也急剧变化.模拟分析结果对移动自组网中安全路由协议的设计与分析有着较好的指导意义,为相关设计打下了良好的基础.