A systematic verification approach for Mondex electronic purses using ASMs

Abstract

In previous work we solved the challenge to mechanically verify the Mondex challenge about the specification and refinement of an electronic purse, using the given data refinement framework. In this paper we show that using ASM refinement and generalized forward simulations instead of the original approach allows to find a more systematic proof. Our technique of past and future invariants and simulations avoids the need to define a lot of properties for intermediate states during protocol runs. The new proof can be better automated in KIV. The systematic development of a generalized forward simulation uncovered a weakness of the protocol that could be exploited in a denial of service attack. We show a modification of the protocol that avoids this weakness, and that is even slightly easier to verify. © 2009 Springer-Verlag.