可信密码模块的模型检测分析

被引：3

作者：

陈小峰

冯登国

机构：

[1] 中国科学院软件研究所信息安全国家重点实验室

来源：

关键词：

可信计算平台; 可信密码模块; 模型检测;

D O I：

暂无

中图分类号：

TP393.08 [];

学科分类号：

0839 ; 1402 ;

摘要：

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

引用

页码：59 / 64+72 +72

页数：7