一种含时间因素的安全协议形式化分析方法

发布时间：2018-08-06 18:10

【摘要】：提出一种针对包含时间因素的安全协议的有色Petri(CPN)形式化分析方法,利用CPN Tools中的内置全局自动时钟标记,时间相关性质可通过仿真和生成状态图进行分析验证。基于这一方法,对著名的NS协议(简化版)建模,来分析验证与时间相关的安全属性。然后利用CPN Tools,采用CPN ML语言编写查询函数验证协议的AUT性质,从而发现协议的漏洞。应用分析结果表明方法有效,且操作简单容易理解。
[Abstract]:This paper presents a formal analysis method of colored Petri (CPN) for security protocols with time factors. By using the built-in global automatic clock tag in CPN Tools, the property of time correlation can be analyzed and verified by simulation and generation of state diagrams. Based on this method, the famous NS protocol (simplified version) is modeled to analyze the security properties related to time. Then, using CPN tools, we use CPN ML language to write query function to verify the AUT nature of the protocol, so as to discover the protocol vulnerabilities. The application results show that the method is effective and easy to understand.
【作者单位】： 华北科技学院计算机学院;中国科学院研究生院信息科学与工程学院;
【基金】：中国科学院研究生院院长基金项目(Y15102HN00)
【分类号】：TP393.08

【参考文献】

相关期刊论文 前3条

1 刘文琦;顾宏;;基于分层时间有色Petri网的支付协议公平性分析[J];电子与信息学报;2009年06期

2 苏桂平;孙莎;;一种基于有色Petri网的安全协议分析方法研究[J];微型机与应用;2011年15期

3 吴瑞龙;李陶深;;基于有色Petri网模型的安全协议检测方法[J];微电子学与计算机;2006年03期

【共引文献】

相关期刊论文 前3条

1 叶红;袁志祥;;SET协议的持卡人匿名性分析[J];安徽工业大学学报(自然科学版);2010年02期

2 陈家伟;王知衍;张艳青;;基于Petri网的流程挖掘算法设计与应用[J];计算机工程与设计;2010年10期

3 林宏刚;胡勇;;WAP环境下移动支付协议公平性分析[J];四川大学学报(工程科学版);2013年03期

相关博士学位论文 前1条

1 杨鹏;基于广义随机Petri网理论的SIP的研究[D];兰州理工大学;2009年

相关硕士学位论文 前7条

1 晁媛媛;基于分层思想的基本通信系统CPN建模[D];山东大学;2011年

2 郝天保;基于模糊时间Petri网的并行工作流模型研究[D];燕山大学;2011年

3 折建峰;WAP事务层协议的有色PETRI网建模与分析[D];武汉科技大学;2007年

4 吕波;IPv6环境下IKEv2的形式化分析及应用研究[D];贵州大学;2007年

5 刘烦;基于着色Petri网的发布/订阅系统的建模与分析[D];中国石油大学;2008年

6 张生财;SCTP关联管理的有色Petri网建模与分析[D];兰州理工大学;2009年

7 卢贝;颜色Petri网的电子商务协议形式化分析方法研究[D];燕山大学;2012年

【二级参考文献】

相关期刊论文 前8条

1 文静华;李祥;张焕国;梁敏;张梅;;基于ATL的公平电子商务协议形式化分析[J];电子与信息学报;2007年04期

2 怀进鹏,李先贤;密码协议的代数模型及其安全性[J];中国科学E辑:技术科学;2003年12期

3 刘道斌,郭莉,白硕;一种新的安全协议验证方法[J];计算机研究与发展;2003年10期

4 王彩芬,葛建华;一种分析电子商务协议的新方法[J];计算机学报;2004年04期

5 李梦君;李舟军;陈火旺;;安全协议的扩展Horn逻辑模型及其验证方法[J];计算机学报;2006年09期

6 周典萃 ,卿斯汉 ,周展飞;一种分析电子商务协议的新工具[J];软件学报;2001年09期

7 杜玉越,蒋昌俊;网上证券交易系统的时序Petri网描述及验证[J];软件学报;2002年08期

8 卿斯汉;一种电子商务协议形式化分析方法[J];软件学报;2005年10期

【相似文献】

相关期刊论文 前10条

1 刘晶;伏飞;肖军模;;Ad Hoc网络安全路由协议形式化分析模型[J];解放军理工大学学报(自然科学版);2008年03期

2 赵华伟,李大兴,秦静;一种时间相关的分析安全协议的扩展逻辑[J];计算机应用;2005年10期

3 吴建耀;张玉清;杨波;;SET支付协议的形式化分析与改进[J];计算机工程;2006年03期

4 刘晶;伏飞;肖军模;;扩展Meadows模型分析Ad Hoc网络路由协议安全性[J];应用科学学报;2008年03期

5 冯登国,范红;安全协议形式化分析理论与方法研究综述[J];中国科学院研究生院学报;2003年04期

6 李韶光,张险峰,秦志光;一个基于活体指纹的用户身份认证协议及其形式化分析[J];重庆邮电学院学报(自然科学版);2004年06期

7 范红,冯登国;一个非否认协议ZG的形式化分析[J];电子学报;2005年01期

8 罗志宏;朱思铭;;有色Petri网的一种密码协议建模分析[J];现代计算机;2006年02期

9 文静华;张梅;李祥;;一种新的密码协议分析方法及其应用[J];计算机应用;2006年05期

10 王惠斌;常青美;祝跃飞;;基于PDS的IKE安全协议形式化分析[J];河南师范大学学报(自然科学版);2007年03期

相关会议论文 前10条

1 刘家芬;周明天;;对安全协议重放攻击的分类研究(英文)[A];计算机技术与应用进展——全国第17届计算机科学与技术应用（CACIS）学术会议论文集（下册）[C];2006年

2 范锐;刘小辉;;企业实体构件动态演化模型[A];2009中国控制与决策会议论文集（3）[C];2009年

3 王焱;夏梦芹;曾家智;;CPN在可靠数据传输机制中的建模研究[A];系统仿真技术及其应用（第7卷）——'2005系统仿真技术及其应用学术交流会论文选编[C];2005年

4 周家浩;王建民;闻立杰;;基于CPN的工作流管理系统访问控制技术研究与实现[A];第二十二届中国数据库学术会议论文集（技术报告篇）[C];2005年

5 文静华;张梅;张焕国;;电子支付协议的博弈逻辑模型与形式化分析[A];2007年全国开放式分布与并行计算机学术会议论文集(上册)[C];2007年

6 林国璋;;博物馆的时间因素[A];2004年科技馆学术年会论文选编[C];2004年

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

8 柳芳;;浅谈《内经》中有关针灸时间因素的论述[A];第十三届针灸对机体功能的调节机制及针灸临床独特经验学术研讨会暨第三届经络分会委员会会议论文集[C];2008年

9 徐锐;;设计安全协议[A];第十八次全国计算机安全学术交流会论文集[C];2003年

10 张梅;文静华;张焕国;;基于ATL的电子商务协议建模与形式化分析[A];2009年全国开放式分布与并行计算机学术会议论文集(上册)[C];2009年

相关重要报纸文章 前10条

1 万春萍　何Z，

本文编号：2168564