Andrew Secure RPG协议的一种组合分析方谢

逻辑方法和模型检验方法是安全协议的两种重要分析方法。逻辑方法简单、直观，但其最大问题是不够完备，模型检验方法自动化程度高且能生成不满足所需求性质的反例。先用BAN逻辑对Andrew Secure RPC协议进行分析，并在此基础上组合模型检验方法进行分析，结果表明逻辑方法组合模型检验方法分析协议比只用逻辑方法分析得到的结果更全面且更具体。     

3-D Secure协议的安全分析

电子商务是当今社会发展的方向。本文着重对当前最新的电子商务协议3-D Secure进行安全分析,通过与其他安全协议的分析、对比得出当前3-D Secure协议的优势和面临的安全问题,并对安全问题提出加强方案。     

一种安全协议的形式化验证方法

BAN(Burrows,Abadi and Needham)类逻辑可以辅助设计、分析和验证网络和分布式系统中的安全协议。介绍BAN逻辑的产生、成分和分析步骤，指出BAN逻辑的缺陷，由此而产生的改进BAN逻辑和现状，并对BAN类逻辑作全面的回顾与展望，得出：BAN类逻辑仍然是密码协议分析和设计的主要工具，但理想化步骤是BAN类逻辑的致命缺陷的结论。展望了BAN类逻辑研究。对未来协议的形式化分析工作具有指导意义。     

一种基于协议组合的协议动态实现模型

在协议组合理论的基础上提出了一种可以动态扩展协议句法的基本协议实现模型,依据现有协议特征中的句法结构,将协议句法结构划分为4个不同的种类,针对这4种不同类型的协议句法结构具体提出了4种不同的可动态扩展的协议句法实现模型.基于该模型实现的协议软件在句法结构上具有灵活可扩展的特性.当该协议扩展句法结构时候,即使相应协议软件处于执行状态,也可以不中止协议软件的运行而完成句法结构的扩展.最后以SIP协议为例,使用VOCAL源码详细说明了如何在该模型的基础上实现协议句法动态扩展.     

一种安全协议的逻辑分析与改进

采用BAN逻辑对著名的Needham—Schroeder(NS)协议建立理想化协议模型,利用协议的初始假设和BAN逻辑的公设分析NS协议的安全性．分析结果表明,该协议只有增加初试假设,即用户B获得的会话密钥是新的会话密钥的前提下才能达到认证的目标,并提出改进方案．     

基于PCL的改进型Helsinki协议的形式化分析

针对改进型的Helsinki协议安全性问题,利用协议组合逻辑PCL对协议进行形式化分析.首先使用基于"Cords演算"的程序描述语言对协议本身进行形式化描述,然后通过协议逻辑描述协议的安全属性,最后给出性质和定理,并通过逻辑推理证明改进型Helsinki协议满足其安全要求,该协议是安全的.     

一种基于状态融合的协议状态机推断方法

针对现有协议状态机推断方法忽视协议系统输入输出报文之间的内在关系,导致自动化程度较低等问题,提出一种基于状态融合的协议状态机推断方法。首先采集会话样本,将会话过程的输入输出报文序列抽象为符号序列;然后采用扩展前缀树转换器(EPTT)构建初始状态机,通过各状态对相同输入符号序列的状态转换和输出响应评判其相似度,依据相似度的高低搜寻候选状态对并尝试对其融合,同时有针对性地构造测试用例以验证此次融合的正确性。上述流程反复执行,直到没有可融合的状态。结果表明,该方法自动化程度较高,推断出的结果与真实协议状态机高度吻合。     

一种基于模型检验的类测试用例生成方法

提出一种新的自动生成类测试用例的方法.使用符号执行从类源代码抽取对象的状态和行为,以一个四元组抽象描述类,并转化成等价的Kripke结构.使用CTL公式描述测试覆盖标准,然后把这组CTL公式和描述类状态行为的Kripke结构输入模型检验工具,并利用模型检验工具自动生成相应的证据路径,最后将路径转化成满足相应覆盖标准的类测试用例.该方法直接从源代码生成测试用例,并使用贪心法约减冗余用例以降低测试成本.实验表明该方法生成的测试用例具有较高的覆盖率.     

一种互认证密码协议的设计和分析

为在不安全的网络中建立安全的通信，提出了一种用于网络管理互认证的具有较高效率的密码协议，介绍了该密码协议的相关设计背景。总结了若干关于密码协议设计的原则，通过运用经过补充的BAN逻辑对该协议进行形式化分析，并通过计算机对该协议的握手协议过程进行仿真。仿真结果表明，在被加密协议参数相同的条件下，该协议减少了系统开销，提高了协议效率。     

一种新的安全协议设计方法

已有的安全协议往往被证实并不如它们的设计者所期望的那样安全,如何设计才能确保协议的安全性是目前研究的难点之一.通过介绍目前安全协议设计的主要思路和方法,说明了PDS系统的主要内容和方法,推导出了ISO-9798-3协议.     

基于组合设计方法的安全支付协议的设计与验证

针对银行、商家和客户对电子支付协议提出的11条安全需求,应用组合设计方法设计一个新的安全支付协议,并用SMV工具分析新协议的原子性.新协议满足指定的安全需求和电子商务协议的原子性要求,实现了电子商品和实物商品在线支付的设计目标,适用于多个客户和商家对同时进行交易.     

一种理性安全协议形式化分析方法及应用

博弈逻辑ATL和ATEL可以对传统安全协议的公平性、安全性等性质进行分析与验证.不过在理性环境下,由于参与者对知识的自利性,ATL和ATEL都不适合形式化分析与验证理性安全协议.于是在并行认知博弈结构CEGS中引入效用函数和偏好关系,得到新的并行认知博弈结构rCEGS,并在合作模态算子《Γ》中引入行为ACT参数,提出新的交替时序认知逻辑rA-TEL-A,并基于不动点描述rATEL-A时序算子.然后基于rATEL-A,提出适合于形式化分析理性安全协议的推理系统,并对具体的理性安全协议的公平性、安全性等性质进行形式化分析.     

基于SPIN的SAS协议和NS公钥协议分析

给出SPIN模型检测协议的验证步骤,使用其分析验证SAS协议的安全属性和数据流行为属性,以及NS公钥协议的机密性和认证性.结果成功发现SAS协议数据流的缺陷和NS公钥协议的攻击路径.     

通信协议分析的一种新方法

本文提出一种用于协议分析的新方法,它以本文提出的带有参数计数器的有限状态自动机为基础,对协议模型进行可达性分析。这种方法不仅解决了“状态爆炸问题”,并有利于实现自动验证。由所生成的可达树,可以构成马尔可夫链模型,并由此确定协议的性能。文中讨论了马尔可夫链模型的性质与建立过程,并进行了吸收分析。最后,给出了简单分组传输协议的例子,以说明方法的应用。     

一个基于模态逻辑的安全协议度量方法

为将量化分析方法引入安全协议分析中,以模态逻辑方法为基础定义了协议度量方法,并形式化地给出度量协议内容对协议安全目标满足度的参数和方法,同时在此基础上,进一步地给出了对安全协议冗余进行度量及化简的方法。应用该方法对实例协议进行分析,直接描述各协议内容的贡献度,显示冗余内容对目标实现的无效作用,从而可以安全化简。量化分析在安全协议形式化分析中的应用是本方法的主要特点,它具有模态逻辑方法的优点及缺陷。     

面向变异分析的协议安全测试方法

在基于构造类别代数的协议描述上引入变异分析方法,由此提出了一种基于错误模型的协议安全测试方法.通过设计针对构造类别代数的变异算子,限制了协议中的错误集合;应用变异算子生成变异体集合,并消除其中的等价变异体;基于变异体构造安全测试例.同比研究表明,采用基于错误模型的变异分析方法,可以有效解决协议安全测试中忽视协议数据流处理过程、错误集合无限和缺少结果判断机制等问题,限定协议可能存在的错误集合,有利于测试的量化和评估,能够更有针对性地进行测试例构造和测试结果判断,提高测试能力.     

组合逻辑电路的设计简化

把EPROM引用到逻辑电路中,将会简化逻辑电路及其设计步骤.     

RPC漏洞分析

介绍了微软操作系统的RPC漏洞,并对RPC溢出漏洞进行分析。     

A Secure and Pragmatic Routing Protocol for Mobile Ad hoc Networks

An ad hoc network is a group of wireless mobile computers （or nodes）, in which individual nodes cooperate by forwarding packets for each other to allow nodes to communicate beyond direct wireless transmission range. Because of node mobility and power limitations, the network topology changes frequently. Routing protocol plays an important role in the ad hoc network. A recent trend in ad hoc network routing is the reactive on-demand philosophy where routes are established only when required. As an optimization for the current Dynamic Source Routing Protocol, a secure and pragmatic routes selection scheme based on Reputation Systems was proposed. We design the Secure and Pragmatic Routing protocol and implement simulation models using GloMoSim. Simulation results show that the Secure and Pragmatic Routing protocol provides better experimental results on packet delivery ratio, power consumption and system throughput than Dynamic Source Routing Protocol.