Skip to main content
SpringerLink
Log in

Formal Analysis of DAA-Related APIs in TPM 2.0

  • Conference paper
Network and System Security (NSS 2015)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 8792))

Included in the following conference series:

Abstract

Direct Anonymous Attestation (DAA) is a signature scheme that provides a balance between user privacy and authentication in a reasonable way. Various DAA schemes are now supported by the latest TPM 2.0 specification. We propose a general symbolic model for DAA schemes and formalize DAA-related APIs in TPM 2.0 specification in applied pi calculus. We present new symbolic definitions of user-controlled traceability and non-frameability. Then we propose a novel property of DAA called forward anonymity. The application of our definitions is demonstrated by analyzing the implementation of an ECC-based DAA protocol using APIs proposed by the TPM 2.0 specification. Our analysis finds a weakness in an API which leads to attack against forward anonymity. We propose modifications to the API and verify our properties for the modified API.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Brickell, E., Camenisch, J., Chen, L.: Direct anonymous attestation. In: Proceedings of the 11th ACM Conference on Computer and Communications Security, pp. 132–145. ACM (2004)

    Google Scholar 

  2. Trusted Computing Group: TCG TPM specification 1.2 (2003), https://www.trustedcomputinggroup.org

  3. Brickell, E., Chen, L., Li, J.: A new direct anonymous attestation scheme from bilinear maps. In: Lipp, P., Sadeghi, A.-R., Koch, K.-M. (eds.) TRUST 2008. LNCS, vol. 4968, pp. 166–178. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  4. Chen, X., Feng, D.: Direct anonymous attestation for next generation tpm. Journal of Computers 3(12), 43–50 (2008)

    MathSciNet  Google Scholar 

  5. Chen, L., Page, D., Smart, N.P.: On the design and implementation of an efficient DAA scheme. In: Gollmann, D., Lanet, J.-L., Iguchi-Cartigny, J. (eds.) CARDIS 2010. LNCS, vol. 6035, pp. 223–237. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  6. Chen, L.: A DAA scheme requiring less TPM resources. In: Bao, F., Yung, M., Lin, D., Jing, J. (eds.) Inscrypt 2009. LNCS, vol. 6151, pp. 350–365. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  7. Brickell, E., Chen, L., Li, J.: Simplified security notions of direct anonymous attestation and a concrete scheme from pairings. International Journal of Information Security 8(5), 315–330 (2009)

    Article  Google Scholar 

  8. Trusted Computing Group: TCG TPM specification 2.0 (2012), https://www.trustedcomputinggroup.org

  9. Chen, L., Li, J.: Flexible and scalable digital signatures in TPM 2.0. In: Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security, pp. 37–48. ACM (2013)

    Google Scholar 

  10. Chen, L., Morrissey, P., Smart, N.P.: On proofs of security for DAA schemes. In: Baek, J., Bao, F., Chen, K., Lai, X. (eds.) ProvSec 2008. LNCS, vol. 5324, pp. 156–175. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Backes, Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: 29th IEEE Symposium on Security and Privacy, pp. 202–215. IEEE Computer Society (2008)

    Google Scholar 

  12. Smyth, B., Ryan, M., Chen, L.: Formal analysis of anonymity in ECC-based direct anonymous attestation schemes. In: Barthe, G., Datta, A., Etalle, S. (eds.) FAST 2011. LNCS, vol. 7140, pp. 245–262. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  13. Chen, L., Morrissey, P., Smart, N.P.: DAA: Fixing the pairing based protocols. Technical report, Cryptology ePrint Archive, Report 2009/198 (2009)

    Google Scholar 

  14. Chen, L., Ryan, M.: Attack, solution and verification for shared authorisation data in TCG TPM. In: Degano, P., Guttman, J.D. (eds.) FAST 2009. LNCS, vol. 5983, pp. 201–216. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. Delaune, S., Kremer, S., Ryan, M.D., Steel, G.: A formal analysis of authentication in the TPM. In: Degano, P., Etalle, S., Guttman, J. (eds.) FAST 2010. LNCS, vol. 6561, pp. 111–125. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  16. Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: CSFW 2001: Proceedings of the 14th IEEE Computer Security Foundations Workshop, pp. 82–96. IEEE Computer Society (2001)

    Google Scholar 

  17. Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. ACM SIGPLAN Notices 36, 104–115 (2001)

    Article  Google Scholar 

  18. Ryan, M., Smyth, B.: Formal Models and Techniques for Analyzing Security Protocols, ch. 6. IOS Press (2010)

    Google Scholar 

  19. Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, LICS 2005, pp. 331–340. IEEE (2005)

    Google Scholar 

  20. Blanchet, B.: Automatic verification of correspondences for security protocols. Journal of Computer Security 17(4), 363–434 (2009)

    Google Scholar 

  21. Camenisch, J., Lysyanskaya, A.: Signature schemes and anonymous credentials from bilinear maps. In: Franklin, M. (ed.) CRYPTO 2004. LNCS, vol. 3152, pp. 56–72. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Trusted Computing and Information Assurance Laboratory Institute of Software, Chinese Academy of Sciences, China

    Li Xi & Dengguo Feng

Authors
  1. Li Xi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dengguo Feng
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing, Hong Kong Polytechnic University, Hung Hom, Kowloon, Hong Kong

    Man Ho Au

  2. Department of Computer Science and Communication, University of Insubria, Via Mazzini, 5, 21100, Varese, Italy

    Barbara Carminati

  3. Ming Hsieh Department of Electrical Engineering, University of Southern California, 3740 McClintock Avenue, EEB 100, 90089-2560, Los Angeles, CA, USA

    C.-C. Jay Kuo

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Xi, L., Feng, D. (2014). Formal Analysis of DAA-Related APIs in TPM 2.0. In: Au, M.H., Carminati, B., Kuo, CC.J. (eds) Network and System Security. NSS 2015. Lecture Notes in Computer Science, vol 8792. Springer, Cham. https://doi.org/10.1007/978-3-319-11698-3_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-11698-3_32

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-11697-6

  • Online ISBN: 978-3-319-11698-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation