Mondex: Engineering a Provable Secure Electronic Purse

Mondex electronic purses are used to replace cash payment by electronic payment with a smart card. Tool-based proofs of an abstract specification of the security protocol used by Mondex cards has been proposed as a challenge for mechanized verification. This paper extends the challenge and describes a comprehensive formal approach for developing Mondex that starts with the abstract specification that was used to certify Mondex, and ends with correct Java code. The development was verified with the theorem prover KIV using several refinements. Mondex cards can also be viewed as a challenge for software engineering a security-critical application. We describe a model-driven tool-supported approach, that uses UML models enhanced with security aspects, and generates correct and secure Java Card code. The UML models can also be used to generate the formal specifications used in KIV.