E6 Smartcard applications

Logica provided security consultancy to NatWest Bank, through platform seven , who were in the process of developing high assurance smartcard based products to E6. The consultancy covered various aspects of electronic commerce and trading.

As part of the consultancy, Logica provided a team of formal methods experts to assist in the development of formally proven, high assurance smartcard based applications.

Some of the products were developed to undergo evaluation to ITSEC level E6 by the Logica CLEF. These were the first such products to target evaluation to E6, and as such broke new ground in the development of high assurance products.

9 September 1999
Mondex and MULTOS are awarded a security rating of ITSEC Level E6

Various discussions and technical details can be found in:

Retrenching the Purse
- 2007 • Retrenchment and the Atomicity Pattern
- 2007 • Engineering and theoretical underpinnings of retrenchment
- 2007 • The Balance Enquiry Quandary, and Generalised and (1, 1) Forward Refinements
- 2006 • Hashing injective CLEAR codes, and security properties
- 2006 • Finite Exception Logs, and Validating the Small
- 2005 • Finite Sequence Numbers and the Tower Pattern
- 2005 • Retrenchment and the Mondex Electronic Purse
2008 • The certification of the Mondex electronic purse to ITSEC Level E6 • history
2002 • Derivation of Z Refinement Proof Rules
2001 • New Horizons in Formal Methods • overview of Mondex and Multos
2000 • An Electronic Purse: Specification, Refinement, and Proof • Mondex
2000 • Formal Methods for Industrial Products • the Multos project
2000 • Segregation with Communication • securely segregating Multos applications
1998 • A Tale of Two Proofs • discussion of the Mondex proof
1998 • More Powerful Z Data Refinement • the backwards and i/o refinement rules

Various presentations: