Access Restriction

Author Wang, Weijin ♦ Qin, Yu ♦ Feng, Dengguo ♦ Chu, Xiaobo
Source CiteSeerX
Content type Text
File Format PDF
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Authorization Protocol ♦ Computational Model ♦ Full Version ♦ Automated Proof ♦ Predefined Set ♦ Tpm-resident Structure ♦ Trusted Plat-form Module ♦ Probabilistic Polynomial-time Calculus ♦ Sound Mechanized Proof ♦ Tool Cryptoverif ♦ Upper Bound ♦ Many Command
Abstract Abstract. 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.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article