Events

3 May 2009

Orsay, Bat I, 1st floor,
MSR-INRIA Joint Centre,
High-Level Programming for E-Cash
Pedro Adão,
Instituto Superior Técnico, Lisbon

High-Level Programming for E-Cash

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.