Abstract
Untraceability and unreuseability are essential security properties for electronic cash protocols. Many protocols have been proposed to meet these two properties. However, most of them have not been formally proved to be untraceable and unreuseable. In this paper we propose to use the applied pi calculus as a framework for describing and analyzing electronic cash protocols, and we analyze Ferguson’s electronic cash protocol as a case study. We believe that this approach is suitable for many different electronic cash protocols.
The work is supported by The National Grand Fundamental Research 973 Program of China (2003CB317005), and The National Nature Science Foundation of China (60473006) and (60573002).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Fournet, C.: Private Authentication. Theoretical Computer Science 322, 427–476 (2004)
Abadi, M., Blanchet, B., Fournet, C.: Just Fast Keying in the Pi Calculus. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 340–354. Springer, Heidelberg (2004)
Abadi, M., Cortier, V.: Deciding Knowledge in Security Protocols under Equational Theories. Theoretical Computer Science 367, 2–32 (2006)
Abadi, M., Fournet, C.: Mobile Values, New Names, and Secure Communication. In: Proceedings of POPL 2001, pp. 104–115 (2001)
Abadi, M., Gordon, A.D.: A Calculus for Cryptographic Protocols: The Spi Calculus. Information and Computation 148, 1–70 (1999)
Abadi, M., Gordon, A.D.: Reasoning about Cryptographic Protocols in the Spi Calculus. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 59–73. Springer, Heidelberg (1997)
Bhargava, M., Palamidessi, C.: Probabilistic anonymity. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 171–185. Springer, Heidelberg (2005)
Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: Proceedings of CSFW 2001, pp. 82–96 (2001)
Blanchet, B., Abadi, M., Fournet, C.: Automated Verification of Selected Equivalences for Security Protocols. In: Proceedings of LICS 2005, pp. 331–340 (2005)
Blom, S., Fokkink, W.J., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J.: μCRL: A Toolset for Analysing Algebraic Specifications. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 250–254. Springer, Heidelberg (2001)
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)
Brands, S.A.: An Efficient Off-line Electronic Cash System Based On The Representation Problem. CWI Technical Report, CS-R9323 (1993)
Chaum, D.: The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability. Journal of Cryptology 1, 65–75 (1988)
Chaum, D., Fiat, A., Naor, M.: Untraceable Electronic Cash. In: Goldwasser, S. (ed.) CRYPTO 1988. LNCS, vol. 403, pp. 319–327. Springer, Heidelberg (1990)
Chothia, T.: Analysing the MUTE Anonymous File-Sharing System Using the Pi-Calculus. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 115–130. Springer, Heidelberg (2006)
Chothia, T., Orzan, S., Pang, J., Dashti, M.T.: A Framework for Automatically Checking Anonymity with μCRL. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2007. LNCS, vol. 4661, Springer, Heidelberg (2007)
Deng, Y., Palamidessi, C., Pang, J.: Weak Probabilistic Anonymity. In: Proceedings of SECCO 2005, Electronic Notes in Theoretical Computer Science, to appear (2005)
Deng, Y., Pang, J., Wu, P.: Measuring anonymity with relative entropy. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2006. LNCS, vol. 4691, pp. 65–79. Springer, Heidelberg (2007)
Ferguson, N.: Single Term Off-Line Coins. In: Helleseth, T. (ed.) EUROCRYPT 1993. LNCS, vol. 765, pp. 318–328. Springer, Heidelberg (1994)
Franklin, M.K., Yung, M.: Secure and Efficient Off-Line Digital Money (Extended Abstract). In: Lingas, A., Carlsson, S., Karlsson, R. (eds.) ICALP 1993. LNCS, vol. 700, pp. 265–276. Springer, Heidelberg (1993)
Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A Tool for Automatic Verification of Probabilistic Systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006)
Hoare, T.: Communicating Sequential Processes. Communications of the ACM 21, 666–677 (1978)
Kremer, S., Ryan, M.: Analysis of an Electronic Voting Protocol in the Applied Pi Calculus. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 186–200. Springer, Heidelberg (2005)
Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-Key. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Herescu, O.M., Palamidessi, C.: Probabilistic Asynchronous π-Calculus. In: Tiuryn, J. (ed.) ETAPS 2000 and FOSSACS 2000. LNCS, vol. 1784, pp. 146–160. Springer, Heidelberg (2000)
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, I. Information and Computation 100, 1–40 (1992)
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes, II. Information and Computation 100, 41–77 (1992)
Schneider, S., Sidiropoulos, A.: CSP and Anonymity. In: Martella, G., Kurth, H., Montolivo, E., Bertino, E. (eds.) ESORICS 1996. LNCS, vol. 1146, pp. 198–218. Springer, Heidelberg (1996)
Tsiounis, Y.: Efficient Electronic Cash: New Notions and Techniques. PhD Thesis, Northeastern University (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Luo, Z., Cai, X., Pang, J., Deng, Y. (2007). Analyzing an Electronic Cash Protocol Using Applied Pi Calculus. In: Katz, J., Yung, M. (eds) Applied Cryptography and Network Security. ACNS 2007. Lecture Notes in Computer Science, vol 4521. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72738-5_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-72738-5_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72737-8
Online ISBN: 978-3-540-72738-5
eBook Packages: Computer ScienceComputer Science (R0)