Automatic Verification for Later-Correspondence of Security Protocols.

Ensuring correspondence is very important and useful in designing security protocols. Previously, many research works focus on the verification of former-correspondence which means "if the protocol executes some event, then it must have executed some other events before". However, in some security protocols, it is also important to ensure the engagement of some events after an event happens. In this work, we propose a new property called later-correspondence, which is very useful for e-commerce protocols. The applied p-calculus is extended to specify the protocols. A simplified intruder model is proposed for modeling the intruder capabilities which includes the malicious behaviors of both protocol agents and intruders. The later-correspondence is verified based on the Labeled Transition System (LTS) using model checking. In order to avoid the states explosion, we limit the number of protocol sessions and reduce most of the useless messages from the intruder knowledge with message pattern filtering. We implement our method in a model checker PAT [23] and the verification results show that our method can verify later-correspondence in an effective way.