High-Level Programming for E-Cash (joint work with Cédric Fournet and Nataliya Guts)
Extended Abstract presented at the 1st Computational and Symbolic Proofs of Security Workshop (CosyProofs). Atagawa Heights, Highashi Izu Peninsula, Japan, April 6--9, 2009.

Abstract: We consider symbolic characterizations of the Compact E-Cash protocol of Camenisch, Hohenberger, and Lysyanskaya [CHL05]. E-cash protocols [C82,CFN88] aim at providing robust abstractions for anonymous payment protocols. Properties of interest include, for instance, that users can spend coins anonymously, that users cannot forge coins, and that user should not spend the same coin twice without being eventually caught. These protocols involve sophisticated cryptographic constructions.
Relying on recent work on optimistic value commitment [FGZN08], we design a calculus with E-cash primitives. Our calculus has a simple, symbolic semantics; it can be used for programming with E-cash and for reasoning on its properties, while shielding the programmer from its cryptographic implementation.
We consider two variants of the symbolic semantics. An abstract semantics rules out any double spending (by design). A more realistic, intermediate semantics accounts for the possibility of double spending, with reliable detection. We first relate these two semantics, then relate the intermediate semantics to the computational properties of the underlying E-cash protocol.

Publication Info. Extended Abstract.

Date: 12 January 2009.

Get a preprint: PDF | PS | BibTeX Citation.