基于强认证理论的三方网络协议安全性证明

发布时间：2017-10-09 14:05

  本文关键词：基于强认证理论的三方网络协议安全性证明

  更多相关文章： 形式化方法 事件逻辑 强认证理论 Neuman-Stubblebine协议

【摘要】：形式化方法是分析网络安全协议的一种重要方法,网络协议安全性也是信息安全领域的研究热点。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于证明网络安全协议的安全性。以事件逻辑为基础,定义强匹配及匹配会话,结合事件逻辑公理和推理规则,提出了强认证理论。利用该理论对有3个主体的Neuman-Stubblebine协议进行了研究,分析得出发送者是安全的而接收者是不安全的,从而证明了该协议是不安全的,说明了强认证理论适用于三方的网络安全协议。该理论适用于类似多方网络安全协议的安全性证明。
【作者单位】： 华东交通大学软件学院;中国人民财产保险股份有限公司宁波市分公司信息技术部;
【关键词】： 形式化方法 事件逻辑 强认证理论 Neuman-Stubblebine协议
【基金】：国家自然科学基金Nos.61163005,61562026 江西省自然科学基金Nos.20132BAB201033,20161BAB202063 江西省对外科技合作技术项目No.20151BDH80005 江西省软科学研究计划项目No.20151BBA10042 江西省高校科技落地计划项目No.KJLD13038 南方山地果园智能化管理与装备协同创新中心资助项目 江西省普通本科高校中青年教师发展计划访问学者专项资金~~
【分类号】：TP393.08
【正文快照】： 1 引言 证明网络协议的安全属性是一个复杂的问题。形式化方法是一种强大的证明网络协议的安全属性的方法,其包括模态逻辑、定理证明和模型检测[1]。模态逻辑和定理证明又可笼统地归为一类。模型检测自动化程度高,用来验证系统的不安全性,但是只能对有限数量的并行通信进行研

【相似文献】

中国期刊全文数据库 前10条

1 古天龙;董荣胜;;欧洲高校计算机专业的形式化方法课程教学[J];计算机教育;2008年10期

2 柴振荣;《编程中的形式化方法及其应用》会议[J];管理科学文摘;1995年06期

3 郑士贵;智能服务网络形式化方法的模拟和实质[J];管理科学文摘;1997年01期

4 姜利;孙永强;;形式化方法的发展及展望[J];计算机科学;1998年02期

5 张广泉;关于软件形式化方法[J];重庆师范学院学报(自然科学版);2002年02期

6 鹿蕾;;形式化方法B的证明技术[J];现代电子技术;2005年23期

7 陈澎;设计模式形式化方法分析和初步比较[J];计算机工程;2005年02期

8 李建华;李红革;;形式化及其历史发展[J];自然辩证法研究;2008年08期

9 曹源;唐涛;徐田华;穆建成;;形式化方法在列车运行控制系统中的应用[J];交通运输工程学报;2010年01期

10 ;《软件学报》形式化方法和工具专刊征文通知[J];软件学报;2010年07期

中国重要会议论文全文数据库 前7条

1 李文健;;形式化的涵义及其认识论本质[A];1993年逻辑研究专辑[C];1993年

2 吴允曾;;关于形式化的几个问题[A];金岳霖学术思想研究——金岳霖学术思想研讨会论文集[C];1985年

3 郑宇军;石海鹤;薛锦云;;Spec#语言中的形式化特性[A];2005年全国理论计算机科学学术年会论文集[C];2005年

4 雷敏;雷友殉;;一种UML到SDL转换方法的研究与应用[A];2006通信理论与技术新进展——第十一届全国青年通信学术会议论文集[C];2006年

5 苗洁君;王克;;密码模块的形式化设计和验证研究[A];第二十一次全国计算机安全学术交流会论文集[C];2006年

6 缪道期;;评审计算机安全等级[A];第二次计算机安全技术交流会论文集[C];1987年

7 赵晓峰;;城市轨道交通自主化信号系统全面创新实践[A];中国系统工程学会第十八届学术年会论文集——A12系统科学与系统工程理论在各个领域中的应用研究[C];2014年

中国重要报纸全文数据库 前1条

1 殷杰 安军 山西大学科学技术哲学研究中心;21世纪科学哲学的关键词:语境、科学理性与形式化[N];中国社会科学报;2011年

中国博士学位论文全文数据库 前8条

1 刘艳;互联网内容分级服务技术标准体系的形式化设计与验证[D];华中师范大学;2015年

2 钱振江;安全操作系统形式化设计与验证方法研究[D];南京大学;2013年

3 刘强;设计模式的形式化研究及其EMF实现[D];华东师范大学;2011年

4 张鹏;形式化方法在云计算中的应用研究[D];吉林大学;2014年

5 刘洋;网络式软件需求验证的形式化方法研究[D];电子科技大学;2013年

6 王迈;语言形式化原理[D];上海外国语大学;2011年

7 胡静;基于Pi-演算的Web服务形式化描述模型[D];天津大学;2013年

8 周宁;代数化符号模拟验证的应用研究[D];北京交通大学;2015年

中国硕士学位论文全文数据库 前10条

1 王春晓;MDF连续平压质量控制形式化建模及优化研究[D];东北林业大学;2015年

2 王亚丽;面向机器人规划的形式化研究[D];北京化工大学;2015年

3 韩佳芮;基于Event-B和MAS的车站进路联锁控制逻辑的形式化方法研究[D];兰州交通大学;2015年

4 徐世泽;基于Timed RAISE的RBC切换建模与分析[D];兰州交通大学;2015年

5 郭叶芳;电网控制系统软件可靠性分析的形式化方法研究[D];华北电力大学;2015年

6 黄峰;系统演化的形式化与具体化研究[D];南京邮电大学;2014年

7 Hamza I.Bangura;基于Z规格的软件缺陷形式化方法[D];天津大学;2010年

8 钟琪;软件分析模式的形式化研究[D];西南师范大学;2004年

9 王祥兵;形式化方法的理论及其影响[D];贵州大学;2009年

10 郭忠伟;神经内分泌复杂系统的形式化研究[D];扬州大学;2009年

，

本文编号：1000590