ISSE

Search

A Systematic Verification Approach for Mondex Electronic Purses using ASMs

G. Schellhorn, H. Grandy, D. Haneberg, N. Moebius, W. Reif

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 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.
published 1.12.2006 in: Augsburg Technical Report, Institute of Computer Science, University of Augsburg


BibTex

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


Downloads: