Formal analysis of HMAC authorisation in the TPM2.0 specification

Formal analysis of HMAC authorisation in the TPM2.0 specification

For access to this article, please select a purchase option:

Buy article PDF
(plus tax if applicable)
Buy Knowledge Pack
10 articles for £75.00
(plus taxes if applicable)

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Your details
Why are you recommending this title?
Select reason:
IET Information Security — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

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.


    1. 1)
      • 1. Trusted Computing Group, available at
    2. 2)
      • 2. Trusted Computing Group: ‘TPM Specification version 1.2. Parts 1–3, revision’, available at
    3. 3)
      • 3. Bruschi, D., Cavallaro, L., Lanzi, A., et al: ‘Replay attack in TCG specification and solution’. Proc. of ACSAC 2005, December 2005, vol. 10, pp. 127137.
    4. 4)
      • 4. Chen, L., Ryan, M.: ‘Attack, solution and verification for shared authorisation data in TCG TPM’. Formal Aspects in Security and Trust, 2010 (LNCS, 5983), pp. 201216.
    5. 5)
      • 5. Chen, L., Ryan, M.: ‘Offline dictionary attack on TCG TPM weak authorisation data, and solution’, in Gawrock, D., Reimer, H., Sadeghi, A.-R., et al, (Eds.): ‘Future of trust in computing’ (Vieweg Teubner, 2009), pp. 193196.
    6. 6)
      • 6. Delaune, S., Kremer, S., Ryan, M., et al: ‘A formal analysis of authentication in the TPM’. Formal Aspects of Security and Trust, 2011 (LNCS, 6561), pp. 111125.
    7. 7)
      • 7. Gurgens, S., Rudolph, C., Scheuermann, D., et al: ‘Security evaluation of scenarios based on the TCG's TPM specification’. Computer Security–ESORICS 2007, 2007 (LNCS, 4734), pp. 438453.
    8. 8)
      • 8. Delaune, S., Kremer, S., Ryan, M.D., et al: ‘Formal analysis of protocols based on TPM state registers’. Proc. of the 2011 IEEE 24th Computer Security Foundations Symp., 2011, pp. 6680.
    9. 9)
      • 9. Trusted Computing Group: ‘TPM Specification version 2.0. revision 01.16. Parts 1–4’, available at
    10. 10)
      • 10. ISO/IEC 11889-1:2015: ‘Information technology – trusted platform module library – part 1: Architecture’, 2015.
    11. 11)
      • 11. Arapinis, M., Liu, J., Ritter, E., et al: ‘Stateful applied pi calculus’. Principles of Security and Trust, 2014 (LNCS, 8414), pp. 2241.
    12. 12)
      • 12. Kremer, S., Künnemann, R.: ‘Automated analysis of security protocols with global state’. Proc. of the 2014 IEEE Symp. Security and Privacy, 2014, pp. 163178, available at
    13. 13)
      • 13. Schmidt, B., Meier, S., Cremers, C., et al: ‘Automated analysis of Diffie-Hellman protocols and advanced security properties’. Proc. of the 2012 IEEE 25th Computer Security Foundations Symp., 2012, pp. 7894.
    14. 14)
      • 14. Chen, L., Li, J.: ‘Flexible and scalable digital signatures in TPM 2.0’. Proc. of the 2013 ACM SIGSAC Conf. Computer and Communications Security, 2013, pp. 3748.
    15. 15)
      • 15. Xi, L., Yang, K., Zhang, Z., et al: ‘DAA-related APIs in TPM 2.0 revisited’. 7th Int. Conf., Trust and Trustworthy Computing, 2014 (LNCS, 8564), pp. 118.
    16. 16)
      • 16. Shao, J., Feng, D., Qin, Y.: ‘Type-based analysis of protected storage in the TPM’. Int. Conf., Information and Communications Security, 2013 (LNCS, 8233), pp. 135150.
    17. 17)
      • 17. Zhang, Q., Zhao, S., Qin, Y., et al: ‘Formal analysis of TPM2.0 key management APIs’, Chin. Sci. Bull., 2014, 59, (32), pp. 42104224.
    18. 18)
      • 18. Shao, J., Qin, Y., Feng, D., et al: ‘Formal analysis of enhanced authorization in the TPM 2.0’. Proc. of the 10th ACM Symp. Information, Computer and Communications Security, 2015, pp. 273284.
    19. 19)
      • 19. Wang, W., Qin, Y., Feng, D.: ‘Automated proof for authorization protocols of TPM 2.0 in computational model’. Information Security Practice and Experience, 2014 (LNCS, 8434), pp. 144158.
    20. 20)
      • 20. Yu, F., Zhang, H., Zhao, B., et al: ‘A formal analysis of trusted platform module 2.0 hash-based message authentication code authorization under digital rights management scenario’, Secur. Commun. Netw., 2016, 9, (15), pp. 28022815.
    21. 21)
      • 21. Abadi, M., Blanchet, B.: ‘Analyzing security protocols with secrecy types and logic programs’. 29th Annual ACM SIGPLAN – SIGACT Symp. Principles of Programming Languages (POPL 2002), Portland, Oregon, January 2002, pp. 3344.
    22. 22)
      • 22. TPM2-HBA-formal-verification, available at

Related content

This is a required field
Please enter a valid email address