Sciweavers

Share
ASM
2008
ASM

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

9 years 10 months ago
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.
Gerhard Schellhorn, Richard Banach
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where ASM
Authors Gerhard Schellhorn, Richard Banach
Comments (0)
books