基于BAN逻辑的ad hoc移动网络路由协议的安全性分析

Ad hoe移动网络路由协议为加强其安全性，采用了密码技术，使其成为安全协议的一种。这使得采用形式化的方法分析其安全性成为可能。考虑ad hoe移动网络路由协议的特点，采用BAN逻辑对协议的安全性进行描述，提出了协议应满足的条件。并对协议的运行过程进行了形式化，给出具体的分析方法。采用该方法对安全路由协议SADSR进行了安全验证，说明方法的有效性。     

NSPK协议的Spin模型检测

NSPK协议是一个经典的认证密码协议.通过建立该协议的Promela模型,采用线性时序逻辑描述模型性质,并用模型检测工具Spin进行验证,进而生成入侵者的攻击序列.     

密码协议主体角色进程表示

密码协议分析与设计的基础是对其进行形式化建模。将主体角色发送和接收消息的行为分别表示为相应的主体角色发送进程和接收进程,定义前缀(串行)和并发运算为主体角色进程演进的算子,并进一步将主体角色进程演进的状态系统描述为密码协议的串空间图。它为密码协议安全属性的验证提供了一个形式化模型。     

密码协议的一种基于组合推理的模型验证

将密码协议与协议中用到的密码算法视为一个系统，基于组合推理技术建立了密码协议系统的形式化模型。采用基于假设／保证的组合推理技术提出了新的假设／保证推理规则和假设／保证推理算法，证明了该规则的正确性，实现了密码协议系统的模型验证，并重点解决了系统分解问题、假设函数的设定问题等难题。以kerberos v5密码协议系统为例，利用该组合推理技术对密码协议系统进行了安全验证。     

网络支付协议的形式化安全需求及验证逻辑

从整个网络支付协议的安全角度出发，提出网络支付协议的多层安全需求模型，包括以认证和密钥分配为基础的基层需求、网络支付协议固有的中层需求(包括保密性、原子性、公平性、完整性、匿名性、不可否认性、可追究性等)、以及面向具体应用的高层需求。基于一阶逻辑和时序逻辑，提出一种适合描述网络支付协议的形式化安全需求的逻辑，描述了该逻辑的语法结构和推理规则，并用该安全需求逻辑对网络支付协议的多层安全需求进行了形式化描述。最后，以SET协议为例进行需求验证。     

WTLS握手协议的形式化验证

目前还未见到公开发表的对WTLS握手协议进行形式化分析的研究成果。本文首次使用密码协议分析工具集AVISPA,从机密性和鉴别两个方面,对WTLS握手协议进行了建模和验证。所得到的验证结果表明WTLS握手协议是安全的。     

运行模式法分析密码协议实例研究

在介绍两方密码协议运行模式分析法的基础上，运用运行模式分析法对自行设计的TW两方密码协议进行了分析，成功地发现了TW协议的攻击，并验证了此协议的安全性，说明了两方密码协议运行模式分析法的有效性。     

基于时序逻辑的仿真系统行为验证方法

仿真系统行为可信性评估是一项复杂的任务，需要综合利用多种方法、从多个角度对仿真系统的行为进行验证。针对仿真系统行为验证既需要具有客观性又需要考虑领域专家宝贵经验的需求，借鉴形式化验证技术的思想，提出基于时序逻辑的仿真系统行为验证方法。该方法首先根据真实系统和实测数据，结合专家经验，对所关注的仿真系统行为属性进行提取；其次，利用时序逻辑语言对提取的待验证属性进行形式化描述；然后，运行仿真系统并获得相应的输出数据，利用验证算法自动检验仿真数据是否满足给定的属性，从而实现行为验证；基于对武器装备体系对抗仿真领域的验证属性分析，选取度量区间时序逻辑作为属性的形式化描述语言；最后，通过一个防空对抗仿真系统的验证示例，表明了该方法的有效性。     

容忍入侵的密码协议自适应调整策略研究

在密码协议的实际运行中,为保护密码协议安全运行,针对密码协议上攻击产生的原因,文中设计了两种能容忍入侵的密码协议自适应调整策略:算法自适应调整策略和参数自适应调整策略,能根据攻击的类型,动态调节密码协议的运行,以容忍/阻止一部分攻击行为,更好的保护密码协议的运行安全,并对两种策略的原理进行了详细的介绍,对它们的性能进行了仿真实验与分析,验证了这些策略的有效性.     

基于形式化方法的安全协议安全性分析

协议安全是确保网络数据安全的基础。传统的基于观察的人工分析协议安全性分析已不能满足安全需求。如何研究安全协议及安全属性的性质,使两者在统一框架下实现可分析和验证是亟待解决的问题,形式化分析为解决这一问题提供了精确的数学手段和强大的分析工具。对已有的安全协议形式化分析方法进行了归纳和总结,并从等价验证、协议优化和增强分析准确度三方面提出了未来的研究设想。     

面向密码协议在线安全性的监测方法

为解决现有方法无法在线监测协议逻辑进行的低交互型攻击的问题,提出一种密码协议在线监测方法CPOMA。首先构建面向密码协议的特征项本体框架,以统一描述不同类型的特征项,并基于该框架首次利用模糊子空间聚类方法进行特征加权,建立个体化的密码协议特征库;在此基础上给出自学习的密码协议识别与会话实例重构方法,进而在线监测协议异常会话。实验结果表明,CPOMA不仅能够较好地识别已知协议、学习未知协议、重构会话,而且能够有效在线监测协议异常会话,提高密码协议在线运行的安全性。     

基于串空间模型的改进型 Otway-Rees 协议分析

串空间模型是一种新兴的密码协议形式化分析工具,其理论中理想和诚实概念的提出大大减少了协议的证明步骤.本文在 Otway-Rees 协议缺陷的基础上对它进行改进,并利用串空间模型的理论对改进后的 Otway-Rees 协议进行了形式化的分析.新的 Otway-Rees 协议满足其安全目标,是安全可行的     

Anonymous and secure electronic transaction protocol

We present a new protocol for electronic transactions which is not only secure but also anonymous, the latter characteristic being obtained by associating an encryption device with a chip card. Security is ensured by the use of encryption, electronic signature and authentication. In order to check the validity of the security properties enforced by the protocol, a model and a specification are provided. The protocol modeling language is a process algebra with value passing extended by an observation mechanism allowing the specification of security levels, by cryptographic primitives, and by a function call feature on private channels allowing the modeling of interactions with the crypto-system. The anonymity is expressed by an information flow property. The verification method, based on cosimulation, is proved consistent and complete and analysis confirms that this approach ensures not only anonymity (thanks to the fact that the client never discloses to the merchant any information permitting his identification), but also the quasi-impossibility of any fraudulent transaction.     

以DNA为载体的线性时序逻辑模型检测

线性时序逻辑模型检测被广泛应用于处理器设计与验证、网络协议验证、安全协议验证等领域.然而到目前为止,该技术只能在电子计算的平台上实现.为了以脱氧核糖核酸(Deoxyribo Nucleic Acid,DNA)为载体对线性时序逻辑(Linear Temporal Logic,LTL)实施模型检测,给出了使用粘贴自动机实现Until算子模型检测的方法.首先,使用粘贴自动机对Until公式的有穷状态自动机(Finite State Automata,FSA)模型进行编码;然后,将系统模型转换为粘贴自动机的输入字符串;最后,用粘贴自动机验证系统是否满足公式.仿真实验结果证实,新方法可实现对LTL逻辑时序算子的检测.     

Three systems for cryptographic protocol analysis

Three experimental methods have been developed to help apply formal methods to the security verification of cryptographic protocols of the sort used for key distribution and authentication. Two of these methods are based on Prolog programs, and one is based on a general-purpose specification and verification system. All three combine algebraic with state-transition approaches. For purposes of comparison, they were used to analyze the same example protocol with a known flaw.     

一种用于密码协议形式化验证的简单逻辑

给出了一个可用于密码协议形式化验证与设计的简单逻辑.该逻辑采用抽象的通道概念表示具有多种安全特性的通信链路,可在比现有认证逻辑的更抽象的层次上对协议进行处理.