论文部分内容阅读
文章介绍了密钥交换协议SSL 3.0协议,并利用模型检测工具SPIN对其进行了形式化分析、建模和验证。实验结果表明此验证方法的正确性,证明了协议本身的安全性与可行性,并且提高了协议的验证效率。
基于SPIN的SSL 3.0握手协议模型检测
【摘 要】
：
文章介绍了密钥交换协议SSL 3.0协议,并利用模型检测工具SPIN对其进行了形式化分析、建模和验证。实验结果表明此验证方法的正确性,证明了协议本身的安全性与可行性,并且提高了协议的验证效率。
【机 构】
：
南昌大学信息工程学院,南昌,33003 江西省信息中心,南昌,330046
【出 处】
：
第七届全国Web信息系统及其应用学术会议、第五届全国语义Web与本体论学术研讨会、第四届全国电子政务技术及应用学术研讨会
【发表日期】
：
2010年9期
其他文献
自十三世纪中叶始,“哈剌章＂和“察罕章＂二字始见于元代蒙古历史文献。经国内外专家学者们的研究和考释,大部分问题已经得到精确的解释,但是,对于其中的一些问题,到目前为止,学
分布式计算系统上的最优任务分配的研究是有效利用系统资源处理实际问题的热点课题。提出的任务分配算法,通过对任务的数据量来估算计算量,然后将数据量按计算量大致相同分配到各个负载,实现分布式三维重建中计算资源的合理分配。还通过实验比较和实例分析验证了任务分配算法的正确性和有效性。因此,提出的任务分配确实能够比较有效和灵活地解决分布式系统的负载均衡问题。
为满足现代企业销售部门的数据分析与决策制定的需求，将联机分析处理技术应用于销售分析系统中。首先介绍了数据仓库和联机分析处理的概念、特点及结构，然后建立了销售分析系统
针对目前内存数据库中索引缓存失配的问题，在分析了现有内存数据库索引结构基础上，提出了一种缓存敏感T树（CST树）的索引数据结构，详细数据结构描述和操作算法也已给出。通过CST树
医疗保险付费方式与公立医院体制机制的适配性，关系到医药卫生体制改革的成败。文章探讨了保险付费方式和公立医院体制机制搭配的依据、错配的形式和矫正的思路，并向政府提出统
分析现有复杂背景下运动目标检测与分割算法存在的不足,提出一种基于帧间差分与时空相关性分析的运动目标检测算法。结合帧图象中象素的空间相关性和帧间差分进行运动目标的分离,用序列图象中运动目标所具有的时间相关性来验证目标的真实性,剔除虚假的运动信息。实验结果表明,能较好地检测出目标,具有较好地抗干扰能力。
目前，电梯群控系统已经得到普遍的应用，但是对群控电梯的独立远程监控还有待研究发展，因此实现群控电梯的集中监视管理系统更具有现实意义。文章通过对一大型新建国际机场航站楼