【摘 要】
：
形式化方法由于其精炼、简洁和无二义性,逐步成为分析加密协议的一条可靠和准确的途径,但是加密协议的形式化分析研究目前还不够深入,至今仍没有统一的加密协议验证体系.针对
【机 构】
：
中国科学院研究生院信息安全国家重点实验室,广州大学理学院数学系信息安全研究所,武汉大学计算机学院软件工程国家重点实验室,华南农业大学理学院计算机系
论文部分内容阅读
形式化方法由于其精炼、简洁和无二义性,逐步成为分析加密协议的一条可靠和准确的途径,但是加密协议的形式化分析研究目前还不够深入,至今仍没有统一的加密协议验证体系.针对这一现状,该文从加密协议可能面临的最强大的攻击着手,提出了一种基于时序逻辑的加密协议描述方法,在该模型下,对协议行为、入侵者行为、安全需求等特性的描述均用时序逻辑公式表达,从而利用现有的统一的时序逻辑框架分析密码协议的性质.特别地,作者描述和检测了一个系统入侵者不能用任何代数和逻辑的办法获得消息的实例.通过对比,作者认为该方法具有形式化程度较高
其他文献
该文给出了量化系数嵌入水印比特信息的基本原理,在此基础上提出了数字音频信号的脆弱水印嵌入算法.该算法充分利用离散子波变换的多分辨率特性,通过等概率随机量化音频信号
图像分割是图像处理中的一个难题 .为了自动抽取图像中的可判别区域 ,提出了一种基于自组织图归约算法的区域抽取新方法 .首先 ,利用包括颜色、纹理以及位置在内的多模特征抽取算法 ,原始图像被转换成特征图 ;接着 ,通过自组织映射学习算法 ,特征图被映射成自组织图 ;然后 ,对自组织图实施归约算法得到一族约简的自组织图谱系 ;最后 ,利用一个综合的聚类有效性分析指标从约简的自组织图谱系中得到一个最优约
该文提出一种对场景进行多视点成像的方法 .该方法首先为场景中的多边形生成多边形模板 ,一个多边形模板 ,包括一条轮廓路径和一组纹条 ,而一个纹条是平行成像面的一个平面与多边形相交的直线段 .由于纹条相对于不同视点的透视投影的变化是线性的 ,因此 ,绘制多边形时可以基于模板逐个纹条地处理 ,而不必按照传统的扫描转换方法逐个点地处理 ,绘制速度可以提高很多 .同时 ,与视点无关的光照和纹理可以预先计算
该文遵循笔者提出的'整词中枢论'思想,基于自然语言复杂特征合一运算理论、方法和技术,通过揭示蒙古语动词构成数学结构,提出了蒙古语动词构成算法的数学模型(机理模
针对对流传热边界条件,本文建立了一种平板逆流交换器的数值模型,分析了溶液温度场、浓度场和空气温度场的分布规律。采用氯化锂溶液作为除湿剂,通过实验方法进行验证,结果表
低密度校验（LDPC）码具有编码增益高，译码速度快，可并行译码等特点，是当前编码界的一个研究热点，但是目前已有的研究成果都集中在高斯信道上，该文分析和讨论了LDPC码在瑞利衰落信道下
Web挖掘的一个重要研究方向是发现用户的迁移模式。一般来说，用户的迁移具有某种目的性。这种目的性表现为用户对某种概念的兴趣。文中提出基于隐马尔可夫模型的兴趣迁移模式
设计项目位于江门市高新区,根据设计所给的资料,通过技术经济分析,选用大温差水蓄冷为宜。空调末端进出水温度为8~11℃/13~16℃,放冷工况进出水温度为12~15℃/4~7℃,利用消防
DiffServ模型是当前实现IP QoS的体系结构之一,在其实现中,缓冲管理技术是很重要的一个方面.根据DiffServ模型实现的需要,在分析现有缓冲管理算法的基础上,提出了QPRED多级主
在多联机空调系统中,一台外机接多台内机,由于在空调运行过程中,全部室内机所处的室内侧负荷变化不同,这要求室内机具备与之同步的处理负荷的能力,尤其是当有部分室内侧环境