中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 期刊论文
Title:
Formal analysis of TPM2.0 key management APIs
Author: Zhang, Qianying ; Zhao, Shijun ; Qin, Yu ; Feng, Dengguo
Keyword: Trusted computing ; TPM2.0 ; Security APIs ; Key management ; Secrecy ; Formal analysis
Source: CHINESE SCIENCE BULLETIN
Issued Date: 2014
Volume: 59, Issue:32, Pages:4210-4224
Indexed Type: SCI
Department: [Zhang, Qianying; Zhao, Shijun; Qin, Yu; Feng, Dengguo] Chinese Acad Sci, Inst Software, Trusted Comp & Informat Assurance Lab, Beijing 100190, Peoples R China.
Abstract: 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.
English Abstract: 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.
Language: 英语
WOS ID: WOS:000342451800006
Citation statistics:
Content Type: 期刊论文
URI: http://ir.iscas.ac.cn/handle/311060/16803
Appears in Collections:软件所图书馆_期刊论文

Files in This Item:

There are no files associated with this item.


Recommended Citation:
Zhang, Qianying,Zhao, Shijun,Qin, Yu,et al. Formal analysis of TPM2.0 key management APIs[J]. CHINESE SCIENCE BULLETIN,2014-01-01,59(32):4210-4224.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[Zhang, Qianying]'s Articles
[Zhao, Shijun]'s Articles
[Qin, Yu]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[Zhang, Qianying]‘s Articles
[Zhao, Shijun]‘s Articles
[Qin, Yu]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2019  中国科学院软件研究所 - Feedback
Powered by CSpace