The Mondex case study about the specification and refinement
of an electronic purse as defined in [Stepney, Cooper, Woodcock 2000] 
has recently been proposed as a challenge for formal system-supported verification. 
I will report on the successful verification of the
case study using the KIV specification and verification system. 
I will 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.

I will also show an alternative formalisation of the communication
protocol using abstract state machines and explain how the verification
fits into our approach of systematic development of
E-commerce communication and security protocols.

Full details of the case study (including all proofs and a technical report) 
are available on http://www.informatik.uni-augsburg.de/swt/projects/mondex.html