安全协议UML模型的SPIN分析

Analysis for UML Model of Security Protocols Using SPIN

统一建模语言(UML)是设计和建模安全协议的常用方法,但UML缺少精确的语义,不能对协议模型作进一步分析和验证;Promela是一种具有精确语义的形式化语言,通过Promela规范给协议的UML模型赋予精确语义可以结合两者的优势,提出一种将安全协议UML模型转换成Promela规范的方法,定义了转换规则实现模型间的转换,实例表明该方法的可行性。

Unified Modeling Language （ protocol. But it ＇ s lack of precise semantics, UML） is a commonly used method in designing and modeling security which leads to the weakness in analyzing and validating UML models. Promela is a formal language with precise semantics. The advantages of these two languages can be combined per- fectly when the former is endowed with the precise semantics from the latter. A method of translating UML model to Promela specification is proposed,which provides the transform rules, and shows the feasibility with case study.