摘要： 根据可信密码模块规范的非形式化描述，利用模型检测工具SPIN对可信密码模块安全性进行形式化分析，给出了可信密码模块形式化分析的基本框架，重点分析了AP授权协议和可信密码模块初始化子系统。指出了AP授权协议存在的缺陷，并给出了具体的改进措施；同时验证可信密码模块初始化子系统状态的一致性。