基于防篡改的双重软件水印方案

针对软件水印抗攻击性差和编码数据率低的缺点,提出一种具有防篡改功能的双重软件水印方案.利用寄存器分配的隐蔽性构造改进颜色排列算法.结合基数k编码的高数据率及平面环路树编码的强抗攻击性,构造混合编码双循环链表平面环路树.水印嵌入后,通过校验和机制及高级加密标准代码加密,防止逆向工程等手段对软件水印的篡改.理论分析和实验数据表明,该方案有较高的隐蔽性、鲁棒性和数据率,实用性较强.     

从线性时序逻辑公式到自动机的转换算法

To combat the well-known state-space explosion problem in Propositional Linear Temporal Logic (PLTL) model checking, a novel algorithm capable of translating PLTL formulas into Nondeterministic Automata (NA) in an efficient way is proposed. The algorithm firstly transforms PLTL formulas into their non-free forms, then it further translates the non-free formulas into their Normal Forms (NFs), next constructs Normal Form Graphs (NFGs) for NF formulas, and it finally transforms NFGs into the NA which accepts both finite words and infinite words. The experimental data show that the new algorithm reduces the average number of nodes of target NA for a benchmark formula set and selected formulas in the literature, respectively. These results indicate that the PLTL model checking technique employing the new algorithm generates a smaller state space in verification of concurrent systems.     

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

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

后量子密码CRYSTALS-Kyber的FPGA多路并行优化实现

在基于格的后量子密码中,多项式乘法运算复杂且耗时,为提高格密码在实际应用中的运算效率,提出了一种后量子密码CRYSTALS-Kyber的FPGA多路并行优化实现。首先,描述了Kyber算法的流程,分析了NTT、INTT及CWM的执行情况。其次,给出了FPGA的整体结构,采用流水线技术设计了蝶形运算单元,并以Barrett模约简和CWM调度优化,提高了计算效率。同时,放置32个蝶形运算单元并行执行,缩短了整体计算周期。最后,对多RAM通道进行了存储优化,以数据的交替存取控制和RAM资源复用,提高了访存效率。此外,采用松耦合架构,以DMA通信实现了整体运算的调度。实验结果和分析表明,所提方案可在44、49、163个时钟周期内完成NTT、INTT及CWM运算,优于其他方案,具有较高的能效比。     

NSSK协议的串空间模型及分析

本文介绍了串空间模型中的基本概念和定理,并首次利用串空间理论,从机密性和认证性两个方面,对改进的NSSK协议进行了分析.分析结果表明改进的NSSK协议是安全的.     

用于安全协议分析的一种新的状态剪枝方法

Strand空间模型是利用图的形式来描述和分析安全协议的。通过对该模型的研究,总结了已有的状态空间简化技术;研究了如何将认证测试理论应用于安全协议分析中,根据认证测试理论我们得出了一个剪枝定理。研究表明该剪枝定理能够大大减少协议分析中的冗余状态,提高了协议分析的效率。     

基于Snort的IPv6入侵检测系统的研究

本文以著名的开源网络入侵检测系统Snort为基础，通过跟踪国内外网络入侵检测系统的研究动向和Snort的研究热点，在对Snort源代码进行分析的基础上，提出Snort系统在IPv4向IPv6过渡阶段的相应改造方案。通过构造IPv6检测规则，添加IPv6解码模块，IPv6分段重组，IPv6快速检测算法以及对过渡技术的支持，实现了一套同时支持IPv4、IPv6和过渡技术的入侵检测系统。     

基于移动代理和免疫原理的IDS模型研究

目前的入侵检测系统大多是等级结构的,容易出现单点失效和网络拥塞问题,把移动代理技术和人工免疫原理应用到入侵检测系统(IDS)中,充分结合二者的优点,使IDS具有更高的容错性和健壮性。     

时间自动机与网络协议验证

随着网络协议复杂性的增大，其自身的潜在错误变得更加重要。使用形式化的方法来描述和验证网络协议可以发现其中的潜在错误。时间自动机是形式化方法的一种，可以很好地应用于网络协议验证中。目前基于时间自动机已经开发出了多种自动验证工具。文章介绍了网络协议验证的几种方法，并以KRONOS验证FDDI协议为例说明了用时间自动机验证协议的方法。