A Systematic Verification Approach for Mondex Electronic Purses using ASMs

A Systematic Verification Approach for Mondex Electronic Purses using ASMs

erschienen 1.12.2006 in: Augsburg Technical Report, Institute of Computer Science, University of Augsburg

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 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.

Downloads:

• A Systematic Verification Approach for Mondex Electronic Purses using ASMs  -  (mondex-TR-27.pdf, 279 KB)