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

Model-Checking Security Protocol with Propositional Projection Temporal Logic

针对无条件安全通信协议,特别是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.