ISSE

Search

The Mondex Challenge: Machine Checked Proofs for an Electronic Purse

Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Wolfgang Reif

The Mondex Challenge: Machine Checked Proofs for an Electronic Purse

The Mondex case study about the specification and refinement of an electronic purse as defined in [SCJ00] has recently been proposed as a challenge for formal system-supported verification. This paper reports on the successful verification of the major part of the 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. We also provide an alternative formalisation of the communication protocol using abstract state machines. Finally the Mondex case study verifies functional correctness assuming a suitable security protocol. Therefore we propose to extend the case study to include the verification of a suitable security protocol.
published August 2006 Proceedings of FM 2006: Formal Methods 14th International Symposium on Formal Methods Hamilton, Canada, August 21-27, 2006, Springer LNCS 4085

Publisher: Springer

DOI: http://dx.doi.org/10.1007/11813040_2


BibTex

For questions regarding the publication, please contact publications@isse.de!


Links: