Abstract
A definition of user-controlled anonymity is introduced for Direct Anonymous Attestation schemes. The definition is expressed as an equivalence property suited to automated reasoning using ProVerif and the practicality of the definition is demonstrated by examining the ECCbased Direct Anonymous Attestation protocol by Brickell, Chen & Li.We show that this scheme satisfies our definition under the assumption that the adversary obtains no advantage from re-blinding a blind signature.
Ben Smyth’s work was partly done at Loria, CNRS & INRIA Nancy Grand Est, France and the School of Computer Science, University of Birmingham, UK.
This is a preview of subscription content, log in via an institution to check access.
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: CCS 2004: 11th ACM Conference on Computer and Communications Security, pp. 132–145. ACM Press (2004)
Brickell, E., Chen, L., Li, J.: Simplified Security Notions of Direct Anonymous Attestation and a Concrete Scheme from Pairings. Cryptology ePrint Archive, Report 2008/104 (2008)
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)
Chen, L.: A DAA Scheme Requiring Less TPM Resources. Cryptology ePrint Archive, Report 2010/008 (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.: 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)
Trusted Computing Group: Draft TPM 2.0 Specification, Revision oo79 (2011)
International Organization for Standardization: ISO/IEC WD 20008-2 (Working Draft) Information technology – Security techniques – Anonymous digital signature – Part 2: Mechanisms using a group public key (2011)
Chen, L., Morrissey, P., Smart, N.P.: DAA: Fixing the pairing based protocols (2011) (unpublished draft)
Chen, L., Morrissey, P., Smart, N.P.: DAA: Fixing the pairing based protocols. Cryptology ePrint Archive, Report 2009/198 (2009)
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, M., Maffei, M., Unruh, D.: Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol. In: S&P 2008: 29th IEEE Symposium on Security and Privacy, pp. 202–215. IEEE Computer Society (2008)
Blanchet, B.: Automatic Proof of Strong Secrecy for Security Protocols. In: S&P 2004: 25th IEEE Symposium on Security and Privacy, pp. 86–100. IEEE Computer Society (2004)
Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming 75(1), 3–51 (2008)
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL 2001: 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 104–115. ACM Press (2001)
Ryan, M.D., Smyth, B.: Applied pi calculus. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols. IOS Press (2011)
Blanchet, B., Smyth, B.: ProVerif: Automatic Cryptographic Protocol Verifier User Manual & Tutorial (2011), http://www.proverif.ens.fr/
Trusted Computing Group: TPM Specification version 1.2 (2007)
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)
Camenisch, J., Stadler, M.: Efficient Group Signature Schemes for Large Groups. In: Kaliski Jr., B.S. (ed.) CRYPTO 1997. LNCS, vol. 1294, pp. 410–424. Springer, Heidelberg (1997)
Smyth, B., Ryan, M.D., Chen, L.: Direct Anonymous Attestation (DAA): Ensuring Privacy with Corrupt Administrators. In: Stajano, F., Meadows, C., Capkun, S., Moore, T. (eds.) ESAS 2007. LNCS, vol. 4572, pp. 218–231. Springer, Heidelberg (2007)
Smyth, B.: Formal verification of cryptographic protocols with automated reasoning. PhD thesis, School of Computer Science. University of Birmingham (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Smyth, B., Ryan, M., Chen, L. (2012). Formal Analysis of Anonymity in ECC-Based Direct Anonymous Attestation Schemes. In: Barthe, G., Datta, A., Etalle, S. (eds) Formal Aspects of Security and Trust. FAST 2011. Lecture Notes in Computer Science, vol 7140. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29420-4_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-29420-4_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29419-8
Online ISBN: 978-3-642-29420-4
eBook Packages: Computer ScienceComputer Science (R0)