Specification,proof, and model checking of the Mondex electronic purse using RAISE

This paper describes how the communication protocol of Mondex electronic purses can be specified and verified against desired security properties. The specification is developed by stepwise refinement using the RAISE formal specification language, RSL, and the proofs are made by translation to PVS and SAL. The work is part of a year-long project contributing to the international grand challenge in verified software engineering. J. C. P. Woodcock     

Verification of Mondex electronic purses with KIV: from transactions to a security protocol

The Mondex case study about the specification and refinement of an electronic purse as defined in the Oxford Technical Monograph PRG-126 has recently been proposed as a challenge for formal system-supported verification. In this paper we report on two results. First, on the successful verification of the full case study using the KIV specification and verification system. We demonstrate that even though the hand-made proofs were elaborated to an enormous level of detail we still could find small errors in the underlying data refinement theory, as well as the formal proofs of the case study. Second, the original Mondex case study verifies functional correctness assuming a suitable security protocol. We extend the case study here with a refinement to a suitable security protocol that uses symmetric cryptography to achieve the necessary properties of the security-relevant messages. The definition is based on a generic framework for defining such protocols based on abstract state machines (ASMs). We prove the refinement using a forward simulation. J. C. P. Woodcock     

Mechanising Mondex with Z/Eves

We describe our experiences in mechanising the specification, refinement, and proof of the Mondex Electronic Purse using the Z/Eves theorem prover. We took a conservative approach and mechanised the original LaT_EX sources without changing their technical content, except to correct errors. We found problems in the original specification and some missing invariants in the refinements. Based on these experiences, we present novel and detailed guidance on how to drive Z/Eves successfully. The work contributes to the Repository for the Verified Software Grand Challenge. C. B. Jones     

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 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. C. B. Jones