# 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

- Date
- Tuesday, May 12 2009 at 11:00AM
- Place
- Salle Condorcet (Bâtiment d'Alembert)
- Speaker
- 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.