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

作     者：杨飏 张焕国 张帆 徐士伟 YANG Yang;ZHANG Huanguo;ZHANG Fan;XU Shiwei

作者机构：武汉大学计算机学院湖北武汉430072 武汉大学软件工程国家重点实验室湖北武汉430072 空天信息安全与可信计算教育部重点实验室湖北武汉430072 

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

出 版 物：《武汉大学学报（理学版）》 (Journal of Wuhan University:Natural Science Edition)

年 卷 期：2010年第56卷第4期

页      码：446-450页

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

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

学科分类：08[工学] 0839[0839] 081201[081201] 0812[工学-测绘类] 

核心收录：

D　O　I：10.14188/j.1671-8836.2010.04.020

馆 藏 号：203333562...