Efficiently Verify Security Properties of Woo-Lam Protocol with Spin/Promela
XIAO Meihua
CHENG Daolei
HU Lei
Abstract：Formal method is one of the crucial technologies to analyze and verify the properties of security protocols . Model checking is a kind of significant means to realize automatic formal verification in formal methods .Based on Promela , the modeling method proposed by P .Maggi and R .Sisto is expanded to model the complex protocols including three legal principals and an attacker .The enumeration method and the tabulation method are synchronously utilized in solving process of knowledge elements which the attacker model needs .Our approach improves the efficiency and guarantees the accuracy of protocol modeling .Taking Woo-Lam protocol as an example ,a known famous attack has been found successfully by Spin . The general approach also can be applied to formal analysis and verification of similar security protocols .
Keywords：formal methodmodel checkingWoo-Lam protocolenumeration methodtabulation method
Publication Date：2014-10-01
Online Publishing Date：2025-08-15(First online date of this platform, not the publication date of the document)
Pages：6( 1768-1772,1928 )