%0 Electronic Article %A Jianxiong Shao %A Yu Qin %A Dengguo Feng %K TPM protected storage %K trusted platform module %K object authorisation value %K TPM2.0 specification %K HMAC authorisation %K ISO standard %K session-bound secret value %K hash message authentication code authorisation mechanism %K SAPIC tool %K encryption mechanisms %K tamarin prover %K TPM-resident key object %K formal analysis %K authValue %K sessionKey %K session-based authorisation mechanism %X The Trusted Platform Module (TPM) is a system component that provides a hardware-based approach to establish trust in a platform. The latest TPM2.0 specification was accepted as the ISO standard in 2015. It offers functionality for key management by storing keys into the TPM's protected storage. The access to the TPM-resident key object is protected by the session-based authorisation mechanism. This mechanism is keyed to the object's authorisation value known as authValue and the session-bound secret value known as sessionKey. The new authValue introduced into the TPM is protected by the session-based encryption mechanism, which is also keyed on the sessionKey. In the authors’ study, they conduct a formal analysis of the TPM2.0 HMAC (hash message authentication code) authorisation mechanism used in the key management. They first use the stateful applied π calculus to formalise the session-based HMAC authorisation and encryption mechanisms in a model of TPM2.0 API commands. They propose a threat model to formalise the secrecy and authentication properties. Then they discuss several attacking scenarios in practice where the sessionKey could be disclosed. They also instantiate their threat model according to specific attacking scenarios. By using the SAPIC tool and the tamarin prover, they automatically give out the analysis results of their models. %@ 1751-8709 %T Formal analysis of HMAC authorisation in the TPM2.0 specification %B IET Information Security %D March 2018 %V 12 %N 2 %P 133-140 %I Institution of Engineering and Technology %U https://digital-library.theiet.org/;jsessionid=kau8ly5f8p5f.x-iet-live-01content/journals/10.1049/iet-ifs.2016.0005 %G EN