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

This Web presentation shows a formalisation of the Mondex case study using three orthogonal ASM refinements (plus a technical one). The emphasis is on clarifying the essential concepts of the Mondex protocol. A description of the results can be found in [Mondex-incr-08]. The development is divided into two layers. The first layer contains the same refinement theory as used for the development as a single refinement step we did earlier. The second layer contains the case study itself. Its main specifications and theorems are:

Specification of the abstract ASM (AASM) containing the transactions to transfer money.
Specification of the first refined ASM (IASM) which defines a protocol using 3 messages .
For verification a simulation relation between AASM and IASM and an invariant for IASM are needed. The invariant is composed of protocol-local invariants, that state informally that the two participating purses have done some steps into the protocol. A wp-calculus formula is used to systematically state this property, avoiding an encoding as predicate logic properties. The protocol-local invariant is an improvement compared to the purse-local invariant CINV used in the verification of Mondex as one refinement.
Specification of the second refined ASM (EASM) which adds replay attacks by moving messages from individual mailboxes to a global attacker knowledge (the ether).
In contrast to the first, the second refinement is a pure data refinement. Again a simulation relation between IASM and EASM (using some auxiliary definitions) and an invariant for EASM are needed.
Specification of the third refined ASM (SASM) which replaces unique identifiers for protocol runs with sequence numbers and adds a challenge-response scheme.
For verification a simulation relation between EASM and SASM (using some auxiliary definitions) and an invariant for SASM are needed.
Specification of the final refined ASM (CASM) which slightly restructures the third to arrive at the concrete level of Mondex (which is the same as in the one step development). The simulation relation between SASM and CASM is rather simple.

[Mondex-incr08]	Gerhard Schellhorn and Richard Banach, A Concept-Driven Construction of the Mondex Protocol using Three Refinements, submitted to ABZ 2008, available from the authors
[Mondex00]	S. Stepney and D. Cooper and J, Woodcock, AN ELECTRONIC PURSE Specification, Refinement and Proof, Technical Monograph, Oxford University Computing Laboratory, PRG-126 available here
[Mondex-ASM08]	Gerhard Schellhorn and Holger Grandy and Dominik Haneberg and Nina Moebius and Wolfgang Reif, A Systematic Verification Approach for Mondex Electronic Purses using ASMs, Proceedings of the Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis,Springer,2008, to appear
[Boe03]	E. Börger, The ASM Refinement Method, Formal Aspects of Computing, 2003
[SchJUCS01]	G. Schellhorn, Verification of ASM Refinements Using Generalized Forward Simulation, Journal of Universal Computer Science, Vol. 7(11),pp. 952--979,2001, available here
[Sch05]	G. Schellhorn, ASM Refinement and Generalizations of Forward Simulation in Data Refinement: A Comparison,Journal of Theoretical Computer Science, vol. 336, no. 2-3, pp. 403-435 ,2005