A Concept-Driven Construction of the Mondex Protocol using Three Refinements

G. Schellhorn and R. Banach

The Mondex case study concerns the formal development and verification of an electronic purse protocol. Several groups have worked on its specification and mechanical verification, their solutions being (as were ours previously), either one big step or several steps motivated by the task's complexity. A new solution is presented that is structured into three refinements, motivated by the three concepts underlying Mondex: a message protocol to transfer money over a lossy medium, protection against replay attacks, and uniqueness of transfers using sequence numbers. We also give an improved proof technique based on our theoretical results on verifying interleaved systems.
published 2008 in: to appear in LNCS Proceedings of ABZ 2008

Publisher: Springer