By the same authors

From the same journal

From the same journal

The certification of the Mondex electronic purse to ITSEC level E6

Research output: Contribution to journalArticle



Publication details

JournalFormal Aspects of Computing
DatePublished - Jan 2008
Issue number1
Number of pages15
Pages (from-to)5-19
Original languageEnglish


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.

Bibliographical note

Query date: 14/01/2011

    Research areas

  • certification, correctness, electronic finance, grand challenges, Grand Challenge in Verified Software, ITSEC Level E6, Mondex, refinement, security, smart cards, theorem proving, verification, Verified Software Repository, Z notation, REFINEMENT

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations