论文部分内容阅读
快速密钥交换协议JFK是一种新型的密钥交换协议，它的安全性引起了人们的重视。论文对密钥交换协议交换过程进行分析的基础上，使用Promela语言描述了协议模型，并用LTL刻画了需要满足的性质，最后对协议验证结果分析，表明该协议满足其设计目标。
快速密钥交换协议JFK的SPIN模型检测
【摘 要】
：
快速密钥交换协议JFK是一种新型的密钥交换协议，它的安全性引起了人们的重视。论文对密钥交换协议交换过程进行分析的基础上，使用Promela语言描述了协议模型，并用LTL刻画了需要
【机 构】
：
南昌大学,佳木斯大学
【出 处】
：
佳木斯大学学报(自然科学版)
【发表日期】
：
2008年1期
其他文献
本文分析了自然风对屋顶通气管的抽吸和倒灌规律,认为如果通气管的位置、高度、通气帽等设计不当,自然风将会对排水系统的正常运行产生不良影响,文中提出了设计屋顶通气管时
本文综合了我国东北地区的多年实际调查实测资料,结合理论验算和分析,说明寒冷地区排水管道的埋深,可以较现行室外排水设计规范所规定的埋深减小,以节省建设投资。文中还提出
针对突发事件的复杂性及相似案例的稀缺性,提出基于情景划分构建突发事件应急响应策略库的方法。有别于已有"情景—应对"研究关注突发事件情景全过程的相似性,该模型将突发事
网络信息化时代已经到来,高校学生工作在此大背景下面临变革.如何利用现代化网络信息手段,更快捷、高效地开展学生工作值得认真探讨.多元化信息平台的建设可以使高校学生工作
伴随着网络的普及和数据库的广泛应用,包括银行等企事业单位在内的几乎每一个组织都建立了网络化的数据库管理系统。数据库的网络化管理在为企业提供办公自动化、数据共享等
PPP是当前政府力推的一种吸引社会投资的投融资管理模式,虽然政府对其愿望比较强烈,但社会资本顾虑重重且参与的积极性不高。从推介与实施时滞性、信息透明性、投资收益吸引
沥青混凝土路面具有坚实、耐久、平整、良好的抗滑性,防渗、耐疲劳的性能和抗高温开裂的温度稳定性,因此我国大部分城市道路都采用沥青混凝土路面。沥青混凝土路面质量控制包
《行政强制法》第二十五条对查封扣押强制措施的期限做出了明确规定，即一般期限为30日，情况复杂的可延长30日。该条第三款还规定了期间中止的情形：“对物品需要进行检测、检验、
报纸
<正>《周易·系辞下》载:"天下同归而殊途,一致而百虑。"浩荡千年,进行先秦各家乐舞理论体系研究的学者们,其成果早已汗牛充栋。百家争鸣中,儒道两家乐舞思想各自的支持和拥