改进的安全协议一阶逻辑模型

由于Blanchet安全协议一阶逻辑模型不能够给出易于理解的攻击序列,基于该安全协议一阶逻辑模型,对逻辑推理中的规则及合一化操作进行了分类,给出了操作置换规则,明确了改进系统中的一些关键性概念和命题。最后,以化简的Needham-Schroeder协议为例,对秘密性进行形式化验证,结果表明改进的系统能够给出易于理解的攻击序列。     

基于同态的安全协议攻击及其形式化验证

介绍2种利用加密算法同态特性的安全协议攻击,定义安全协议项代数表示和基于角色行为序列的协议模型,提出一种基于角色行为实例交互的安全协议约束序列生成方法,应用等式理论将Dolev D等人提出的Dolev-Yao模型（IEEE Transactions on Information Theory,1983,第12期）进行扩展,设计攻击者一阶逻辑演绎系统,采用约束求解方法对NSL协议进行建模和形式化验证,发现基于“完美密码系统假设”无法验证的同态攻击。     

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

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

一种基于攻击序列求解的安全协议验证新算法

基于完美加密机制前提及D-Y攻击者模型,指出注入攻击是协议攻击者实现攻击目标的必要手段.分析了注入攻击及其形成的攻击序列的性质,并基于此提出了搜索攻击序列的算法,基于该算法实现了对安全协议的验证.提出和证明了该方法对于规则安全协议的搜索是可终止的,并通过实验实现了NS公钥协议的验证.实验结果表明,与OFMC等同类安全协议验证工具相比,该算法不仅能实现安全协议验证自动化,而且由于规则安全协议验证的可终止性,使得本算法更具实用性.     

基于Horn逻辑扩展模型的时间敏感安全协议验证

分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法,针对它们在验证时间敏感安全协议时的不足,提出了带时间约束的安全协议的Horn逻辑扩展模型和修改版本的安全协议验证方法,并给出了相应的定义和定理,使得带时间约束的安全协议的Horn逻辑扩展模型和修改版本的安全协议验证能够分析依赖时间的安全协议的安全性质.通过在验证中加入时间约束条件,得到了大嘴青蛙协议的攻击序列,并可从约束条件中导出避免攻击的条件.     

注入攻击序列搜索算法对安全协议的验证研究

通过对D-Y攻击者模型研究,可知注入攻击是攻击者实现其攻击目标的必要手段。对注入攻击序列的性质进行分析,提出了一种在安全协议会话状态空间中搜索注入攻击序列的算法,基于该算法可实现一种新的安全协议验证方法。利用该方法实现了NS公钥协议的验证。实验表明该方法可以实现对安全协议的自动化验证,降低了验证的复杂度,并能给出安全协议漏洞的具体攻击方法。     

一种基于进程代数的安全协议验证消解算法

安全协议本质上是分布式并发程序,可以描述为多个子进程的并发合成系统.将安全协议对应的并发合成系统抽象为一组逻辑规则,能够对安全协议无穷会话的交叠运行进行验证.本文首先给出了将安全协议基于进程代数的形式描述转化成为一组逻辑规则的方法,并提出了基于逻辑规则分类的高效逻辑程序消解算法,对安全协议认证性和保密性进行验证.     

一种基于ECB模式的NSL协议改进方案

安全协议形式化方法大都在一个很高的抽象层次建立协议模型。但是协议的许多安全问题是在很低的抽象层次产生。本文分析了ECB工作模式下的NSL协议的安全问题,并通过破坏同态性的方法给出一种改进方案。通过扩展规则的BAN逻辑对NSL协议建模和分析,验证结果表明协议中存在着安全漏洞,新的改进方案可以避免这种攻击。     

一种基于规划理论的密码协议形式模型

将规划理论引入到密码协议形式化分析领域,结合密码协议在实际网络环境中的运行特点和规律,提出了密码协议攻击规划理论;建立了一种对密码协议进行安全性验证的形式化模型,即密码协议攻击规划问题模型;给出了模型的一阶语法、形式定义及相关运算语义.同时,分析了Dolev-Yao模型的不足之处,基于基本消息元素策略对其进行了改进;并通过增强应用语义来保证改进模型的可行性,从而避免了"状态空间爆炸"问题的发生,提高了密码协议攻击规划问题模型的完备性;并给出了基于该模型的NS公钥协议分析实例.提出的密码协议形式模型是证伪的,目的在于对密码协议进行验证,并查找协议中可能存在的漏洞,既可以方便地进行手工推导证明,也非常易于自动化实现.     

动态远程证明协议及其形式化分析

针对程序的运行时动态攻击给远程证明带来的安全威胁,设计一种动态远程证明协议DRAP,对内存中处于运行状态的程序实施实时的动态度量,并向远程验证方证明平台实时状态。针对DRAP协议所用的TPM功能对LS2逻辑进行扩展,引入重置规则、时刻规则等新的推理规则,利用扩展的LS2逻辑对DRAP协议进行分析,分析表明DRAP中可重置配置寄存器中的扩展序列能够反映平台中程序的实时运行状态,并且在TPM可信和证明代理可信的前提下,远程验证者能够有效验证平台的实时可信状态。     

基于T-G保护系统的抗病毒网络安全分析模型

攻击者采用病毒、利用脆弱性等方式进行网络攻击,实质是其攻击权限不断扩大,进而导致系统状态变化的过程,针对这一特性,本文对原有的T--G模型和dejure重写规则进行了扩充,增加了攻击图中节点之间权限、连接关系、节点属性的描述和脆弱性重写规则,形成了DTGSA模型;通过对真实的漏洞进行建模和实验,证明此模型对攻击特征有很好的描述能力,能帮助网络管理员预测可能的攻击,进而采取相应的安全措施。     

信任攻击建模方法

针对信任环境系统中存在的客观弱点和主观弱点,使用弱点利用规则和信任关系盗用规则来描述信任关系状态之间的转移过程,构建了信任攻击模型TAM。在该模型中,攻击者将客观弱点用于信任级别的提升,将主观弱点用于信任关系传递,将主、客观弱点的综合利用将导致信任关系的渗透与扩散,从而可导致攻击可达距离更大;提出了复杂度为多项式时间的TAM信任关系传递闭包生成算法,该算法可以给出当前弱点状态下的所有信任攻击路径。通过对真实弱点的建模,证明此模型可以对信任的安全性进行综合分析,生成信任攻击图、信任攻击路径等详细信息,展示攻击者和信任主体之间的交互过程,对攻击特征有更好的描述能力,帮助管理者预测所有可能的信任攻击,进而为相应的安全措施的制定提供依据。     

密码协议安全性证明系统解析器的设计与实现*

可证明安全性是密码协议安全性评估的重要依据,但手写安全性证明容易出错且正确性难以判定,利用计算机辅助构造游戏序列进而实现自动化证明是当前一种可行的方法。为此提出一种基于进程演算的密码协议形式化描述模型,定义了描述密码协议安全性证明中攻击游戏的语法规则,并借助工具LEX和YACC,设计出解析器程序,将密码协议及其安全性的形式化描述解析为自动化安全性证明系统的初始数据结构,并用实例来说明这种方法的可行性。     

基于面向对象信任攻击图的信任风险传播模型

针对信任环境系统中存在的信任攻击问题,设计基于面向对象的信任攻击图模型。利用Take规则、Grant规则和Pervade规则,描述信任主体对象属性弱点导致的信任级别的提升、信任关系的传递、渗透与扩散问题,使攻击可达距离更大。根据弱点利用规则和信任关系盗用规则,提出多项式时间复杂度信任关系传递闭包生成算法及基于信任关系传递闭包的信任风险传播算法。实验结果证明了该模型的正确性。     

基于改进Apriori的网络安全感知方法

针对网络安全态势评估过程中存在数据源单一、实时性不强、准确率不高的问题,提出一种基于改进关联规则算法(Apriori算法)的网络安全态势感知方法;通过对数据的分析,发现在网络中存在关于安全态势的关联规则;通过网络攻击影响熵值序列的分析,对关联规则进行分类为空间正常和异常空间,进而对关联规则进行聚类分析;根据聚类后的规则划分网络安全态势等级;将改进后的算法应用到网络安全态势感知当中,实验结果表明,该方法满足了网络安全危险预警和实时监控的要求;改进的算法用于安全态势感知是可行的、有效的。     

Discovery and prevention of attack episodes by frequent episodes mining and finite state machines

This paper proposes a framework that applies frequent episode rules, implemented by finite state machines (FSMs), to design a real-time network-based intrusion prevention system (NIPS) for Probe/Exploit (hacking) intrusion. This type of Probe/Exploit (hacking) intrusion is executed by a series of relevant actions that occur in some sequence. In frequent episode rules mining, data are viewed as a sequence of events, where each event has an associated time of occurrence; thus, such mining technique has significant effect on discovering sophisticated Probe/Exploit intrusion attacks. Prior to a devastating attack on a victim's computer, the hacker must gather information about the victim, and transfer instructions or files to the victim's computer. The proposed system could detect such abnormal episodes and repel hackers from the firewall before they are able to launch a deadly attack. In one network service (a corresponding port number), mine frequent episode rules from the log files of a commercial honeypot system, then refine the rules, which eventually constructs a finite state machine to protect the network service, according to the refined rules. During implementation and simulation, this study applied the framework focus on protecting a Server Message Block (SMB) protocol, which is the most important protocol in Microsoft's Windows Network. As confirmed in the experiments, this study successfully mined sophisticated intrusion episodes and demonstrated the efficiency of tracing connections by a FSM. The framework of intrusion prevention proposed in this paper can be modified straightforward to protect other network services.     

A decision support system for constructing an alert classification model

As the rapid growth of network attacking tools, patterns of network intrusion events change gradually. Although many researches had been proposed to analyze network intrusion behaviors in accordance with low-level network data, they still suffer a large mount of false alerts and result in difficulties for network administrators to discover useful information from these alerts. To reduce the load of administrators, by collecting and analyzing unknown attack sequences systematically, administrators can do the duty of fixing the root causes. Due to the different characteristics of each intrusion, none of analysis methods can correlate IDS alerts precisely and discover all kinds of real intrusion patterns. Therefore, an alert-based decision support system is proposed in this paper to construct an alert classification model for on-line network behavior monitoring. The architecture of decision support system consists of three phases: Alert Preprocessing Phase, Model Constructing Phase and Rule Refining Phase. The Alert Processing Phase is used to transform IDS alerts into alert transactions with specific data format as alert subsequences, where an alert sequence is a kind of well-aggregated alert transaction format to discover intrusion behaviors. Besides, the Model Constructing Phase is used to construct three kinds of rule classes: normal rule classes, intrusion rule classes and suspicious rule classes, to filter false alert patterns and analyze each existing or unknown alert patterns; each rule class represents a set of classification rules. Normal rule class, a set of false alert classification rules, can be trained by using sequential pattern mining approach in an attack-free environment. Intrusion rule classes, a set of known intrusion classification rules, and suspicious rule classes, a set of novel intrusion classification rules, can be trained in a simulated attacking environment using several well-known rootkits and labeling by experts. Finally, the Rule Refining Phase is used to change the classification flags of alert sequence across different time intervals. According to the urgent situations of different levels, Network administrators can do event protecting or vulnerability repairing, even or cause tracing of attacks. Therefore, the decision support system can prevent attacks effectively, find novel attack patterns exactly and reduce the load of administrators efficiently.     

攻击案例综合学习系统研究

随着入侵检测系统在安全领域的广泛应用,入侵报警学习和分析已经成为一个研究热点。针对目前入侵报警泛滥和知识贫乏等问题,设计了一个完整的攻击案例学习系统框架。该学习系统分为两个阶段：入侵报警精简和典型攻击案例挖掘。前者利用改进的密度聚类方法实现相似报警聚合以及报警聚类的自动精简表示,后者利用序列模式挖掘方法挖掘频繁入侵事件序列。进一步提出一种基于入侵执行顺序约束关系的攻击案例评估算法实现典型攻击案例的自动筛选。最后,利用真实入侵报警数据测试了该攻击案例学习系统,结果表明该系统能够实现高效报警精简和典型攻击案例的准确学习。     

基于多传感器的嵌入式安全监控体系研究

提出一种基于多传感器的嵌入式系统安全状态监控体系。该监控体系通过对安全威胁等级的合理划分、优先级设计以及各监控点安全等级关联,建立攻击行为的匹配、处理规则,给出一种基于数据融合的监控感知数据处理模型。应用实例及性能评估结果表明,该安全状态监控体系能够准确、及时地发现并应对针对系统的各类攻击行为,极大地提升系统的整体安全性。