2007/12/11 by Jim Woodcock, Susan Stepney, David Cooper +2 · 3 citations
Computer Science · #Security and Verification in Computing #Cryptographic Implementations and Security #Advanced Malware Detection Techniques
paper · pdf · doi:10.1007/s00165-007-0060-5
openalex publication_date 2007/12/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/23
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.