LSV Seminar

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.

Past Seminars

High-Level Programming for E-Cash

 Pedro Adão
Tuesday, May 12 2009 at 11:00AM
Salle Condorcet (Bâtiment d'Alembert)
Pedro Adão (Instituto de Telecomunicacões, Lisboa, Portugal)

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 impossible task.

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.

About LSV