Model-Checking Security Protocol with Propositional Projection Temporal Logic
Yang Chen · Xi'an Jiaotong Daxue xuebao · 2010
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.