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

Security Protocol Verification Based on Bounded Model Checking and Strand Space

作　　者：杨晋吉[1,2] 苏开乐[3] 肖茵茵[2] 李超明[2] 

机构地区：[1]华南师范大学计算机学院,广东广州510631 [2]中山大学计算机科学系,广东广州510275 [3]北京大学信息科学技术学院,北京100871

出　　处：《小型微型计算机系统》2010年第8期1484-1488,共5页Journal of Chinese Computer Systems

基　　金：国家杰出青年基金项目(60725207)资助;国家“九七三”重点基础研究发展计划项目(2010CB328103)资助;广东省自然科学基金项目(06023195)资助;广东省科技计划攻关项目(2007B010400068)资助

摘　　要：提出用BMC和串空间结合的方法对安全协议进行验证.首先是通过串空间的出测试理论先构造不安全协议的部分丛结构,通过该丛结构来约束协议运行的的规模和角色行为;然后用BMC对该丛结构进行建模,建立起对应的有限状态自动机和LTL验证规范,进行验证,有效减轻状态空间爆炸问题;利用不安全协议丛结构的特点,对BMC的下界进行优化.这种方式结合了模型检测和定理证明的优点,通过典型的安全协议的分析和实验,验证了本方法较传统的模型检测方法在验证安全协议时,验证效率提高明显.An approach for verifying security protocol with the combination of BMC and strand space formalism is presented.First,the part bundle structure of security protocol is designed through strand space theory,this bundle is very important to constrain the running size of the protocol and the behavior of the roles.Then,the bundle structure is modeled and verified by BMC.According to the bundle,the FSM is created in BMC and LTL specification is given.By the characteristic of this bundle,the optimized down bound of BMC is presented.This method takes advantage of both model checking and theorem proving.Analyses and verification experiments of several security protocols indicate that this approach is more efficient than traditional model checking technique when verifying the security protocols.

关 键 词：有界模型检测 串空间 协议 验证 NUSMV 

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