The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
E-cash protocols 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 a user should not spend the same coin
twice without being eventually caught. These protocols involve
sophisticated cryptographic constructions such as blind signatures
and commitment and proving their correctness is a non-trivial
task, hence reasoning about e-cash applications becomes an almost
Relying on recent work on optimistic value commitment [FGZN08], we propose a calculus to reason about e-cash applications. 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) while a more realistic, intermediate semantics accounts for the possibility of double spending, with reliable detection. We first relate these two semantics, and then relate the intermediate semantics to the computational properties of the underlying e-cash protocol. We show that our calculus is a sound abstraction of the low-level e-cash protocols, that is, all low-level behaviours can be mapped to an high-level equivalent trace.