基于Spin的安全协议形式化验证技术

发布时间：2019-09-20 05:40

【摘要】：针对安全协议的形式化验证问题,运用模型检测方法,以一种改进的入侵者Promela语义模型,对双方密钥分配中心协议进行Spin模型检测,验证发现其不满足线性时序逻辑(LTL)公式描述的安全性,得到了原协议的安全漏洞。针对该漏洞,提出了一种协议改进方案,并针对改进后的协议,给出新的Promela语义模型的建模方法。改进的入侵者模型建模方法比起原方法:模型检测过程中的存储状态数减少,使模型复杂度降低约40%;迁移状态数减少,使验证效率提升约44%。
【作者单位】： 中国科学院成都计算机应用研究所;中国科学院大学;广西混杂计算与集成电路设计分析重点实验室(广西民族大学);北京交通大学计算机与信息技术学院;
【基金】：国家自然科学基金资助项目(11371003) 广西自然科学基金资助项目(2011GXNSFA018154,2012GXNSFGA060003) 广西区主席科技资金资助项目(10169-1) 广西教育厅科研资助项目(201012MS274)
【分类号】：TN918.4

【共引文献】

相关期刊论文 前10条

1 李月寒;郑议天;;信息安全关键技术演示系统的设计与实现[J];合肥师范学院学报;2008年06期

2 王凯;高阳阳;秦雅娟;;分离机制下一种互联网安全接入方法[J];北京交通大学学报;2011年02期

3 李兰翠;孟博;;网络投票协议[J];长江大学学报(自然科学版)理工卷;2008年03期

4 桑林琼;王玉柱;;具有零知识特性的身份认证方案设计及分析[J];重庆科技学院学报(自然科学版);2008年04期

5 胡焰智;马大玮;田增山;;一种基于移动公网的安全专网认证与密钥协商方案[J];电讯技术;2008年03期

6 葛玮;谢坚;刘斌;;基于终端的计算机网络防御体系技术小析[J];江西电力职业技术学院学报;2011年01期

7 余磊;顾维娜;王猛;;基于串空间极小元理论的改进Woo-Lam协议的认证性分析[J];电脑编程技巧与维护;2010年04期

8 杨杰;;基于串空间理论的kerberos协议的安全性分析[J];电脑编程技巧与维护;2010年04期

9 刘慧芳;;基于串空间模型的Andrew安全RPC协议分析[J];电脑编程技巧与维护;2012年04期

10 曹进;;计算机协议安全漏洞及其防护[J];电脑知识与技术;2006年26期

相关会议论文 前8条

1 李秋山;胡游君;;低成本RFID系统安全协议设计及其形式化分析[A];2006北京地区高校研究生学术交流会——通信与信息技术会议论文集（上）[C];2006年

2 胡远锋;;数字签名原理浅析及其在网上银行的应用[A];2007北京地区高校研究生学术交流会通信与信息技术会议论文集（上册）[C];2008年

3 徐天岭;王景中;袁开国;杨义先;;基于USB-KEY的P2P保密通信研究与实现[A];中国电子学会第十五届信息论学术年会暨第一届全国网络编码学术年会论文集（上册）[C];2008年

4 王远敏;汪学明;;一种改进的含离线可信第三方多方不可否认协议[A];逻辑学及其应用研究——第四届全国逻辑系统、智能科学与信息科学学术会议论文集[C];2008年

5 王斌君;韦杨;巩荣;;B/S环境下反网络钓鱼双向身份鉴别系统的设计与实现[A];全国计算机安全学术交流会论文集·第二十五卷[C];2010年

6 王聪;王智学;;基于UML2.0的安全协议建模方法[A];江苏省系统工程学会第十一届学术年会论文集[C];2009年

7 徐梦茗;李斌;肖聪;;怎样用好AVISPA工具[A];第十一届保密通信与信息安全现状研讨会论文集[C];2009年

8 贺琦;鲁昌华;侯锋平;;基于指纹识别与数字签名的身份认证系统设计[A];计算机技术与应用进展·2007——全国第18届计算机技术与应用（CACIS）学术会议论文集[C];2007年

相关博士学位论文 前10条

1 杨元原;密码协议的安全性分析技术研究[D];西安电子科技大学;2011年

2 李向东;公平交换协议的形式化分析与设计[D];解放军信息工程大学;2009年

3 王惠斌;安全认证协议的设计与分析[D];解放军信息工程大学;2010年

4 陈莉;电子商务安全协议的设计与分析[D];解放军信息工程大学;2009年

5 刘益和;应用区域边界安全体系结构的模型研究[D];四川大学;2005年

6 肖迪;混沌理论在数字产品安全中的应用研究[D];重庆大学;2005年

7 王英龙;Ad Hoc网络路由协议安全性分析方法研究[D];山东大学;2005年

8 邢育红;公平交换协议分析方法研究[D];山东大学;2005年

9 王强华;基于公共信道信令模型的网格体系结构研究[D];西北大学;2006年

10 缪祥华;一种分析和设计安全协议的新逻辑[D];西南交通大学;2006年

相关硕士学位论文 前10条

1 毋晓英;基于串空间模型的安全协议分析与验证方法的研究[D];郑州大学;2010年

2 余磊;基于串空间模型的安全协议分析方法研究[D];淮北师范大学;2010年

3 程莹;网络安全协议的模型检测分析及验证系统[D];南昌大学;2010年

4 李长军;企业级复合式数据保护系统关键技术的研究[D];电子科技大学;2010年

5 鲁文静;异构无线融合网络中通用接入认证协议研究[D];解放军信息工程大学;2009年

6 马松;不可否认机制与时间戳服务系统研究[D];西安电子科技大学;2009年

7 尚艳萍;RIPC中数据压缩与安全通信技术的研究与实现[D];西安电子科技大学;2010年

8 姬国珍;基于Maude的安全协议的形式化分析[D];西安电子科技大学;2011年

9 秦好磊;基于树自动推理的安全协议自动化检测[D];西安电子科技大学;2011年

10 卢卫雄;基于IPSec的VPN网络及其SA实现的研究[D];北方工业大学;2011年

【相似文献】

相关期刊论文 前10条

1 余冬梅,边培泉,冯涛;安全协议中的形式化验证技术[J];微机发展;2003年11期

2 王忆;;基于面向特征编程范式的形式化验证技术的应用与研究[J];信息与电脑(理论版);2011年01期

3 杨泽民;范全润;;硬件设计的形式化验证技术[J];太原师范学院学报(自然科学版);2007年02期

4 叶俊;谭庆平;李暾;;面向特征编程范式的形式化验证技术研究综述[J];计算机工程与科学;2010年09期

5 周宏斌,黄连生,桑田;基于串空间的安全协议形式化验证模型及算法[J];计算机研究与发展;2003年02期

6 韩俊刚;硬件设计的形式化验证[J];计算机研究与发展;1991年11期

7 王彦本;;集成电路形式化验证方法研究[J];电子科技;2008年08期

8 张慧;郑超美;;安全协议的形式化验证方法概述[J];计算机安全;2007年01期

9 黄连生,王新兵,谢峰,杨克;安全协议形式化验证方法的比较与分析[J];计算机工程与应用;2001年14期

10 张博颖;;优先级顶协议的形式化验证[J];计算机仿真;2007年06期

相关会议论文 前2条

1 吴铃铃;周干民;何伟;高明伦;;IP软核的形式化验证[A];全国第十五届计算机科学与技术应用学术会议论文集[C];2003年

2 郭华;庄雷;;电子商务协议的形式化验证方法及FR验证实例[A];2005年全国理论计算机科学学术年会论文集[C];2005年

相关硕士学位论文 前8条

1 李小波;龙芯2号功能部件半形式化验证方法的研究与实现[D];首都师范大学;2006年

2 焦金良;基于多项式模型的高层次形式化验证[D];哈尔滨工程大学;2006年

3 张倩;基于可编程逻辑的硬件平台的设计与形式化验证[D];北京交通大学;2009年

4 张金磊;形式化验证技术在EDA软件开发中的应用[D];西安电子科技大学;2011年

5 马小龙;形式化验证在Office安全中的应用研究[D];中国人民解放军信息工程大学;2005年

6 张泽恩;基于GSTE中的符号仿真设计与实现[D];电子科技大学;2012年

7 林立;基于高阶逻辑系统HOL的数字硬件形式化验证[D];西安电子科技大学;2005年

8 谭力;基于情态演算的UML形式化验证与OCL约束自动生成研究[D];华东师范大学;2010年

，

本文编号：2538580