一种基于SPIN的安全协议形式化验证方法

下载PDF

导出

摘要基于形式化的验证方法是提高软件系统质量以及保证安全攸关系统安全性和可靠性的有效方法。本文提出了一种基于SPIN的模型检测方法,该方法通过Dolev-Yao模型来描述协议系统及攻击者,通过LTL公式对待验证属性进行形式化规约。通过运用这种验证方法以及模型检测器SPIN找到了一种不满足待验证属性的情况即找到了一种针对协议的攻击,说明了这种方法的在实际中可以有效的发现协议的缺陷,而且可方便地用于其它网络安全协议验证。

作者刘虹

机构地区河北省张家口市阳原县华原市政工程有限公司

出处《电子技术与软件工程》 2013年第16期247-248,共2页 ELECTRONIC TECHNOLOGY & SOFTWARE ENGINEERING

关键词安全协议形式化方法模型检测 SPIN Pmmda

分类号 TP309 [自动化与计算机技术—计算机系统结构]

引文网络
相关文献

1梅宏,申峻嵘.软件体系结构研究进展[J].软件学报,2006,17(6):1257-1275. 被引量：143
2付江.探究架构方法论窭践之路[J].程序员,2011(9):82-83.
3马长捷,马晓云,袁野.浅析提高信息系统软件测试质量的途径[J].国防技术基础,2009(5):29-31.
4罗敏,方琳,施炜利.基于小系统理论的简化SET协议[J].计算机与现代化,2014(12):97-102.
5赵晓凡,周清雷,赵东明.基于线性时态逻辑的Petri网模型检测研究[J].微计算机信息,2009,25(3):100-101. 被引量：2
6肖云华.AOP技术辅助构件测试的应用研究[J].洛阳师范学院学报,2007,26(2):79-82.
7Eight Days a Week——Yao Jui-chung Solo Exhibition[J].China's Foreign Trade,2017(1):56-56.
8陈平,池同柱.UML模型测试策略及在软件测试中的应用[J].微计算机信息,2008(3):287-289. 被引量：1
9李宣东,刘超,毛晓光.安全攸关软件系统建模与验证专题前言[J].软件学报,2015,26(2):179-180. 被引量：1
10章甫源,戚正伟.基于D3S的分布式系统监控技术[J].微型电脑应用,2009,25(2):28-30.

电子技术与软件工程

2013年第16期

浏览历史

内容加载中请稍等...

一种基于SPIN的安全协议形式化验证方法

相关作者

相关机构

相关主题

浏览历史