A dynamic approach on quickly predicting non-termination of logic program of security protocol

Based on the dynamic approach to characterizing termination of generic logic program, a dynamic approach to characterizing termination of solved-form fixpoint is researched in this paper, and a sufficient condition of non-termination of solved-form fixpoint of the extended Horn logic model of security protocol is presented. Based on this condition, an approach is represented to predict non-termination of computation of solved-form fixpoint. This approach can predict the non-termination of computing fixpoint by checking new generated rules, and localize the solved-form rules in the extended Horn logic model which cause infinite computations of solved-form fixpoint. The non-termination prediction results will provide the criteria for choosing different verification methods of security protocols, such as accurate methods and abstract methods. The experiment results show the effectiveness of the prediction algorithms.