@inproceedings{ebb9d9c1c58f48d5b8191a89ac981ae7,
title = "Constraint abstraction in verification of security protocols",
abstract = "This paper incorporates time constraints in the Horn logic model, and this extended model can verify Wide-Mouthed-Frog protocol quickly. It discusses relations between the constraint system and Horn model, abstracts the constraint system, and gives the proofs of some propositions and theorems. We also give the algorithm about how to compute the abstract constraint, and analyze its complexity. As a case study we discuss the verification of Wide-Mouthed-Frog protocol whose attack can be found quickly in new model. Therefore, the method in this paper is very effective in verification of time sensitive security protocols. In the future, we will use this method to verify some complex protocols, such as Kerberos protocol etc.",
keywords = "Constraint system, Formal verification, Logic model, Security protocol, Time sensitive",
author = "Ti Zhou and Zhoujun Li and Mengjun Li and Huowang Chen",
year = "2008",
doi = "10.1007/978-3-540-69311-6\_27",
language = "英语",
isbn = "3540693106",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "252--263",
booktitle = "Frontiers in Algorithmics - Second International Workshop, FAW 2008, Proceedings",
note = "2nd International Frontiers in Algorithmics Workshop, FAW 2008 ; Conference date: 19-06-2008 Through 21-06-2008",
}