共查询到20条相似文献，搜索用时 187 毫秒
1.
分析了模型检测技术和逻辑推证技术的优点与不足,并在此基础上提出了一种混合的形式化分析技术的说明,该技术可提供更为完全的安全协议形式化分析. 相似文献
2.
综述目前安全协议形式化分析的理论与方法,包括安全协议的分类与模型,安全协议形式化分析的 3种典型方法 (基于推理的结构性方法,基于攻击的结构性方法,基于证明的结构性方法 ),安全协议分析的形式化语言,安全协议设计的形式化方法,以及安全协议形式化分析面临的挑战. 相似文献
3.
给出用PVS对密码协议进行形式化规范的一种方法.该方法以高阶逻辑为规范语言,利用trace模型来描述协议的行为,并假设系统中存在强攻击者和理想加密系统.重要的结构如消息、事件、协议规则等都通过语义编码方式定义. 相似文献
4.
介绍了抽象状态机（ASM）,建立了基于这种形式化方法的协议描述于验证的环境,并建立了一般意义上的入侵者模型.作为应用实例,给出了 Helsinki协议的 ASM规约,说明利用这个规约可以直观的演绎 Horng-Hsu攻击. 相似文献
5.
主要使用运行模式法对简化的SSL30基本握手协议进行了形式化分析.通过分析,找到了3种不同的攻击形式,并且对这3种攻击形式进行了深入研究,发现这3种攻击虽然从表面上看都是由于允许不同版本共存的漏洞引起的,但是经过仔细分析攻击的形式,发现这3种攻击是存在差异的.主要是角色欺骗不相同,而这又可能会造成潜在攻击.最后对这个协议进行了改进,从而有效避免了以上3种攻击,提高了协议的安全性 相似文献
6.
为π演算建立具有安全级别的简单类型系统,并证明该类型系统在规约语义下的类型可靠性.此类型系统使得π演算成为安全系统、安全协议分析与规范的普适形式化工具. 相似文献
7.
依照下一代网络协议的发展趋势,分析IETF提出的SIP协议和P2P网络结合的P2P-SIP网络的特点,针对其优势和不足提出一个基于椭圆曲线算法并适用于IPv6的P2P-SIP无证书匿名通信协议,使用CK安全模型对方案的安全性进行了证明. 对协议的安全性分析表明,该协议具有相互认证、完美前向保密性、匿名性、已知密钥安全、非密钥泄露伪装等安全属性;协议可抵御已知密钥攻击、中间人攻击、SYBIL攻击等攻击. 通过与已知协议的比较可知,该协议有更好的安全性和效率. 相似文献
8.
提出一个基于混合密码体制的抗否认密码协议 :可以运行在不安全信道上实现交易的公平性与通信双方的不可否认性;在通常情况下只需通信双方进行 3次信息的交互,且保证传递数据的机密性与收发方交易的隐私权;避免了可信第三方可能成为系统瓶颈的问题.最后给出该协议的形式化分析,证明了它的公平性、安全性与可行性. 相似文献
9.
针对网络通讯软件的Fuzzing技术受限于协议格式,尤其是未知协议难以保证测试效果,提出了基于符号表达式的协议分析方法.将数据包关键处理代码翻译为符号表达式,利用符号表达式的丰富含义加快未知协议格式分析,并依此开发了协议格式分析及漏洞挖掘框架PAVD.通过对亿邮客户端的漏洞测试,验证了PAVD能有效提升协议分析效率,为网络通讯软件Fuzzing测试提供良好的支持. 相似文献
10.
介绍了L2TP协议和IPSec协议的基本原理,分析了L2TP协议实现VPN时存在的安全问题,提出了一种将L2TP协议和IPSec协议相结合,利用IPSec为L2TP协议提供保护的安全隧道技术方案,并实现了基于IPSec的L2TP传输VPN实例. 相似文献
11.
采用Gröbner基方法,可以把一个在有限群作用下不变的多项式写成不变环的生成元的多项式.核心问题是如何有效地计算这个正维不变理想的Gröbner基.本文引入一个有效提升算法来计算这组Gröbner基.当用straight line program模型对整个计算过程进行复杂度分析时,可以把计算开销控制在多项式时间内. 相似文献
12.
徐斌 《玉溪师范学院学报》2006,22(3):12-15
把原函数看成是-1阶的导数,定义了一类n阶导数通式,称为不变n阶式.利用“不变n阶式”概念,对不定积分进行了求解分析,结果发现,用n阶导数的形式不变性可以对不定积分进行求解. 相似文献
13.
线性混合模型(linear mixture model,LMM)在端元提取中起着至关重要的作用.在LMM假设下,理想的端元提取效果需要重建误差最小.但是在实际的高光谱数据集中噪声是不可避免的,单纯追求重建误差最小化可能会导致最终结果偏离真实端元.为平衡重建误差与噪声的影响,使用几何优化模型计算重建误差,通过约束重建误差... 相似文献
14.
形状特征是目标识别的重要参数,而小波变换的低频部分代表物体的总体形状特征.首先选取SYM小波,利用小波变换的低频系数重构图像提取物体总体形状,进而利用特征不变矩距离进行目标识别。将该方法应用在实测车标图像的识别中,结果表明该方法识别效果较好。 相似文献
15.
SIFT是尺度不变特征的变换,因具有较强的鲁棒性,广泛应用于人脸识别系统当中.本文总结分析了现有采用SIFT特征提取的人脸识别技术,发现基于SIFT的识别系统所用算法的识别率不高,且耗时长.研究引入了权重函数,提出了对人脸识别系统数据库的数据结构的优化方法,不但提高了人脸识别系统的识别率,而且缩短了识别系统的运行时间. 相似文献
16.
研究具有一对纯虚特征值的实系统的实不变代数曲线在原点空心邻域非零的性质,使用不变代数曲线和指数因子构造局部首次积分或积分因子,提出进行平衡点类型判别的方法。 相似文献
17.
沈关生 《上海海事大学学报》1990,(4)
本文讨论了层次分析法中用特征向量估计方案权与方案下标序的关系。指出特征向量法的解相对于方案下标序来说是不变的,而梯度特征向量法的解依赖于方案的下标序。同时,证明了当方案个数为3时,梯度特征向量法的解的几何平均就等于特征向量法的解。 相似文献
18.
季益水 《安徽职业技术学院学报》2004,3(4):56-61
“传神”对于文学翻译而言是一个较高的要求 ,也是提高译文质量的重要手段。欲要使译文传神 ,绝不可忽视文学的物质属性。因为 ,抽象的“神”必须扎根于物质的 (具体的 )措辞、句法、表达方式等之中。欲要传“神”,必须首先知道“神”在何处。这就要从文学的物质属性入手 ,通过语内比较来充分领会原文的“神”,是文学翻译传神的先决条件。文章通过对一些未能传神的译文实例的分析 ,探讨了语内比较在文学欣赏乃至传神翻译方面的重要作用。 相似文献
19.
SAR图像的绝对辐射精度直接影响SAR定量化应用水平，现有基于定标器的绝对辐射定标方法难以对SAR系统进行持续监测。如能在普通场景中找到一种稳定的散射特征量，则可将其作为参考实现常态化定标。针对C波段SAR图像，建立不同类别地物散射样本库，分析发现城区的后向散射系数中值重心具有良好的时间稳定性，进而提出一种基于神经网络的城区地物精筛与散射稳定特性提取方法。测试数据及与热带雨林数据的比较实验表明，该方法提取的散射稳定特性可用于SAR系统的常态化辐射定标。 相似文献
20.
李永才 《济宁师范专科学校学报》2006,27(4):63-65
本文分析了语言教师在英语课堂教学中较少采用文学作品的原因。它反映了语言研究和文学研究的历史性分歧,从而限制了文学在语言教学中的作用。然而,在课堂上文学教材的采用,不仅能使之成为语言教学的一种有力的工具,而且还可为学习者提供更多的理解和掌握语言知识与训练交际技巧的机会。本文还阐述了语言课堂中综合教授文学方法的基本原理,其前提就是文学是语言,而语言也的确能成为文学性的。 相似文献