基于Spin/Promela的Woo-Lam协议安全性质高效验证

Efficiently Verify Security Properties of Woo-Lam Protocol with Spin/Promela

形式化方法是分析验证安全协议的重要技术之一。模型检测是用在形式化方法中实现形式化自动验证的重要手段。基于Promela语言,将P.Maggi和R.Sisto提出的建模方法扩展到建立包含三个合法主体和一个攻击者的复杂模型,枚举法和打表法同时被运用在求解攻击者模型需要表示的知识项过程中,提高了协议建模效率,保证了建模准确性。以Woo-Lam协议为例,运用Spin工具成功发现一个已知著名攻击。此通用方法适用于类似复杂协议形式化分析与验证。

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 .