Formal analysis of TPM2.0 key management APIs
文献类型：期刊论文
| 作者 | Zhang, Qianying ; Zhao, Shijun ; Qin, Yu ; Feng, Dengguo |
| 刊名 | CHINESE SCIENCE BULLETIN
 |
| 出版日期 | 2014 |
| 卷号 | 59期号:32页码:4210-4224 |
| 关键词 | Trusted computing TPM2.0 Security APIs Key management Secrecy Formal analysis |
| ISSN号 | 1001-6538 |
| 中文摘要 | The trusted platform module (TPM), a system component implemented on physical resources, is designed to enable computers to achieve a higher level of security than the security level that it is possible to achieve by software alone. For this reason, the TPM provides a way to store cryptographic keys and other sensitive data in its memory, which is shielded from access by any entity other than the TPM. Users who want to use those keys and data to achieve some security goals are restricted to interact with the TPM through its APIs defined in the TPM specification. Therefore, whether the TPM can provide Protected Capabilities it claimed depends to a large extent on the security of its APIs. In this paper, we devise a formal model, which is accessible to a fully mechanized analysis, for the key management APIs in the TPM2.0 specification. We identify and formalize security properties of these APIs in our model and then successfully use the automated prover Tamarin to obtain the first mechanized analysis of them. The analysis shows that the key management subset of TPM APIs preserves the secrecy of non-duplicable keys for unbounded numbers of fresh keys and handles. The analysis also reports that the key duplication mechanism, used to duplicate a key between two hierarchies, is vulnerable to impersonation attacks, which enable an adversary to recover the duplicated key of the originating hierarchy or import his own key into the destination hierarchy. Aiming at avoiding these vulnerabilities, we propose an approach, which restricts the originating and destination TPMs to authenticate each other's identity during duplication. Then we formally demonstrate that our approach maintains the secrecy of duplicable keys when they are duplicated. |
| 英文摘要 | The trusted platform module (TPM), a system component implemented on physical resources, is designed to enable computers to achieve a higher level of security than the security level that it is possible to achieve by software alone. For this reason, the TPM provides a way to store cryptographic keys and other sensitive data in its memory, which is shielded from access by any entity other than the TPM. Users who want to use those keys and data to achieve some security goals are restricted to interact with the TPM through its APIs defined in the TPM specification. Therefore, whether the TPM can provide Protected Capabilities it claimed depends to a large extent on the security of its APIs. In this paper, we devise a formal model, which is accessible to a fully mechanized analysis, for the key management APIs in the TPM2.0 specification. We identify and formalize security properties of these APIs in our model and then successfully use the automated prover Tamarin to obtain the first mechanized analysis of them. The analysis shows that the key management subset of TPM APIs preserves the secrecy of non-duplicable keys for unbounded numbers of fresh keys and handles. The analysis also reports that the key duplication mechanism, used to duplicate a key between two hierarchies, is vulnerable to impersonation attacks, which enable an adversary to recover the duplicated key of the originating hierarchy or import his own key into the destination hierarchy. Aiming at avoiding these vulnerabilities, we propose an approach, which restricts the originating and destination TPMs to authenticate each other's identity during duplication. Then we formally demonstrate that our approach maintains the secrecy of duplicable keys when they are duplicated. |
| 收录类别 | SCI |
| 语种 | 英语 |
| WOS记录号 | WOS:000342451800006 |
| 公开日期 | 2014-12-16 |
| 源URL | [http://ir.iscas.ac.cn/handle/311060/16803]  |
| 专题 | 软件研究所_软件所图书馆_期刊论文 |
| 推荐引用方式 GB/T 7714 | Zhang, Qianying,Zhao, Shijun,Qin, Yu,et al. Formal analysis of TPM2.0 key management APIs[J]. CHINESE SCIENCE BULLETIN,2014,59(32):4210-4224. |
| APA | Zhang, Qianying,Zhao, Shijun,Qin, Yu,&Feng, Dengguo.(2014).Formal analysis of TPM2.0 key management APIs.CHINESE SCIENCE BULLETIN,59(32),4210-4224. |
| MLA | Zhang, Qianying,et al."Formal analysis of TPM2.0 key management APIs".CHINESE SCIENCE BULLETIN 59.32(2014):4210-4224. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。