TY - GEN
T1 - SPVT-II
T2 - 4th International Conference on Information Security and Cryptology, Inscrypt 2008
AU - Li, Meng Jun
AU - Zhou, Ti
AU - Li, Zhou Jun
PY - 2009
Y1 - 2009
N2 - SPVT-II is a security protocol verifier based on logic programming, in which an accurate verification approach and an abstract verification approach are combined by a non-termination prediction algorithm. The prediction algorithm predicts non-termination of the solved-form fixpoint of the logic program model of security protocols. In SPVT-II, if the fixpoint is predicted non-termination, then the abstract approach is used to verify protocols, otherwise the accurate approach is used. The combined approach inherits the efficiency of the accurate approach for verifying those security protocols whose fixpoint terminates, and in the abstract-refinement iteration verification framework, the combined approach can be used to incrementally verify security protocols whose fixpoint is predicted non-termination. And in SPVTII, the non-termination prediction of fixpoint, verification, constructing counterexamples and refinement are all implemented mechanically. The experiment results demonstrate the practicality of our verifier.
AB - SPVT-II is a security protocol verifier based on logic programming, in which an accurate verification approach and an abstract verification approach are combined by a non-termination prediction algorithm. The prediction algorithm predicts non-termination of the solved-form fixpoint of the logic program model of security protocols. In SPVT-II, if the fixpoint is predicted non-termination, then the abstract approach is used to verify protocols, otherwise the accurate approach is used. The combined approach inherits the efficiency of the accurate approach for verifying those security protocols whose fixpoint terminates, and in the abstract-refinement iteration verification framework, the combined approach can be used to incrementally verify security protocols whose fixpoint is predicted non-termination. And in SPVTII, the non-termination prediction of fixpoint, verification, constructing counterexamples and refinement are all implemented mechanically. The experiment results demonstrate the practicality of our verifier.
KW - Abstract and refinement
KW - Non-termination characterization and prediction
KW - Security protocol
UR - https://www.scopus.com/pages/publications/67650162676
U2 - 10.1007/978-3-642-01440-6_12
DO - 10.1007/978-3-642-01440-6_12
M3 - 会议稿件
AN - SCOPUS:67650162676
SN - 9783642014390
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 125
EP - 140
BT - Information Security and Cryptology - 4th International Conference, Inscrypt 2008, Revised Selected Papers
Y2 - 14 December 2008 through 17 December 2008
ER -