Local abstract verification and refinement of security protocols
Ti Zhou, Mengjun Li, Zhoujun Li · 2008
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.