By the same authors

An Electronic Purse: Specification, Refinement, and Proof

Research output: Working paper

Author(s)

Department/unit(s)

Publication details

DatePublished - 1 Jul 2000
PublisherOxford University Computing Laboratory
Place of PublicationOxford
Original languageUndefined/Unknown

Abstract

This case study is a reduced version of a real development by the NatWest Development Team of a Smartcard product for electronic commerce. This development was deeply security critical: it was vital to ensure that these cards would not contain any bugs in implementation or design that would allow them to be subverted once in the field.

The system consists of a number of electronic purses that carry financial value, each hosted on a Smartcard. The purses interact with each other via a communications device to exchange value. Once released into the field, each purse is on its own: it has to ensure the security of all its transactions without recourse to a central controller. All security measures have to be implemented on the card, with no real­time external audit logging or monitoring.

We develop two key models in this case study. The first is an abstract model, describing the world of purses and the exchange of value through atomic transactions, expressing the security properties that the cards must preserve. The second is a concrete model, reflecting the design of the purses which exchange value using a message protocol. Both models are described in the Z notation, and we prove that the concrete model is a refinement of the abstract.

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations