ASM Refinement Preserving Invariants

Gerhard Schellhorn (University of Augsburg, Germany)

Abstract: This paper gives a definition of ASM refinement suitable for the verification that a protocol implements atomic transactions. We used this definition as the basis of the formal verification of the refinements of the Mondex case study with the interactive theorem prover KIV. The refinement definition we give differs from the one we gave in earlier work which preserves partial and total correctness assertions of ASM runs. The reason is that the main goal of the refinement of the Mondex protocol is to preserve a security invariant, while total correctness is not preserved. To preserve invariants, the definition of generalized forward simulation is limited to the use of "small" diagrams, which contain of a single protocol step. We show a technique that allows to use the natural "big" diagrams that consist of an atomic action being refined by a full protocol run.

Keywords: Abstract State Machines, Mondex, commuting diagrams, data refinement, dynamic logic, electronic purses, forward simulation, interactive theorem proving, refinement, security, weakest preconditions

Categories: D.2.1, D.2.4, D.3.1, D.4.6, F.3.1, F.4.1