By the same authors

An Electronic Purse: Specification, Refinement, and Proof

Research output: Working paper

Standard

An Electronic Purse : Specification, Refinement, and Proof. / Stepney, Susan; Cooper, David; Woodcock, Jim.

Oxford : Oxford University Computing Laboratory, 2000.

Research output: Working paper

Harvard

Stepney, S, Cooper, D & Woodcock, J 2000 'An Electronic Purse: Specification, Refinement, and Proof' Oxford University Computing Laboratory, Oxford.

APA

Stepney, S., Cooper, D., & Woodcock, J. (2000). An Electronic Purse: Specification, Refinement, and Proof. Oxford: Oxford University Computing Laboratory.

Vancouver

Stepney S, Cooper D, Woodcock J. An Electronic Purse: Specification, Refinement, and Proof. Oxford: Oxford University Computing Laboratory. 2000 Jul 1.

Author

Stepney, Susan ; Cooper, David ; Woodcock, Jim. / An Electronic Purse : Specification, Refinement, and Proof. Oxford : Oxford University Computing Laboratory, 2000.

Bibtex - Download

@techreport{28ae29ade54c4ed9a17ac7675d64751b,
title = "An Electronic Purse: Specification, Refinement, and Proof",
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.",
author = "Susan Stepney and David Cooper and Jim Woodcock",
year = "2000",
month = "7",
day = "1",
language = "Undefined/Unknown",
publisher = "Oxford University Computing Laboratory",
type = "WorkingPaper",
institution = "Oxford University Computing Laboratory",

}

RIS (suitable for import to EndNote) - Download

TY - UNPB

T1 - An Electronic Purse

T2 - Specification, Refinement, and Proof

AU - Stepney, Susan

AU - Cooper, David

AU - Woodcock, Jim

PY - 2000/7/1

Y1 - 2000/7/1

N2 - 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.

AB - 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.

M3 - Working paper

BT - An Electronic Purse

PB - Oxford University Computing Laboratory

CY - Oxford

ER -