Automated Proof for Authorization Protocols of TPM 2.0 in Computational Model
We present the first automated proof of the authorization protocols in TPM 2.0 in the computational model.The Trusted Plat form Module(TPM) is a chip that enables trust in computing platforms and achieves more security than software alone.The TPM interacts with a caller via a predefined set of commands.Many commands reference TPM-resident structures, and use of them may require authorization.The TPM will provide an acknowledgement once receiving an authoriza tion.This interact ensure the authentication of TPM and the caller.In this paper, we present a computationally sound mechanized proof for authorization protocols in the TPM 2.0.We model the authorization protocols using a probabilistic polynomial-time calculus and prove au thentication between the TPM and the caller with the aid of the tool CryptoVerif, which works in the computational model.In addition, the prover gives the upper bounds to break the authentication between them.
TPM Trusted Computing formal methods computational model authorization
Weijin Wang Yu Qin Dengguo Feng
Trusted Computing and Information Assurance Laboratory,Institute of Software,Chinese Academy of Sciences,Beijing,China
国际会议
福州
英文
144-158
2014-05-05（万方平台首次上网日期，不代表论文的发表时间）