Your browser does not support JavaScript!
http://iet.metastore.ingenta.com
1887

access icon free Formal analysis of HMAC authorisation in the TPM2.0 specification

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.

References

    1. 1)
      • 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.
    2. 2)
      • 2. Trusted Computing Group: ‘TPM Specification version 1.2. Parts 1–3, revision’, available at http://www.trustedcomputinggroup.org/resources/tpm_main_specification.
    3. 3)
      • 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 http://sapic.gforge.inria.fr/.
    4. 4)
      • 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.
    5. 5)
      • 22. TPM2-HBA-formal-verification, available at https://github.com/sjxzmc/TPM2-HBA-formal-verification.
    6. 6)
      • 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.
    7. 7)
      • 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.
    8. 8)
      • 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.
    9. 9)
      • 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.
    10. 10)
      • 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.
    11. 11)
      • 10. ISO/IEC 11889-1:2015: ‘Information technology – trusted platform module library – part 1: Architecture’, 2015.
    12. 12)
      • 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.
    13. 13)
      • 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.
    14. 14)
      • 9. Trusted Computing Group: ‘TPM Specification version 2.0. revision 01.16. Parts 1–4’, available at https://www.trustedcomputinggroup.org/resources/tpm_library_specification.
    15. 15)
      • 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.
    16. 16)
      • 1. Trusted Computing Group, available at http://www.trustedcomputinggroup.org.
    17. 17)
      • 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.
    18. 18)
      • 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.
    19. 19)
      • 11. Arapinis, M., Liu, J., Ritter, E., et al: ‘Stateful applied pi calculus’. Principles of Security and Trust, 2014 (LNCS, 8414), pp. 2241.
    20. 20)
      • 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.
    21. 21)
      • 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.
    22. 22)
      • 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.
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-ifs.2016.0005
Loading

Related content

content/journals/10.1049/iet-ifs.2016.0005
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading
This is a required field
Please enter a valid email address