【摘 要】
：
安全协议分析和验证在信息安全领域占有重要地位。目前，安全协议形式化方法分析和验证主要集中在对实用性较差的安全协议抽象规范分析和验证方面，对注重实用性的安全协议代码分
论文部分内容阅读
安全协议分析和验证在信息安全领域占有重要地位。目前，安全协议形式化方法分析和验证主要集中在对实用性较差的安全协议抽象规范分析和验证方面，对注重实用性的安全协议代码分析和验证涉及比较少；而静态程序验证技术的应用主要集中在程序正确性等方面，很少涉及代码的密码学安全性。因此本文将结合安全协议形式化分析与验证和静态程序验证技术来分析和验证安全协议Java代码密码学安全性。本研究成果具有较强的理论意义和一定的应用价值。本文主要工作如下：1.对安全协议分析和验证做了一个完整的概述，说明了进行形式化分析的必要性，介绍了形式化分析的模型并详细描述了形式化分析和验证的方法。2.探讨了Java语言的形式化描述，具体介绍了Java语句和表达式到应用PI演算语句的映射。同时，介绍了程序静态分析方法，研究了如何利用抽象语法树对程序进行预处理。3.首先探索Java代码抽象模型抽取方法和从Java代码到应用PI演算的映射；然后应用一阶定理证明器ProVerif分析与验证Needham-Schroeder协议Java代码的密码学安全性。
其他文献
2000年,R. Ahlswede等人提出了网络编码的概念,它完全颠覆了传统的路由方式。网络编码技术允许网络节点对接收到的数据信息进行编码处理,然后将编码数据包发送出去;接收端根
识别蛋白质相互作用网络中的模块结构，是理解细胞功能的组织结构以及动态性的第一步。因而，如何在蛋白质相互作用网络中寻找模块结构便成为一项十分重要而且极具挑战的任务。目
随着信息技术的迅速发展和现代教育需求的增长，E-learning（Electronic learning）逐渐成为人们生活中重要的学习方式。E-learning具有良好的交互性和较小的时空约束性，它能够不受
目标跟踪是计算机视觉和模式识别领域当前的研究热点问题之一,并且在诸如智能导航、自动监控、军事防御、人机交互等方面有着广泛的实际应用。虽然目标跟踪经过几十年的发展
第三代合作伙伴计划(3rd Generation Partnership Project,3GPP)考虑到互联网和传统运营商的融合,引入了IP多媒体子系统(IP Multimedia Subsystem,IMS)作为核心网的发展方向
由于技术的发展以及成本的降低,基因组测序在孟德尔遗传疾病,复杂疾病,以及癌症基因检测中得到了运用,并产生了海量的测序数据。这些数据对研究疾病的致病机制、疾病的临床诊
基于位置的服务(Location Based Service, LBS)是根据用户的位置信息提供服务的一种移动通信应用服务。在给用户带来便利的同时,现有LBS的工作机制也使得用户面临个人信息,甚
在当今信息化世界中，中文信息处理技术已经在各个领域中得到了广泛的应用。本文主要对中文分词算法中的基于分词词典机制的最大匹配算法进行研究讨论。由于中文语法语义复杂导
在飞速发展的交流调速系统中，交流变频电机作为主要的拖动方式已逐渐占据主导地位，在生产实践中的应用越来越广泛。而在采用了绝缘栅双极型晶体管(IGBT)器件的脉冲宽度调制(PWM)型变频器后，变频电机却出现了寿命问题，其中变频电机用漆包线耐电晕性能是制约其寿命的一个重要方面，这时就需要特定的测试仪器能够有效检测漆包线耐电晕的性能。在深入研究漆包线耐电晕测试相关技术的基础上，本文采用了IGBT的H桥技术
产品评论挖掘就是从用户发表的评论中挖掘出产品特征、用户观点，并判断观点极性，为生产、营销商家和潜在的用户提供参考。通过对提取出的产品特征进行分析，发现用户对产品特征粒