The certification of the Mondex electronic purse to ITSEC Level E6

Ten years ago the Mondex electronic purse was certified to ITSEC Level E6, the highest level of assuranceforsecuresystems.ThisinvolvedbuildingformalmodelsintheZnotation,linkingthemwithrefinement, and proving that they correctly implement the required security properties. The work has been revived recently as a pilot project for the international Grand Challenge in Verified Software. This paper records the history of the original project and gives an overview of the formal models and proofs used.

• Type: Journal
• Year: 2008
• Where: FAC
• Authors: Jim Woodcock, Susan Stepney, David Cooper, John A. Clark, Jeremy Jacob
• Keywords: FAC 2008, International Grand Challenge, Mondex Electronic Purse, Required Security Properties