Abstract
The trusted platform module (TPM), a system component implemented on physical resources, is designed to enable computers to achieve a higher level of security than the security level that it is possible to achieve by software alone. For this reason, the TPM provides a way to store cryptographic keys and other sensitive data in its memory, which is shielded from access by any entity other than the TPM. Users who want to use those keys and data to achieve some security goals are restricted to interact with the TPM through its APIs defined in the TPM specification. Therefore, whether the TPM can provide Protected Capabilities it claimed depends to a large extent on the security of its APIs. In this paper, we devise a formal model, which is accessible to a fully mechanized analysis, for the key management APIs in the TPM2.0 specification. We identify and formalize security properties of these APIs in our model and then successfully use the automated prover Tamarin to obtain the first mechanized analysis of them. The analysis shows that the key management subset of TPM APIs preserves the secrecy of non-duplicable keys for unbounded numbers of fresh keys and handles. The analysis also reports that the key duplication mechanism, used to duplicate a key between two hierarchies, is vulnerable to impersonation attacks, which enable an adversary to recover the duplicated key of the originating hierarchy or import his own key into the destination hierarchy. Aiming at avoiding these vulnerabilities, we propose an approach, which restricts the originating and destination TPMs to authenticate each other’s identity during duplication. Then we formally demonstrate that our approach maintains the secrecy of duplicable keys when they are duplicated.
Similar content being viewed by others
References
Trusted Computing Group (2011) TPM main specification version 1.2 revision 116 parts 1–3. http://www.trustedcomputinggroup.org. Accessed 14 Sept 2013
Trusted Computing Group (2014) TPM platform module library family “2.0” revision 01.07 parts 1–4. http://www.trustedcomputinggroup.org. Accessed 14 April 2014
Chen L, Ryan M (2010) Attack, solution and verification for shared authorisation data in TCG TPM. Lect Notes Comput Sci 5983:201–216
Herzog J (2006) Applying protocol analysis to security device interfaces. IEEE Secur Priv 4:84–87
Lin AH (2005) Automated analysis of security APIs. PhD thesis, Massachusetts Institute of Technology
Ables K (2009) An alleged attack on key delegation in the trusted platform module. University of Birmingham, MSc Advanced Computer Science First semester mini-project
Gürgens S, Rudolph C, Scheuermann D et al (2007) Security evaluation of scenarios based on the TCG’s TPM specification. Lect Notes Comput Sci 4734:438–453
Delaune S, Kremer S, Ryan MD et al (2011) A formal analysis of authentication in the TPM. Lect Notes Comput Sci 6561:111–125
Abadi M, Fournet C (2001) Mobile values, new names, and secure communication. ACM SIGPLAN Notices 36:104–115
Blanchet B (2009) Automatic verification of correspondences for security protocols. J Comput Secur 17:363–434
Delaune S, Kremer S, Ryan MD et al (2011) Formal analysis of protocols based on TPM state registers. In: Proceedings of the 24th IEEE Computer Security Foundations Symposium. IEEE, Cernay-la-Ville, pp 66–80
Shao JX, Feng DG, Qin Y (2013) Type-based analysis of protected storage in the TPM. Lect Notes Comput Sci 8233:135–150
Schmidt B, Meier S, Cremers C et al (2012) Automated analysis of diffie-hellman protocols and advanced security properties. In: proceedings of the 25th IEEE Computer Security Foundations Symposium. IEEE, Cambridge, pp 78–94
Barker E, Chen L, Roginsky A et al (2013) Recommendation for pair-wise key establishment schemes using discrete logarithm cryptography. NIST Special Publication 800–56A
Meier S (2013) Advancing automated security protocol verification. PhD thesis, ETH
Escobar S, Sasse R, Meseguer J (2012) Folding variant narrowing and optimal variant termination. J Logic Algebr Progr 81:898–928
Meier S, Schmidt B, Cremers C et al (2013) The tamarin prover for the symbolic analysis of security protocols. Lect Notes Comput Sci 8044:696–701
LaMacchia B, Lauter K, Mityagin A (2007) Stronger security of authenticated key exchange. Lect Notes Comput Sci 4784:1–16
Acknowledgments
This work was supported by the National Natural Science Foundation of China (91118006 and 61202414) and the National Basic Research Program of China (2013CB338003).
Author information
Authors and Affiliations
Corresponding author
Additional information
SPECIAL TOPIC: Network and Information Security
About this article
Cite this article
Zhang, Q., Zhao, S., Qin, Y. et al. Formal analysis of TPM2.0 key management APIs. Chin. Sci. Bull. 59, 4210–4224 (2014). https://doi.org/10.1007/s11434-014-0575-0
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11434-014-0575-0