Formal Analysis of a TTP-Free Blacklistable Anonymous Credentials System

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10631)

Abstract

This paper firstly introduces a novel security definition for BLAC-like schemes (BLAC represents TTP-free BLacklistable Anonymous Credentials) in symbolic model using applied pi calculus, which is suitable for automated reasoning via formal analysis tools. We model the definitions of some common security properties: authenticity, non-framebility, mis-authentication resistance and privacy (anonymity and unlinkability). The case study of these security definitions is demonstrated by modelling and analyzing BLACR (BLAC with Reputation) system. We verify these security properties by Blanchet’s ProVerif and a ZKP (Zero-Knowledge Proof) compiler developed by Backes et al.. In particular, we analyze the express-lane authentication in BLACR. The analysis discovers a known attack that can be carried out by any potential user to escape from being revoked as he wishes. We provide a revised variant that can be proved successfully by ProVerif, which also indicates that the fix provided by ExBLACR (Extending BLACR) is incorrect.

Keywords

Formal analysis Anonymous credential ProVerif BLACR 

Notes

Acknowledgements

The research presented in this paper is supported by the National Grand Fundamental Research 973 Program of China under Grant No.2013CB338003 and the National Natural Science Foundation of China under Grant Nos. 91118006, 61202414.

References

  1. 1.
    Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. J. ACM (JACM) 52(1), 102–146 (2005)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Arapinis, M., Cheval, V., Delaune, S.: Verifying privacy-type properties in a modular way. In: CSF 2012, pp. 95–109. IEEE (2012)Google Scholar
  3. 3.
    Arapinis, M., Cheval, V., Delaune, S.: Composing security protocols: from confidentiality to privacy. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 324–343. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46666-7_17CrossRefGoogle Scholar
  4. 4.
    Arapinis, M., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In: CSF 2010, pp. 107–121. IEEE (2010)Google Scholar
  5. 5.
    Arapinis, M., Phillips, J., Ritter, E., Ryan, M.D.: Statverif: verification of stateful processes. J. Comput. Secur. 22(5), 743–821 (2014)CrossRefGoogle Scholar
  6. 6.
    Au, M.H., Tsang, P.P., Kapadia, A.: PEREA: practical TTP-free revocation of repeatedly misbehaving anonymous users. ACM Trans. Inf. Syst. Secur. (TISSEC) 14(4), 29 (2011)CrossRefGoogle Scholar
  7. 7.
    Au, M.H., Kapadia, A.: PERM: practical reputation-based blacklisting without TTPs. In: CCS 2012, pp. 929–940. ACM (2012)Google Scholar
  8. 8.
    Au, M.H., Kapadia, A., Susilo, W.: BLACR: TTP-free blacklistable anonymous credentials with reputation. In: NDSS Symposium 2012: 19th Network & Distributed System Security Symposium, pp. 1–17. Internet Society (2012)Google Scholar
  9. 9.
    Au, M.H., Susilo, W., Mu, Y.: Constant-size dynamic k-TAA. In: De Prisco, R., Yung, M. (eds.) SCN 2006. LNCS, vol. 4116, pp. 111–125. Springer, Heidelberg (2006).  https://doi.org/10.1007/11832072_8CrossRefGoogle Scholar
  10. 10.
    Backes, M., Maffei, M., Unruh, D.: Zero-knowledge in the applied pi-calculus and automated verification of the direct anonymous attestation protocol. In: SP 2008, pp. 202–215. IEEE (2008)Google Scholar
  11. 11.
    Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: SP 2004, pp. 86–100. IEEE (2004)Google Scholar
  12. 12.
    Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: 20th IEEE Symposium on Logic in Computer Science. Proceedings, pp. 331–340. IEEE (2005)Google Scholar
  13. 13.
    Blanchet, B., et al.: ProVerif: cryptographic protocol verifier in the formal model. http://prosecco.gforge.inria.fr/personal/bblanche/proverif/
  14. 14.
    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
  15. 15.
    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).  https://doi.org/10.1007/978-3-540-68979-9_13CrossRefGoogle Scholar
  16. 16.
    Brickell, E., Li, J.: Enhanced privacy ID: a direct anonymous attestation scheme with enhanced revocation capabilities. In: Proceedings of the 2007 ACM Workshop on Privacy in Electronic Society, pp. 21–30. ACM (2007)Google Scholar
  17. 17.
    Bruni, A., Modersheim, S., Nielson, F., Nielson, H.R.: Set-pi: set membership p-calculus. In: CSF 2015, pp. 185–198. IEEE (2015)Google Scholar
  18. 18.
    Camenisch, J., Drijvers, M., Lehmann, A.: Universally composable direct anonymous attestation. In: Cheng, C.-M., Chung, K.-M., Persiano, G., Yang, B.-Y. (eds.) PKC 2016. LNCS, vol. 9615, pp. 234–264. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49387-8_10CrossRefGoogle Scholar
  19. 19.
    Camenisch, J., et al.: Specification of the identity mixer cryptographic library, version 2.3. 1, 7 December 2010Google Scholar
  20. 20.
    Cheval, V., Blanchet, B.: Proving more observational equivalences with ProVerif. In: Basin, D., Mitchell, J.C. (eds.) POST 2013. LNCS, vol. 7796, pp. 226–246. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-36830-1_12CrossRefGoogle Scholar
  21. 21.
    Johnson, P.C., Kapadia, A., Tsang, P.P., Smith, S.W.: Nymble: anonymous IP-address blocking. In: Borisov, N., Golle, P. (eds.) PET 2007. LNCS, vol. 4776, pp. 113–133. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-75551-7_8CrossRefGoogle Scholar
  22. 22.
    Paquin, C., Zaverucha, G.: U-prove cryptographic specification v1. 1. Technical report, revision 3. Microsoft Corporation (2013)Google Scholar
  23. 23.
    Ryan, M.D., Smyth, B.: Applied pi calculus. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols, Chap. 6. IOS Press (2011)Google Scholar
  24. 24.
    Schmidt, B., Meier, S., Cremers, C., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: CSF 2012, pp. 78–94. IEEE (2012)Google Scholar
  25. 25.
    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).  https://doi.org/10.1007/978-3-642-29420-4_16CrossRefGoogle Scholar
  26. 26.
    Smyth, B., Ryan, M.D., Chen, L.: Formal analysis of privacy in direct anonymous attestation schemes. Sci. Comput. Program. 111, 300–317 (2015)CrossRefGoogle Scholar
  27. 27.
    Tsang, P.P., Au, M.H., Kapadia, A., Smith, S.W.: BLAC: revoking repeatedly misbehaving anonymous users without relying on TTPs. ACM Trans. Inf. Syst. Secur. (TISSEC) 13(4), 39 (2010)CrossRefGoogle Scholar
  28. 28.
    Wang, W.: Proverif inputs for analyzing BLACR system. https://github.com/WangWeijin/Formal-analysis-of-BLACR-system
  29. 29.
    Wang, W., Feng, D., Qin, Y., Shao, J., Xi, L., Chu, X.: ExBLACR: extending BLACR system. In: Susilo, W., Mu, Y. (eds.) ACISP 2014. LNCS, vol. 8544, pp. 397–412. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-08344-5_26CrossRefGoogle Scholar
  30. 30.
    Xi, L., Feng, D.: FARB: fast anonymous reputation-based blacklisting without TTPs. In: Proceedings of the 13th Workshop on Privacy in the Electronic Society, pp. 139–148. ACM (2014)Google Scholar
  31. 31.
    Xi, L., Feng, D.: Formal analysis of DAA-related APIs in TPM 2.0. In: Au, M.H., Carminati, B., Kuo, C.-C.J. (eds.) NSS 2014. LNCS, vol. 8792, pp. 421–434. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11698-3_32CrossRefGoogle Scholar
  32. 32.
    Yu, K.Y., Yuen, T.H., Chow, S.S.M., Yiu, S.M., Hui, L.C.K.: PE(AR)2: privacy-enhanced anonymous authentication with reputation and revocation. In: Foresti, S., Yung, M., Martinelli, F. (eds.) ESORICS 2012. LNCS, vol. 7459, pp. 679–696. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33167-1_39CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Weijin Wang
    • 1
    • 2
  • Jingbin Liu
    • 1
    • 2
  • Yu Qin
    • 1
  • Dengguo Feng
    • 1
    • 3
  1. 1.TCAInstitute of Software, Chinese Academy of SciencesBeijingChina
  2. 2.University of Chinese Academy of SciencesBeijingChina
  3. 3.SKLCSInstitute of Software, Chinese Academy of SciencesBeijingChina

Personalised recommendations