ISSE

Search

A Systematic Verification Approach for Mondex Electronic Purses using ASMs

Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Nina Moebius, Wolfgang Reif

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.
published 2007 Proceedings of the Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis, Springer, LNCS