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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
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)
Trusted Computing Group: TCG TPM specification 1.2 (2003), https://www.trustedcomputinggroup.org
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)
Chen, X., Feng, D.: Direct anonymous attestation for next generation tpm. Journal of Computers 3(12), 43–50 (2008)
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)
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)
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)
Trusted Computing Group: TCG TPM specification 2.0 (2012), https://www.trustedcomputinggroup.org
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)
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)
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)
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)
Chen, L., Morrissey, P., Smart, N.P.: DAA: Fixing the pairing based protocols. Technical report, Cryptology ePrint Archive, Report 2009/198 (2009)
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)
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)
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)
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. ACM SIGPLAN Notices 36, 104–115 (2001)
Ryan, M., Smyth, B.: Formal Models and Techniques for Analyzing Security Protocols, ch. 6. IOS Press (2010)
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)
Blanchet, B.: Automatic verification of correspondences for security protocols. Journal of Computer Security 17(4), 363–434 (2009)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)