The certification of the Mondex electronic purse to ITSEC Level E6
Jim Woodcock, Susan Stepney, David F. Cooper, John A. Clark, Jeremy L. Jacob · Formal Aspects of Computing · 2007
Abstract. Ten years ago the Mondex electronic purse was certified to ITSEC Level E6, the highest level of assurance for secure systems. This involved building formal models in the Z notation, linking them with refinement, 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.