基于模型检测的策略冲突检测方法

发布时间：2018-06-22 21:10

  本文选题：反例 + 模型检测　； 参考：《电子科技大学学报》2013年05期

【摘要】：提出一种基于模型校验的策略冲突检测新方法。首先通过形式化描述语言进行系统建模,采用时态逻辑表征策略冲突的系统属性,然后利用NuSMV模型检测器验证属性的可满足性,并根据模型检测器产生的反例轨迹追溯策略冲突点。该方法可提高策略冲突检测的效率。
[Abstract]:A new strategy conflict detection method based on model checking is proposed. Firstly, the system is modeled by formal description language, and the system attributes of policy conflict are represented by temporal logic. Then, NuSMV model detector is used to verify the satisfiability of attributes. According to the counter-example trajectory generated by the model detector, the conflict point of the strategy is traced back. This method can improve the efficiency of policy conflict detection.
【作者单位】： 北京理工大学机电学院;北京理工大学软件安全工程技术北京市重点实验室;北京理工大学软件学院;
【基金】：国家863项目(2009AA01Z433)
【分类号】：TP393.08

【参考文献】

相关期刊论文 前3条

1 姚键 ,茅兵 ,谢立;一种基于有向图模型的安全策略冲突检测方法[J];计算机研究与发展;2005年07期

2 李祥军;孟洛明;焦利;;网管系统策略冲突解决的结果中存在的问题及检测与解决方法[J];计算机研究与发展;2006年07期

3 程亮;张阳;;基于UML和模型检测的安全模型验证方法[J];计算机学报;2009年04期

相关博士学位论文 前1条

1 吴蓓;安全策略转换关键技术研究[D];解放军信息工程大学;2010年

【共引文献】

相关期刊论文 前10条

1 张屹;魏学业;何春明;;基于时间化UML的安全通信模型检测[J];电子测量与仪器学报;2010年10期

2 胡媛媛;;利用软集成设计实时网络程序框架[J];电子技术;2011年10期

3 李凤华;苏斢;史国振;马建峰;;访问控制模型研究进展及发展趋势[J];电子学报;2012年04期

4 谢琳;;Geopriv协议形式化分析与模型检测[J];计算机光盘软件与应用;2013年17期

5 任占阳;望育梅;张琳;;一种新的策略冲突解决方法的研究[J];信息通信;2010年01期

6 张涛;黄少滨;黄宏涛;吕天阳;刘刚;;一种UML状态图模型检测方法[J];哈尔滨工程大学学报;2011年08期

7 唐成华;余顺争;;基于特征的网络安全策略验证[J];计算机研究与发展;2009年11期

8 梅芳;刘衍珩;张旭利;古天野;王旺;;移动网络资源管理策略的动态冲突消解机制[J];吉林大学学报(工学版);2009年02期

9 倪俊;陈晓苏;刘辉宇;李劲;;网络安全策略求精一致性检测和冲突消解机制的研究[J];计算机科学;2011年02期

10 翟浩良;韩道军;李磊;;基于逻辑和辩论的安全策略一致性研究[J];计算机科学与探索;2012年04期

相关博士学位论文 前7条

1 焦素云;基于概念格的动态策略存取模型[D];吉林大学;2011年

2 张立勇;软件源代码安全分析研究[D];西安电子科技大学;2011年

3 皮建勇;分布式并行系统若干安全技术的研究[D];电子科技大学;2008年

4 梅芳;基于策略的移动网络自主管理机制研究[D];吉林大学;2010年

5 赵也非;动态UML子图的形式语义研究[D];华东师范大学;2010年

6 张涛;复杂信息系统模型的形式化验证方法研究[D];哈尔滨工程大学;2012年

7 李赤松;访问控制中授权一致性问题的研究[D];华中科技大学;2012年

相关硕士学位论文 前10条

1 韩冰;线性时序逻辑在失业保险审计中的应用研究[D];哈尔滨工程大学;2010年

2 朱耀强;网格安全策略冲突检测及其消解机制的研究[D];长春工业大学;2010年

3 潘国栋;基于CORBA的信息系统安全组件管理研究[D];西安电子科技大学;2009年

4 吕审;NuSMV模型检测的研究及应用[D];武汉理工大学;2011年

5 陈倩倩;基于实时UML对实时系统LTE无线通信系统信令子系统（RRC系统）建模[D];华东师范大学;2011年

6 李华;智能化通信网络综合管理技术[D];电子科技大学;2011年

7 李添翼;多策略支持下的策略冲突检测与消解研究[D];华中科技大学;2011年

8 晏鸿敏;基于UML和镜像策略的3G无线网络镜像技术研究[D];上海交通大学;2011年

9 吕飞;基于混合式P2P网络的NAT穿越技术的研究与应用[D];大连理工大学;2011年

10 彭洪德;四川建院学生资助管理系统的设计与实现[D];电子科技大学;2011年

【二级参考文献】

相关期刊论文 前10条

1 何再朗,田敬东,张毓森;策略冲突类型的细化及检测方法的改进[J];吉林大学学报(信息科学版);2005年03期

2 李莉,任秀丽,栾贵兴;基于策略的分布式网络管理系统[J];东北大学学报;2002年06期

3 易汉文;由合理路径阻抗推求区间出行阻抗[J];系统工程;1995年04期

4 何再朗,田敬东,张毓森;策略冲突分析、检测及解决方案[J];兰州理工大学学报;2005年05期

5 王震;袁兆山;;基于本体的数据集成冲突消解[J];合肥工业大学学报(自然科学版);2010年03期

6 陈冬松,潘成胜,俞承志,王光兴;一种基于策略的配置管理思想[J];火力与指挥控制;2003年05期

7 夏春和;魏玉娣;李肖坚;王海泉;何巍;;计算机网络防御策略描述语言研究[J];计算机研究与发展;2009年01期

8 梅芳;刘衍珩;张旭利;古天野;王旺;;移动网络资源管理策略的动态冲突消解机制[J];吉林大学学报(工学版);2009年02期

9 李祥军,邱雪松,孟洛明;基于策略的网管中策略条件“或”运算的问题及解决方法[J];计算机工程与应用;2005年12期

10 黄俊;韩玲莉;;IPSec策略冲突发现形式化技术的研究[J];计算机工程与应用;2007年06期

相关博士学位论文 前1条

1 郎风华;基于人工智能理论的网络安全管理关键技术的研究[D];北京邮电大学;2008年

相关硕士学位论文 前4条

1 亢嵛;基于多层策略网络管理系统研究[D];中南大学;2005年

2 田涛;基于防火墙的企业网络安全策略及实现技术研究[D];中国科学院研究生院（计算技术研究所）;2004年

3 王柏昀;面向多主体的政策描述规范及冲突研究[D];湖南大学;2009年

4 王永亮;网络安全设备策略冲突检测与消解技术研究[D];解放军信息工程大学;2008年

【相似文献】

相关期刊论文 前10条

1 李卫民;徐炳雪;;基于NuSMV的攻击图模型生成技术研究[J];硅谷;2010年19期

2 周立青;杨晋吉;;乐观合同签订协议的模型检测分析[J];计算机工程;2011年07期

3 高昀;;信息系统的可生存性建模与分析研究[J];甘肃科技;2010年21期

4 林璇;;模型检测方法在入侵检测中的应用研究[J];现代计算机(专业版);2009年02期

5 徐有福;文伟平;万正苏;;基于漏洞模型检测的安全漏洞挖掘方法研究[J];信息网络安全;2011年08期

6 吉猛;胡克瑾;;基于模型检测的电子商务鉴证技术[J];陕西师范大学学报(自然科学版);2006年04期

7 李忠慧;张广泉;;基于UPPAAL的NS密码协议模型检测分析[J];重庆师范大学学报(自然科学版);2009年04期

8 杨晋吉,苏开乐;电子商务中安全协议的验证方法[J];计算机工程与应用;2003年19期

9 刘芳;魏昭;董荣胜;;基于SPIN的SAS协议和NS公钥协议分析[J];广西科学院学报;2008年04期

10 陈妍;唐成华;吴丹;;基于模型检测的工作流访问控制策略验证[J];计算机应用研究;2010年02期

相关会议论文 前7条

1 刘芳;魏昭;董荣胜;;基于SPIN的协议分析技术研究[A];广西计算机学会2008年年会论文集[C];2008年

2 肖美华;邓宸芳;马小薏;薛锦云;江耘;;网络安全认证协议形式化分析[A];第二十次全国计算机安全学术交流会论文集[C];2005年

3 孙守卿;李廉;章超;李彩虹;;基于模型检测工具SPIN的安全协议形式化分析[A];2005年全国理论计算机科学学术年会论文集[C];2005年

4 谢鸿波;周明天;;安全协议的形式化技术:述评[A];’2004计算机应用技术交流会议论文集[C];2004年

5 奚琪;王清贤;曾勇军;;恶意代码检测技术综述[A];计算机研究新进展（2010）——河南省计算机学会2010年学术年会论文集[C];2010年

6 余兴超;马争先;王玉斌;董荣胜;;基于UPPAAL的简单网络支付协议形式化验证[A];广西计算机学会2010年学术年会论文集[C];2010年

7 刘艳芳;丁帅;李建欣;张毅;;一种基于攻击树的网络攻击路径生成方法[A];全国第20届计算机技术与应用学术会议（CACIS·2009）暨全国第1届安全关键技术与应用学术会议论文集（上册）[C];2009年

相关博士学位论文 前10条

1 朱维军;时间区间时序逻辑模型检测：理论、算法及应用[D];西安电子科技大学;2011年

2 张玉清;计算机通信网安全协议的分析研究[D];西安电子科技大学;2000年

3 文静华;电子商务协议形式化方法及模型检测技术的研究与应用[D];贵州大学;2006年

4 陈靖;带实时的传值与移动系统研究[D];中国科学院研究生院（软件研究所）;2003年

5 门鹏;基于Petri网的Web服务组合相关技术研究[D];西安电子科技大学;2009年

6 范红;安全协议形式化分析理论与方法[D];中国人民解放军信息工程大学;2003年

7 王小兵;面向对象MSVL语言及其在组合Web服务验证中的应用[D];西安电子科技大学;2009年

8 宋波;Web应用交互的建模和测试用例生成[D];上海大学;2010年

9 龙士工;串空间理论及其在安全协议分析中的应用研究[D];贵州大学;2007年

10 傅朝阳;面向实时任务求解的自治服务协同模型、形式语义及其验证[D];浙江大学;2010年

相关硕士学位论文 前10条

1 袁建廷;鉴别协议的分析研究[D];西安电子科技大学;2008年

2 高丹丹;无线认证协议的模型检测与分析研究[D];长春理工大学;2010年

3 刘学锋;安全协议形式化分析及其应用[D];湘潭大学;2004年

4 吴建耀;电子商务安全协议的形式化分析技术研究[D];西安电子科技大学;2005年

5 吴瑞龙;一种基于有色Petri网模型的安全协议检测技术的研究[D];广西大学;2005年

6 邓保华;动态Web服务组合中业务流程建模环境的研究与实现[D];国防科学技术大学;2005年

7 刘秀英;计算机通信网安全协议形式化分析研究[D];西安电子科技大学;2004年

8 黄瑛;SET协议支付过程分析及模型检测[D];贵州大学;2006年

9 阮小黎;基于模型检测的C语言安全信息流研究[D];清华大学;2007年

10 党继胜;基于SVO逻辑的电子商务协议形式化分析与研究[D];贵州大学;2007年

，

本文编号：2054236