Skip to main content
SpringerLink
Log in

Automated Verification of e-Cash Protocols

  • Conference paper
  • First Online:
E-Business and Telecommunications (ICETE 2015)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 585))

Included in the following conference series:

  • 885 Accesses

Abstract

Electronic cash (e-cash) permits secure e-payments by providing security and anonymity similar to real cash. Several protocols have been proposed to meet security and anonymity properties of e-cash. However, there are no general formal definitions that allow the automatic verification of e-cash protocols. In this paper, we propose a formal framework to define and verify security properties of e-cash protocols. To this end, we model e-cash protocols in the applied \(\pi \)-calculus, and we formally define five relevant security properties. Finally, we validate our framework by analyzing, using the automatic tool ProVerif, four e-cash protocols: the online and the offline Chaum protocols, the Digicash protocol, and the protocol by Petersen and Poupard.

This research was conducted with the support of the “Digital trust” Chair from the University of Auvergne Foundation.

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 EPUB and 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

Notes

  1. 1.

    http://www.infsec.ethz.ch/research/software/tamarin.html.

  2. 2.

    http://sapic.gforge.inria.fr/.

  3. 3.

    DigiCash declared bankruptcy in 1998, and was sold to Blucora.

References

  1. Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: The 28th Symposium on Principles of Programming Languages, UK, pp. 104–115. ACM (2001)

    Google Scholar 

  2. Abe, M., Fujisaki, E.: How to date blind signatures. In: Kim, K.-C., Matsumoto, T. (eds.) ASIACRYPT 1996. LNCS, vol. 1163, pp. 244–251. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  3. Aboud, S.J., Agoun, A.: Analysis of a known offline e-coin system. Int. J. Comput. Appl. 98(15), 27–30 (2014)

    Google Scholar 

  4. Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: 14th IEEE Computer Security Foundations Workshop (CSFW 2014), Canada, pp. 82–96 (2001)

    Google Scholar 

  6. Brands, S.: Untraceable off-line cash in wallets with observers. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol. 773, pp. 302–318. Springer, Heidelberg (1994). http://dl.acm.org/citation.cfm?id=646758.705703

    Chapter  Google Scholar 

  7. Canard, S., Gouget, A.: Anonymity in transferable e-cash. In: Bellovin, S.M., Gennaro, R., Keromytis, A.D., Yung, M. (eds.) ACNS 2008. LNCS, vol. 5037, pp. 207–223. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  8. Chaum, D.: Blind signatures for untraceable payments. In: Chaum, D., Rivest, R.L., Sherman, A.T. (eds.) Advances in Cryptology: Proceedings of CRYPTO 1982, pp. 199–203. Springer, US (1983)

    Google Scholar 

  9. Chaum, D., Fiat, A., Naor, M.: Untraceable electronic cash. In: Goldwasser, S. (ed.) CRYPTO 1988. LNCS, vol. 403, pp. 319–327. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  10. Cheng, C.Y., Yunus, J., Seman, K.: Estimations on the security aspect of brand’s electronic cash scheme. In: 19th International Conference on Advanced Information Networking and Applications (AINA 2005), Taipei, Taiwan, 28–30 March 2005, pp. 131–134 (2005)

    Google Scholar 

  11. Crescenzo, G.D.: A non-interactive electronic cash system. In: Bonuccelli, M.A., Crescenzi, P., Petreschi, R. (eds.) CIAC 1994. LNCS, vol. 778, pp. 109–124. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  12. Damgård, I.B.: Payment systems and credential mechanisms with provable security against abuse by individuals. In: Goldwasser, S. (ed.) CRYPTO 1988. LNCS, vol. 403, pp. 328–335. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  13. D’Amiano, S., Di Crescenzo, G.: Methodology for digital money based on general cryptographic tools. In: De Santis, A. (ed.) EUROCRYPT 1994. LNCS, vol. 950, pp. 156–170. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  14. Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17, 435–487 (2009). http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DKR-jcs08.pdf

    MATH  Google Scholar 

  15. Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–208 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  16. Dreier, J., Kassem, A., Lafourcade, P.: Formal analysis of e-cash protocols. In: Proceedings of the 12th International Conference on Security and Cryptography, SECRYPT 2015, Colmar, Alsace, France, 20–22 July 2015, pp. 65–75 (2015). http://dx.doi.org/10.5220/0005544500650075

  17. Fan, C.I., Huang, V.S.M., Yu, Y.C.: User efficient recoverable off-line e-cash scheme with fast anonymity revoking. Math. Comput. Modell. 58(1–2), 227–237 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  18. Ferguson, N.: Single term off-line coins. In: Helleseth, T. (ed.) EUROCRYPT 1993. LNCS, vol. 765, pp. 318–328. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  19. Kim, S., Oh, H.: A new electronic check system with reusable refunds. Int. J. Inf. Sec. 1(3), 175–188 (2002). http://dx.doi.org/10.1007/s10207-002-0015-z

    Article  MATH  Google Scholar 

  20. Küsters, R., Truderung, T.: Reducing protocol analysis with xor to the xor-free case in the horn theory based approach. J. Autom. Reason. 46(3), 325–352 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  21. Luo, Z., Cai, X., Pang, J., Deng, Y.: Analyzing an electronic cash protocol using applied pi calculus. In: Katz, J., Yung, M. (eds.) ACNS 2007. LNCS, vol. 4521, pp. 87–103. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  22. Ogiela, M.R., Sulkowski, P.: Improved cryptographic protocol for digital coin exchange. In: Soft Computing and Intelligent Systems (SCIS), pp. 1148–1151 (2014)

    Google Scholar 

  23. Peterson, H., Poupard, G.: Efficient scalable fair cash with off-line extortion prevention. In: Han, Y., Quing, S. (eds.) ICICS 1997. LNCS, vol. 1334. Springer, Heidelberg (1997)

    Google Scholar 

  24. Pfitzmann, B., Schunter, M., Waidner, M.: How to break another “Provably Secure” payment system. In: Guillou, L.C., Quisquater, J.-J. (eds.) EUROCRYPT 1995. LNCS, vol. 921, pp. 121–132. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  25. Pfitzmann, B., Waidner, M.: How to break and repair a “Provably Secure” untraceable payment system. In: Feigenbaum, J. (ed.) CRYPTO 1991. LNCS, vol. 576, pp. 338–350. Springer, Heidelberg (1992)

    Google Scholar 

  26. Schoenmakers, B.: Security aspects of the Ecash\(^{\rm TM}\) payment system. In: Preneel, B., Rijmen, V. (eds.) COSIC 1997 Course. LNCS, vol. 1528, pp. 338–352. Springer, Heidelberg (1998)

    Google Scholar 

  27. Swe, A.T., Kyaw, K.K.K.: Formal analysis of secure e-cash transaction protocol. In: International Conference on Advances in Engineering and Technology, ICAET 2014, Singapore (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Inria, 54600, Villers-lés-Nancy, France

    Jannik Dreier

  2. CNRS, Loria, UMR 7503, 54506, Vandoeuvre-lés-Nancy, France

    Jannik Dreier

  3. Université de Lorraine, Loria, UMR 7503, 54506, Vandoeuvre-lés-Nancy, France

    Jannik Dreier

  4. University Grenoble Alpes, VERIMAG, 38000, Grenoble, France

    Ali Kassem

  5. Ascola Team (Mines Nantes, Inria, Lina) DAPI, École des Mines de Nantes, Nantes, France

    Ali Kassem

  6. University Clermont Auvergne, LIMOS, Clermont-Ferrand, France

    Pascal Lafourcade

Authors
  1. Jannik Dreier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ali Kassem
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Pascal Lafourcade
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ali Kassem .

Editor information

Editors and Affiliations

  1. Dept. of Computer & Info Science, Fordham University, Bronx, New York, USA

    Mohammad S. Obaidat

  2. IUT, University of Haute Alsace, Colmar, France

    Pascal Lorenz

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Dreier, J., Kassem, A., Lafourcade, P. (2016). Automated Verification of e-Cash Protocols. In: Obaidat, M., Lorenz, P. (eds) E-Business and Telecommunications. ICETE 2015. Communications in Computer and Information Science, vol 585. Springer, Cham. https://doi.org/10.1007/978-3-319-30222-5_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-30222-5_11

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-30221-8

  • Online ISBN: 978-3-319-30222-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation