非否认协议形式化分析技术

对目前现有的非否认协议的几种形式化分析方法进行了分析和比较,指出了它们的优缺点,最后提出了进一步的研究方向。

积极推进课程建设改革,着力培养学员创新能力

课程建设质量决定人才培养质量,影响学员创新能力的发展,因此,积极开展课程建设改革十分重要。本文结合"装备原理"课程建设的实践经验,针对如何培养学员的创新能力,着重从课程目标、课堂教学、实践教学和考核方式等方面进行了探讨。

基于一阶逻辑的非否认协议模型

为了将密码协议的非否认性和公平性统一在一个框架之下更好地进行分析,提出了一套适用于分析非否认性和公平性的一阶逻辑语法和语义。在此基础上建立了一个用于分析非否认性和公平性的一阶逻辑模型,并以FairZG非否认协议为例进行了分析,发现了该协议的一个已知攻击,证明了模型的有效性和正确性。

SPFPA:一种面向未知安全协议的格式解析方法

针对未知安全协议的格式解析方法是当前信息安全技术中亟待解决的关键问题.现有基于网络报文流量信息的方法仅考虑报文载荷中的明文信息,不适用于包含大量密文信息的安全协议.针对该问题,提出一种新的面向未知安全协议的格式解析方法(security protocols format parsing approach,SPFPA).SPFPA首次利用序列模式挖掘方法层次化、序列化提取协议的关键词序列特征,为明文信息格式解析提供一种新的解决思路,并在此基础上给出查找协议密文长度域的启发式规则,进而利用密文数据的随机性特征确定密文域.实验结果表明,该方法在不借助任何主机运行特征的基础上,仅依靠网络报文数据即能够有效解析未知安全协议的不变域、可变域、密文长度域及相应的密文域,并具有较高的准确率.

基于熵估计的安全协议密文域识别方法

现有基于网络报文流量信息的协议分析方法仅考虑报文载荷中的明文信息,不适用于包含大量密文信息的安全协议。为充分发掘利用未知规范安全协议的密文数据特征,针对安全协议报文明密文混合、密文位置可变的特点,该文提出一种基于熵估计的安全协议密文域识别方法 CFIA(Ciphertext Field Identification Approach)。在挖掘关键词序列的基础上,利用字节样本熵描述网络流中字节的分布特性,并依据密文的随机性特征,基于熵估计预定位密文域分布区间,进而查找密文长度域,定位密文域边界,识别密文域。实验结果表明,该方法仅依靠网络数据流量信息即可有效识别协议密文域,并具有较高的准确率。

自组网环境下基于组合公钥的分布式密钥管理

结合组合公钥密码体制和秘密共享思想,针对移动自组网环境,提出了一种分布式密钥管理方案。从系统初始化、管理平台构建、节点公私钥生成、私钥矩阵份额更新等4个方面进行了详细描述,并给出了具体实施方法。分析表明,该方案具有安全性高、扩展性强、计算量小、适用性好的特点,特别适合移动自组网环境。

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

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

基于主体行为的多方安全协议会话识别方法

针对分布在多个相关流中的多方安全协议会话问题,提出了多方安全协议会话的3个启发式的主体行为特征——邻接主机行为、主体角色行为以及主机消息行为,给出了主体行为特征检测原理,提出了多方安全协议会话识别方法。针对3个典型的多方安全协议,分别在3种会话运行场景下进行实验,结果表明该方法识别率在90%以上,误报率和漏报率在6%以下,能够有效地识别协议会话。

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

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

具有计算可靠性的符号模型

MW方法仅考虑使用公钥加密原语,不包含{{m}k}k'类型消息的双方协议。针对该问题,使用公钥加密和对称加密,建立扩展标记符号模型与扩展计算模型,论证扩展标记符号模型的计算可靠性,实现对MW方法的扩展。

主动攻击下数字签名的计算可靠性

研究在密码协议仅使用数字签名原语时,主动攻击下符号形式化分析系统的计算可靠性。借鉴Micciancio-Warinschi方法,分别引入符号模型和计算模型中的协议运行状态集合,通过反证法证明符号模型中的迹与计算模型中的迹之间的对应关系,建立数字签名的计算可靠性,即如数字签名方案满足N-UNF,则符号模型所得到的结果在计算模型中也是正确的。基于该结论,可以构建具有计算可靠性的形式化分析系统。

一种基于问题求解理论的密码协议形式模型

提出了一种基于问题求解理论的密码协议模型,给出了模型的基本语法以及基于ρ演算的形式语义,明确了模型推理过程中涉及到的一些关键性的概念和命题。该模型具有以下特点能够对密码协议进行精确的形式化描述;具有合理可靠的可证明语义;对密码协议安全性的定义精确合理;便于实现自动化推理。所有这些均确保了基于该模型的密码协议安全性分析的合理性和有效性,为正确的分析密码协议的安全性提供了可靠依据。

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

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

调和安全协议两种分析方法的理论研究

安全协议形式化分析方法分为两种,即符号方法和计算方法。比较两种方法,它们各有优缺点。目前,将两者进行组合优化,建立统一的调和方法框架对安全协议进行分析是研究的热点和难点。针对该问题,对目前国际上流行的相关方法进行了分类总结,并对涉及到的技术手段进行了全面分析。

基于半监督子空间聚类的协议识别方法

针对现有的基于统计特征的协议识别方法选择识别特征时未考虑不同协议个体之间的差异的问题,结合半监督学习和模糊子空间聚类(FSC)方法,提出了一种半监督子空间聚类协议识别方法(SSPIA)。首先,将有标签的样本流转化为成对约束信息,从而获取先验约束条件;其次,在此基础上提出半监督模糊子空间聚类(SFSC)算法,该算法利用约束条件指导子空间聚类过程;然后,建立类簇和协议类型的映射,以获取协议各个特征的权重系数,进而构建个体化的密码协议特征库用于后续协议识别;最后,针对5个典型的密码协议进行聚类效果和识别效果实验。实验结果表明,针对基于统计特征的协议识别问题,与传统K-means方法和FSC方法相比,所提SSPIA的聚类效果更好,且SSPIA构建的协议识别分类器更为精确,协议识别率更高,误识别率更低。所提SSPIA提高了基于统计特征的识别效果。

应用改进卷积神经网络的网络安全态势预测方法

针对神经网络态势预测模型训练复杂度高的问题,提出了一种基于改进卷积神经网络的态势预测方法。结合深度可分离卷积与分解卷积技术的优点,提出了一种基于复合卷积结构的改进型卷积神经网络安全态势预测模型,实现了态势要素和态势值的映射。实验仿真结果证明,相比于已有的典型预测方法,该方法明显降低了复杂度,减少了预测时间,并提升了预测准确率。

一种基于状态扩展的安全协议验证机制

基于模型检测验证协议的方法存在状态空间爆炸问题,其中基于目标绑定搜索状态空间的方法有效控制了状态空间,但不能完全给出协议的运行情况。针对这一问题,提出了一种基于状态扩展的安全协议自动化验证机制,首先对协议状态进行初始搜索,给出协议运行需要的事件,得到协议基本状态,然后进行扩展搜索,考虑基本状态与其他协议运行的关系,形成协议扩展状态。该机制能够有效反映出协议的运行情况,且能够同时对多种安全性质进行验证。

基于事件顺序的时间戳协议处理

在不考虑网络延迟的情况下,提出一种基于事件顺序的时间戳协议处理方法。在分析时间戳大小与事件关系的基础上,证明为使事件绑定时主体接收的时间戳是新的,状态转移必须满足时间戳关系无环性,并基于事件顺序给出时间戳关系无环性的验证算法。实例表明,该方法易于实现,且具有一定适用性。

基于逻辑程序的访问控制描述与推理

提出访问控制的逻辑描述方法,满足最小模型语义的条件(不含负逻辑),并分析访问控制逻辑程序中不动点的迭代计算方法。通过迭代计算,得到访问控制逻辑程序的最小Herbrand模型——Mp。使用基于逻辑程序的方法对访问控制策略进行了较为精确的推理。