Introduction:

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.

@techreport(SS-PRG-126,
  author = "Susan Stepney and David Cooper and Jim Woodcock",
  title = "An Electronic Purse: Specification, Refinement, and Proof",
  institution = "Oxford University Computing Laboratory",
  type = "Technical monograph",
  number = "PRG-126",
  month = jul,
  year = 2000
)