论文部分内容阅读
形式化方法是分析验证安全协议的重要技术之一。模型检测是用在形式化方法中实现形式化自动验证的重要手段。基于Promela语言,将P.Maggi和R.Sisto提出的建模方法扩展到建立包含三个合法主体和一个攻击者的复杂模型,枚举法和打表法同时被运用在求解攻击者模型需要表示的知识项过程中,提高了协议建模效率,保证了建模准确性。以Woo-Lam协议为例,运用Spin工具成功发现一个已知著名攻击。此通用方法适用于类似复杂协议形式化分析与验证。
Formal methods are one of the important techniques for analyzing and verifying security protocols. Model checking is an important method used to realize formal automatic verification in formal methods. Based on the Promela language, the modeling methods proposed by P. Maggi and R. Sisto are extended to build a complex model containing three legal entities and one attacker. Enumeration and tabulation methods are also applied to solve the attacker model. In the process of knowledge items, the efficiency of protocol modeling is improved and the modeling accuracy is guaranteed. Take the Woo-Lam protocol as an example, using the Spin tool to successfully discover a known-known attack. This generic method is suitable for formal analysis and verification of similar complex protocols.