有界模型检测和串空间模型相结合的安全协议验证

CORC > 北京大学 > 信息科学技术学院

	有界模型检测和串空间模型相结合的安全协议验证; Security Protocol Verification Based on Bounded Model Checking and Strand Space
	杨晋吉 ; 苏开乐 ; 肖茵茵 ; 李超明
刊名	小型微型计算机系统
	2010
关键词	有界模型检测串空间协议验证 NuSMV
英文摘要	提出用BMC和串空间结合的方法对安全协议进行验证.首先是通过串空间的出测试理论先构造不安全协议的部分丛结构,通过该丛结构来约束协议运行的的规模和角色行为;然后用BMC对该丛结构进行建模,建立起对应的有限状态自动机和LTL验证规范,进行验证,有效减轻状态空间爆炸问题;利用不安全协议丛结构的特点,对BMC的下界进行优化.这种方式结合了模型检测和定理证明的优点,通过典型的安全协议的分析和实验,验证了本方法较传统的模型检测方法在验证安全协议时,验证效率提高明显.; 国家杰出青年基金; 国家"九七三"重点基础研究发展计划项目; 广东省自然科学基金; 广东省科技计划攻关项目; 中文核心期刊要目总览(PKU); 中国科技核心期刊(ISTIC); 中国科学引文数据库(CSCD); 0; 8; 1484-1488; 31
语种	中文
内容类型	期刊论文
源URL	[http://ir.pku.edu.cn/handle/20.500.11897/250599]
专题	信息科学技术学院
推荐引用方式 GB/T 7714	杨晋吉,苏开乐,肖茵茵,等. 有界模型检测和串空间模型相结合的安全协议验证, Security Protocol Verification Based on Bounded Model Checking and Strand Space[J]. 小型微型计算机系统,2010.
APA	杨晋吉,苏开乐,肖茵茵,&李超明.(2010).有界模型检测和串空间模型相结合的安全协议验证.小型微型计算机系统.
MLA	杨晋吉,et al."有界模型检测和串空间模型相结合的安全协议验证".小型微型计算机系统 (2010).