Automatically Constructing Counter-Examples of Security Protocols Based on the Extended Horn Logic Model

It is very important to construct counter-examples of security protocols automatically, but there are few methods to do this work. Based on the extended Horn logic model and the corresponding verification method of security protocols, the solution strategies are presented, which are used to construct automatically intuitionistic counter-examples in protocols which break the security properties. Some important theorems are proved to make sure the correctness of these solution strategies. Based on this model, a series of algorithms are designed to construct counter-examples of security protocols automatically, the optimal methods of some main algorithms are given, and their complexities are analyzed in detail. These algorithms are implemented in the verifier SPVT which is developed in the functional programming language Objective Caml. The time complexities of these algorithms are proved to be linear theoretically. Finally, some classical security protocols are verified by SPVT which presents counter-examples automatically. Those results are also discussed and some counter-examples are analyzed. The results of experiments also show that these algortithms are linear. As the form of counter-examples is very similar to Alice-Bob notations, it is very convenient to read. Therefore, this formal method can be used by experts in all fields to check if there is a real counter-example in security protocols.