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

作者：杨飏 张焕国 张帆 徐士伟可信平台模块安全性分析应用编程接口一阶逻辑

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

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社