Analyzing an Electronic Cash Protocol Using Applied Pi Calculus

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.

• Type: Conference
• Year: 2007
• Where: ACNS
• Authors: Zhengqin Luo, Xiaojuan Cai, Jun Pang, Yuxin Deng
• Keywords: ACNS 2007, Cryptography, Electronic Cash Protocols, Ferguson’s Electronic Cash, Many Protocols