An Improved and Efficient Tool for Analyzing Industrial Security Protocols

Formal methods and automatic tools are always necessary for analyzing security protocols, and model checking has become a hot spot of research for its ability of verifying finite-state concurrent system automatically. In this paper, we propose a model of security protocols based on MSR (multi-set rewriting), coupled with PLTL describing security properties. Based on the model, a series of key automatic analysis algorithms close to the implementation are designed for our own tool. By using the tool, we illustrate the methodpsilas effectiveness with some typical protocols and give the experimental results.