面向命题投影时序逻辑的安全协议模型检测  

Model-Checking Security Protocol with Propositional Projection Temporal Logic

作　　者：杨琛[1,2] 段振华[1] 王小兵[1,2] 

机构地区：[1]西安电子科技大学计算理论与技术研究所,西安710071 [2]武汉大学软件工程国家重点实验室,武汉430072

出　　处：《西安交通大学学报》2010年第8期30-35,共6页Journal of Xi'an Jiaotong University

基　　金：国家自然科学基金重大国际合作项目(60910004);国家自然科学基金资助项目(60873018);国家重点基础研究发展规划资助项目(2010CB328102);武汉大学软件工程国家重点实验室开放基金资助项目(SKLSE20080713);中央高校基本科研业务费专项资金资助项目(JY10000903004)

摘　　要：针对无条件安全通信协议,特别是Russian Cards协议的安全性验证问题,提出基于命题投影时序逻辑(PPTL)的模型检测方法.根据协议构造规则建立了Russian Cards协议的ProMeLa模型;利用chop算子将多个交互事件进行顺序复合,以表达协议所期望的通信序列;由projection算子定义了协议在该序列上的安全性质,再将该性质转为Never Claim语法结构并连同协议模型作为模型检测器SPIN的输入,以完成验证工作.验证结果表明,由协议规则构造的Russian Cards通信协议是安全可靠的,该方法也适用于一般的无条件安全通信协议的验证.A method of model-checking is proposed based on propositional projection temporal logic（PPTL）to verify the security of unconditional security communication protocols,in particular the Russian Cards protocols.The protocol model is built up in ProMeLa language according to the rules of constructing Russian Cards protocol that are given in our previous work.The security properties are defined by PPTL,that is,the chop operator is used to compose interactive events sequentially and to formalize the expected communication sequence,and the projection operator is employed to express the security properties over the sequence.Then the PPTL properties are transformed into Never Claim structures.The verification is done in a widely-used model checker-SPIN with the ProMeLa model and the Never Claim properties as the inputs.Experimental results show that Russian Cards protocols constructed using the protocol rules are safe and reliable.The model-checking method is also applicable in verifying ordinary unconditional security communication protocols.

关 键 词：模型检测 协议验证 时序逻辑 安全协议 

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