A Systematic Verification Approach for Mondex Electronic Purses using ASMs

We have already solved the challenge to mechanically verify the Mondex challenge about the specification and refinement of an electronic purse. In this paper we show that the verification can be made more systematic and better automated using ASM refinement instead of the original data refinement. This avoids to define a lot of properties of intermediate states during protocol runs. The systematic development of a generalized forward simulation also uncovered a weakness of the protocol that could be exploited in a denial of service attack.