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

Abstract. 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.

• Type: Conference
• Year: 2008
• Where: ASM
• Authors: Gerhard Schellhorn, Richard Banach
• Keywords: ASM 2008, Computational Biology, Concepts Underlying Mondex, Electronic Purse Protocol, Mondex Case Study