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

被引：1

作者：

杨飏 ^{[1
]}

张焕国 ^{[1
,2
,3
]}

张帆 ^{[1
]}

徐士伟 ^{[1
]}

机构：

[1] 武汉大学计算机学院

[2] 武汉大学软件工程国家重点实验室

[3] 空天信息安全与可信计算教育部重点实验室

来源：

武汉大学学报(理学版) | 2010年 / 56卷 / 04期

关键词：

可信平台模块; 安全性分析; 应用编程接口; 一阶逻辑;

D O I：

10.14188/j.1671-8836.2010.04.020

中图分类号：

TP309 [安全保密];

学科分类号：

081201 ; 0839 ; 1402 ;

摘要：

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

引用

页码：446 / 450

页数：5