Cryptology ePrint Archive: Report 2013/501

Type-Based Analysis of Protected Storage in the TPM (full version)

Jianxiong Shao and Dengguo Feng and Yu Qin

Abstract: The Trusted Platform Module (TPM) is designed to enable trustworthy computation and communication over open networks. The TPM provides a way to store cryptographic keys and other sensitive values in its shielded memory and act as \emph{Root of Trust for Storage} (RTS). The TPM interacts with applications via a predefined set of commands (an API). In this paper, we give an abstraction model for the TPM 2.0 specification concentrating on Protected Storage part. With identification and formalization of their secrecy properties, we devise a type system with asymmetric cryptographic primitives to statically enforce and prove their security.

Category / Keywords: cryptographic protocols / TPM, Trusted computing, Type system, API analysis

Original Publication (with minor differences): ICICS2013

Date: received 14 Aug 2013, last revised 15 Aug 2013

Contact author: shaojianxiong at tca iscas ac cn

Available format(s): PDF | BibTeX Citation

Version: 20130816:044154 (All versions of this report)

Short URL: ia.cr/2013/501

Discussion forum: Show discussion | Start new discussion