A Systematic Verification Approach for Mondex Electronic Purses using ASMs

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

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.
published 2008 Rigorous Methods for Software Construction and Analysis - Papers Dedicated to Egon Börger on the Occasion of His 60th Birthday. Jean-Raymond Abrial, Uwe Glässer (Editors), LNCS 5115

Publisher: Springer



For questions regarding the publication, please contact!