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

Model checking of trusted cryptographic module

作　　者：陈小峰[1] 冯登国[1] 

机构地区：[1]中国科学院软件研究所信息安全国家重点实验室,北京100190

出　　处：《通信学报》2010年第1期59-64,72,共7页Journal on Communications

基　　金：国家自然科学基金资助项目(60673083;60603017);国家重点基础研究发展计划("973"计划)基金资助项目(2007CB311202)~~

摘　　要：根据可信密码模块规范的非形式化描述,利用模型检测工具SPIN对可信密码模块安全性进行形式化分析,给出了可信密码模块形式化分析的基本框架,重点分析了AP授权协议和可信密码模块初始化子系统。指出了AP授权协议存在的缺陷,并给出了具体的改进措施;同时验证可信密码模块初始化子系统状态的一致性。The formal security analysis was given for the trusted cryptographic module according to the specification of the trusted cryptographic module using model checking tools. The flaws in the AP protocol were pointed and the solution was given. Meanwhile, the framework was proposed for analyzing the security property of the trusted cryptographic module using the model checking tools .

关 键 词：可信计算平台 可信密码模块 模型检测 

分 类 号：TP309[自动化与计算机技术—计算机系统结构]