AN ELECTRONIC PURSE − Specification‚ Refinement‚ and Proof

Abstract

This case study is a reduced version of a real development by the NatWest Development Team (now platform seven) 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.