一种形式化的可信平台模块应用编程接口安全性分析方法

摘要：

针对可信平台模块(TPM)应用编程接口(API)规范设计的安全性未得到有效验证,本文提出了一种形式化的安全性分析方法.具体内容包括:采用形式化模型定义应用编程接口、攻击者能力与安全目标;借助自动证明机实现了一种基于归结准则和定理证明的推理方法,在该方法中还集成了可执行状态判决机制,在一定程度上缓解了状态空间爆炸的问题.实验结果表明,可信平台模块密钥迁移功能的设计存在一定安全缺陷.

关键词：可信平台模块、安全性分析、应用编程接口、一阶逻辑

所属期刊栏目：56

分类号：TP309(计算技术、计算机技术)

资助基金：国家高技术研究发展计划863项目2007AA01Z411

在线出版日期：2011-01-11（万方平台首次上网日期，不代表论文的发表时间）

页码：446-450