论文部分内容阅读
安全协议形式化分析方法通过规范描述和数学推理来检验安全协议是否满足各种安全要求。GSPM是安全协议形式化分析的一般模型。在该模型中加入新鲜性的定义,形式化描述了新鲜性这一特殊的安全性质,扩展了GSPM的适用范围,并通过Andrew Secure RPC协议给出了形式化分析新鲜性的实例研究。
基于GSPM的安全协议新鲜性分析
【摘 要】
：
安全协议形式化分析方法通过规范描述和数学推理来检验安全协议是否满足各种安全要求。GSPM是安全协议形式化分析的一般模型。在该模型中加入新鲜性的定义,形式化描述了新鲜性这一特殊的安全性质,扩展了GSPM的适用范围,并通过Andrew Secure RPC协议给出了形式化分析新鲜性的实例研究。
【机 构】
：
上海交通大学计算机科学与技术系,湖州师范学院计算机科学与技术系
【出 处】
：
计算机应用研究
【发表日期】
：
2007年11期
其他文献
用卷积码的活性距离来分析卷积码的性能是随着分析Turbo码的性能而开始的,卷积码的活性距离是自由距离的扩展,它主要是由一个参数来决定的,即活性距离的斜率α。在对卷积码的活性距离进行简要介绍后,主要针对应用α对编织卷积码进行优化作出了探讨,指出了卷积码的活性距离α是分析用卷积码作为成员码的组合编码性能的重要参数。这对优化用卷积码作为成员码的组合编码,降低其编码复杂性有重要作用,也对推动该类组合码的应
介绍了一种新的证书撤销方案———NewPKI证书撤销方案,运用这种新的撤销机制解决公钥证书与属性证书不能简单合并的问题。定义了一类新的属性———NewPKI属性,并且将NewPKI属性与X.509公钥证书相结合,从而提出一类新的证书———融合证书。融合证书保留与X.509 v3证书相同的证书格式,且能够将属性加到X.509身份证书中,它能够作为一个理想的机制来携带属性信息而不需要属性证书,在很多情
基于彩色图像的四元数模型,将彩色人脸图像视为一个模板直接处理,并首次将奇异值向量应用到彩色人脸识别中。首先证明了彩色图像的奇异值向量具有代数和几何不变性;然后将其提取为图像的代数特征并应用到人脸识别中。实验表明该方法的识别率为90%左右,是一种有效的彩色人脸识别方法。
针对训练大样本支持向量机内存开销大、训练速度慢的缺点,提出了一种改进的算法—边界邻近支持向量机。实验表明在分类效果相同情况下,改进算法训练速度明显提高。
建立了一个新的智能化计算机辅助概念设计环境。该环境除巧妙地将计算机图形学理论、建筑设计专业知识和群体智能中的蚁群算法集成在一起外,还根据建筑构件间的实际偏序关系,在原算法的基础上引入了一种可使蚁群变得更聪明的创新机制。实验表明,该环境运行性能良好、样例构思新颖。
提出的过程—角色模型从动态视图描述了框架的控制流及相关角色,体现了框架的运行时体系结构。过程—角色模型和特定的框架实现模式相分离,在一定抽象层次上描述框架,可作为软件框架的元模型。
为增强IDS之间信息共享和交换的能力,加强IDS之间的交流和协作,给出了统一入侵报警信息格式的详细提案,并提出了用XML Schema对报警信息建模的方案,最后用XML描述语言实现了该提案并通过了XML Schema的有效性验证。所提出的统一入侵检测报警信息格式提案给不同IDS之间和IDS不同组件之间提供了信息共享和信息交换的平台,对于增强IDS之间以及IDS和其他安全设备的协作能力具有十分重要的
首先实时提取参考路面的平均色度值,对图像进行自适应分割,初步划分出可疑障碍区域;然后选取可疑障碍区域的对角线,利用立体视觉的方法进一步检测出障碍区域。证明了两摄像机平行放置时左右图像中区域对角线的对应关系,在此基础上进行匹配计算。该方法能适应光照条件变化,提高立体视觉算法速度,实验结果表明了该方法的有效性和可靠性。
介绍了一种从流媒体接收者的角度对流媒体性能进行测量的方法,提出了相应的应用层评价指标。利用已有的商业化流媒体服务软件,通过改变网络环境在不同的条件下对指标进行测量,最后通过实验数据来验证这些指标的有效性。