@inproceedings{58e10e374cb14ad7b726ceaf89bdf96a,
title = "Local abstract verification and refinement of security protocols",
abstract = "The verification problem for security protocols is undecidable, but it is feasible to verify protocols by abstract interpretation. This paper presents a method based on local abstraction and refinement for verifying security protocols terminably. Local abstraction produces a safe approximation of the security protocol, modeled as a set of Horn logic rules. Refinement removes false attacks introduced by local abstraction. In contrast with methods based on global abstraction, our method abstracts only certain rules that can lead to non-termination when computing fixpoints, that is, it does not abstract all rules. We implement this method in a verification tool SPVT and are able to verify well-known protocols. Moreover, our experiments indicate that local abstraction is less costly than global abstraction.",
keywords = "Abstraction, Refinement, Security protocols, Verification",
author = "Ti Zhou and Mengjun Li and Zhoujun Li",
year = "2008",
doi = "10.1145/1456396.1456399",
language = "英语",
isbn = "9781605582887",
series = "Proceedings of the ACM Conference on Computer and Communications Security",
pages = "21--29",
booktitle = "Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering, FMSE'08,Co-located with the 15th ACM Computer and Communications Security Conference, CCS'08",
note = "6th ACM Workshop on Formal Methods in Security Engineering, FMSE'08, Co-located with the 15th ACM Computer and Communications Security Conference, CCS'08 ; Conference date: 27-10-2008 Through 31-10-2008",
}