Security protocol's extended Horn logic model and its verification method

Based on analyzing and pointing out the limitations for constructing counter-examples of the security protocol's Horn logic model and its verification method proposed by Bruno Blanchet and Martin Abadi, the security protocol's extended Horn logic model and the modified-version verification method are presented such that the counter-examples are able to be constructed from them automatically. In the authors' verifier SPVT developed based on the functional programming language Objective Caml, these algorithms are implemented and their correctness are proved.