UML是一种通用的面向对象建模语言，具有很强的描述能力和良好的扩展机制，但UML缺少精确的语义，不能对UML模型作进一步分析和验证。形式化方法具有精确的数学语义和自动化验证工具的支持，可以对软件规范进行严格的分析和验证，但形式化方法存在难以设计大型软件，直接用形式化规范对系统建模难度大等缺点。为保证安全协议设计的正确性，在早期的时候发现可能存在的错误，对协议的UML模型进行形式化验证很有必要。本文试图结合面向对象和形式化方法的优点，提出了一种将安全协议的UML模型转换成PROMELA规范的方法。首先选取UML的包括类图、序列图和状态图的核心子集来建模安全协议，然后定义了该UML子集到PROMELA语言的转换规则，根据规则将它自动转换成PROMELA规范，再调用模型检测器SPIN进行分析。该方法避免了直接使用形式化的PROMELA语言对协议建模，降低了分析协议的难度和出错的可能，具有较高的分析可靠性和效率：该原型系统经进一步完善后，可作为以网络认证协议为核心的网络通信系统安全性的有效分析评测工具。