Formal Analysis of Trusted Platform Module Commands for Compromising User Key

作     者：Qin Yu Zhao Shijun Zhang Qianying 

作者机构：Institute of SoftwareChinese Academy of ScienceBeijing 100190P.R.China 

出 版 物：《China Communications》 (中国通信（英文版）)

年 卷 期：2012年第9卷第10期

页      面：91-102页

核心收录：

学科分类：0810[工学-信息与通信工程] 0808[工学-电气工程] 0809[工学-电子科学与技术（可授工学、理学学位）] 08[工学] 0839[工学-网络空间安全] 081201[工学-计算机系统结构] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

基　　金：This paper was supported by the National Natural Science Foundation of China under Grants No.91118006, No. 61202414 the Knowledge Innovation Project of Chinese Academy of Science under Grant No. ISCAS2009-DR14. 

主　　题：计算平台 用户 命令 形式分析 模块 信任 密钥管理 TPM 

摘      要：The Trusted Platform Module (TPM) is a dedicated hardware chip designed to provide a higher level of security for computing platform. All TPM functionalities are implemented in TPM commands to achieve specific security goals. We attempt to analyze the security properties of these commands, especially the key management API. Our study utilizes applied pi calculus to formalize the commands and determine how their security properties affect TPM key management. The attacker is assumed to call TPM commands without bounds and without knowing the TPM root key, expecting to obtain or replace the user key. The analysis goal in our study is to guarantee the corresponding property of API execution and the integrity of API data. We analyze the security properties of TPM commands with a process reduction method, identify the key-handle hijack attack on a TPM newly created key, and propose reasonable solutions to solve the problem. Then, we conduct an experiment involving a key-handle attack, which successfully replaces a user key with an attacker s key using malicious TPM software. This paper discloses the weakness of the relationship between the key handle and the key object. After the TPM software stack is compromised, the attacker can launch a key-handle attack to obtain the user key and even break into the whole storage tree of user keys.