A Systematic Verification Approach for Mondex Electronic Purses using ASMs

In [SGHR06] we have solved the challenge to mechanically verify the Mondex challenge about the specification and refinement of an electronic purse as defined in [SCJ00]. 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 many 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.