对安全协议重放攻击的分类研究

在详细研究攻击实例的基础上,从攻击成功的根本原因出发,提出了一种新的重放攻击分类方法.该分类方法能够更清楚地认识到重放攻击的原理和本质,并针对不同的重放种类给出了避免攻击的原则性方法,对协议的设计和分析起到了借鉴作用.     

安全协议形式化分析方法综述之二——基于攻击结构性方法

本文给出了现行的基于攻击结构性方法的分类,分析了各类工具的特点。     

认证协议攻击与非形式化分析

协议的分析验证方法有形式化与非形式化之分．很多代表性的协议虽然存在着缺陷，但对这些协议的非形式化分析，却可以提出一些值得借鉴的规则，参考这些规则可以避免和减少协议逻辑的漏洞，本文针对Woo-Lam两个改进协议以及SSL协议给出了攻击方法，分析协议存在的漏洞并提出如何使协议更为安全的建议。     

改进的安全协议逻辑系统及评估技术

改进了Blanchet安全协议一阶逻辑系统并建立了用于评估攻击者攻击耗费的攻击树模型,明确了系统和模型中涉及的一些关键性概念和命题.改进的系统能够将逻辑推导转换成易于理解的攻击过程.建立的攻击树模型具有以下特点:能够形象直观地描述攻击者对一个协议进行攻击的行为;能够对不同方法所耗费的资源进行相对比较;基于树状结构,便于计算机实现搜索、存储.     

分析安全协议猜测攻击的模态逻辑方法

以CKT5逻辑为基础,对其进行了多方面重要的扩展;在原有对称密钥机制的基础上,增加了公开密钥机制和vernam加密机制以增强其描述协议的能力;打破完善加密假设,给出了一组定义和规则使主体具备猜测和验证口令的能力;给出了与在线猜测攻击相关的定理以反映在线猜测攻击的特点;通过相关引理和定理的证明,简化了猜测攻击的分析过程,使该文方法比现有方法更加简洁高效.扩展后的逻辑能够用于分析安全协议的猜测攻击,包括在线猜测攻击.     

DDoS攻击分类与效能评估方法研究

DDoS攻击是一类常见而又难以防范的网络攻击模式，对Internet网络系统的正常运行构成了巨大威胁。DDoS攻击的分类方法和攻击效能评估是计算机网络攻防对抗研究的一项重要而紧迫的任务。本文介绍了DDoS攻击的原理、方法、一般概念和主要目标，研究了基于攻击代理的传播模式、通讯方式、作用机制等特征的DDoS攻击分类方法体系，分析了DDoS攻击的攻击效能评价指标体系。在分析了DDoS攻击效能评估的特点的基础上提出了DDoS攻击效能评估的模糊评价评估模型。     

安全协议攻击序列重构技术

攻击者攻击序列在安全协议形式化分析技术中用于描述攻击者对安全漏洞的攻击步骤.目前,攻击序列重构技术是安全协议形式化分析研究的热点与难点.对国际流行的方法进行了介绍和总结,重点分析和比较了基于模型检测的方法、基于定理证明的方法、基于逻辑程序的方法等能够进行攻击序列重构的各种方法,指出了各自的优缺点及技术手段、技术特点,最后给出了该领域的进一步研究方向.     

安全协议的设计规范及安全性分析

网络安全的根本在于保护网络中的信息免受各种攻击,安全协议是网络安全的一个重要方面。要确 保这些协议的安全运行,安全协议的设计及安全性分析就显得尤为重要。     

安全协议类型漏洞攻击研究

类型漏洞攻击是对安全协议攻击的方法之一。当协议主体将所接收消息中的一种类型数据解释成其他类型数据时,就会发生类型漏洞攻击。该文描述了几种典型的类型漏洞攻击实例,结合实例指出了J.Heather等人提出的在消息中添加标识消息类型的附加信息以防止类型漏洞攻击的tag方法的局限性,并提出在协议实现中通过检测消息长度防止类型漏洞攻击的方法。     

一种安全协议的安全性分析及攻击研究

针对Web安全协议SSL的握手协议部分进行了详尽的阐述，对其安全性作了一定的分析，给出了理论上存在的三个协议漏洞的详尽描述，并且经过测试验证，指出了SSL协议存在***模式漏洞。     

安全协议的串空间图表示

串空间是安全协议的一种形式化描述，串空间图是它的图示化表示．定义开丛为串空间图的构造单元，并在开丛集上定义前缀算子和组合算子．通过开丛之间的前缀和组合运算，给出了无穷并发运行安全协议串空间图的生成方法．定义了开丛互模拟以及串空间图之间的互模拟等价关系，并给出用于消除串空间图冗余结构的化简规则＋案例分析和与相关工作的比较表明，无冗余的串空间图为无穷并发运行安全协议的安全属性验证提供了一个有效的分析模型．     

A Method for Patching Interleaving-Replay Attacks in Faulty Security Protocols

The verification of security protocols has attracted a lot of interest in the formal methods community, yielding two main verification approaches: i) state exploration, e.g. FDR [Gavin Lowe. Breaking and fixing the needham-schroeder public-key protocol using FDR. In TACAs'96: Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, pages 147–166, London, UK, 1996. Springer-Verlag] and OFMC [A.D. Basin, S. Mödersheim, and L. Viganò. An on-the-fly model-checker for security protocol analysis. In D. Gollmann and E. Snekkenes, editors, ESORICS'03: 8th European Symposium on Research in Computer Security, number 2808 in Lecture Notes in Computer Science, pages 253–270, Gjøvik, Norway, 2003. Springer-Verlag]; and ii) theorem proving, e.g. the Isabelle inductive method [Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal in Computer Security, 6(1-2):85–128, 1998] and Coral [G. Steel, A. Bundy, and M. Maidl. Attacking the asokan-ginzboorg protocol for key distribution in an ad-hoc bluetooth network using coral. In H. König, M. Heiner, and A. Wolisz, editors, IFIP TC6 /WG 6.1: Proceedings of 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems, volume 2767, pages 1–10, Berlin, Germany, 2003. FORTE 2003 (work in progress papers)]. Complementing formal methods, Abadi and Needham's principles aim to guide the design of security protocols in order to make them simple and, hopefully, correct [M. Abadi and R. Needham. Prudent engineering practice for cryptographic protocols. IEEE Transactions on Software Engineering, 22(1):6–15, 1996]. We are interested in a problem related to verification but far less explored: the correction of faulty security protocols. Experience has shown that the analysis of counterexamples or failed proof attempts often holds the key to the completion of proofs and for the correction of a faulty model. In this paper, we introduce a method for patching faulty security protocols that are susceptible to an interleaving-replay attack. Our method makes use of Abadi and Needham's principles for the prudent engineering practice for cryptographic protocols in order to guide the location of the fault in a protocol as well as the proposition of candidate patches. We have run a test on our method with encouraging results. The test set includes 21 faulty security protocols borrowed from the Clark-Jacob library [J. Clark and J. Jacob. A survey of authentication protocol literature: Version 1.0. Technical report, Department of Computer Science, University of York, November 1997. A complete specification of the Clark-Jacob library in CAPSL is available at http://www.cs.sri.com/millen/capsl/].     

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

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

“舒特”攻击行动描述与效能评估探要

文章基于UML概念建模语言对“舒特”攻击行动进行了形式化描述,构建了“舒特”攻击行动效能评估指标体系,运用模糊层次分析法对“舒特”攻击行动的效能进行了评估,同时给出了应对“舒特”攻击的建议。     

安全协议20年研究进展

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

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

形式化方法能有效检验安全协议的安全性,BAN类逻辑的发展极大地促进了这一领域的研究,但是现有的BAN类逻辑仍然存在许多问题．在分析现有BAN类逻辑的基础上,提出一种新的安全协议形式化验证方法,实现现有BAN类逻辑的验证功能,并使安全协议验证工作简单可行,便于实现机器自动验证．为安全协议形式化验证提供了一种新的途径．     

Decision Procedures for the Security of Protocols with Probabilistic Encryption against Offline Dictionary Attacks

We consider the problem of formal automatic verification of cryptographic protocols when some data, like poorly chosen passwords, can be guessed by dictionary attacks. First, we define a theory of these attacks and propose an inference system modeling the deduction capabilities of an intruder. This system extends a set of well-studied deduction rules for symmetric and public key encryption, often called Dolev–Yao rules, with the introduction of a probabilistic encryption operator and guessing abilities for the intruder. Then, we show that the intruder deduction problem in this extended model is decidable in PTIME. The proof is based on a locality lemma for our inference system. This first result yields to an NP decision procedure for the protocol insecurity problem in the presence of a passive intruder. In the active case, the same problem is proved to be NP-complete: we give a procedure for simultaneously solving symbolic constraints with variables that represent intruder deductions. We illustrate the procedure with examples of published protocols and compare our model to other recent formal definitions of dictionary attacks.     

交叉树:一种用于安全协议分析的数据结构

提出用一种特殊的数据结构交叉树来描述安全协议中的消息。交叉树有一些交叉结点，拥有交叉结点的几棵交叉树形成交叉森林。一棵交叉树唯一对应于一个消息，一个交叉森林表示那些在协议执行过程中采用相同机制发送或接收的消息。一个或几个消息中相同的原子消息在交叉树或交叉森林中用交叉结点来表示，这样易于保证原子消息的一致性，以及公钥和它所有者之间的一致性。另外，交叉树还可用于为消息模板建立可接受消息，这时于建立在模型检验基础上的安全协议分析是非常必要的。