Mondex ASM Refinement

• Project ASM-INV-Refinement contains a formalization of a variant of ASM Refinement [SchJUCS01][Boe03][Sch05]). This variant preserves invariants. The theory is developed in 3 steps:
  • First a purely algebraic theory of refinement is developed: trace-EF-AF defines a theory of traces (runs) and temporal operators (EF,AF) for an interpreter consisting of initial states, final states and a step relation. Specification forward defines the proof obligations for generalized forward simulation and forward-is-refine shows that these imply refinement (a form of trace inclusion that preserves a relation IO for infinite runs).
  • In the second step this algebraic theory is used as the semantics of ASM rules using an embedding: specification DLinterpreter gives the abstract shape of an ASM rule (+ initial and final states). Based on this definition a relation over states with bottom (for nontermination) is defined (the semantics of the ASM rule). Then the notions of traces, temporal operators and refinement are lifted to show that the proof obligations for generalized forward simulation (now for ASM rules) are instances of those semantically defined, and imply refinement, which is now also expressed without explicit reference to bottom.
  • The proof obligations are rather complex. Stronger conditions based on loops (instead of temporal operators) are usually satisfied in case studies (such as Mondex or WAM), and we show that they imply the fully general ones of Step 2.
• Project Mondex-ASM contains the Mondex case study itself. Its main specifications and theorems are the following:
  • Specification of the abstract ASM containing the transactions. and specification of the concrete ASM containing the communication protocol. Both ASMs specification uses various data types to build up their states. Two types of sets are involved: finite Sets that are term-generated by an empty set and an insert operation, and (potentially) infinite Sets , which are specified to be isomorphic to boolean functions via a .
  • The main proof obligation of the refinement: , (commutativity of a diagram for simulation relation ACINV) is proven in specification ASM-refine . The specification of ACINV, which is based on a systematic definition of a local simulation relation LACINV for an individual purse, is also given in this specification. Because of this definition, the proof can be localised to a lemma for each purse that uses LACINV . Getting LACINV right such that this lemma is provable is the creative (and hard) part of the development. Note that the proof of the lemma is rather large but (nearly) fully automatic.
  • The proof of the local simulation relation could be fully automated, by defining an invariant CINV for the concrete ASM (first only syntactically) that was used as an additional precondition. Every time the proof got stuck we looked at which property CINV should imply to close the proof. The resulting 26 properties are collected and proved here .
  • The invariant CINV of the concrete ASM is also defined using a local invariant LOCALINV . The main idea behing the local invariant is simply: Every purse has done some steps into the protocol starting from some old state (correspoding to the four axioms):
    • for state idle, it has done no steps and is still in the old state
    • for state epr, it has done a STARTFROM
    • for state epv, it has done STARTTO
    • for state epa, it has done STARTFROM and REQ
    Note the use of protocol steps in the definition of the invariant, which trivialises all steps into the protocol, and allows to avoid the definition of many properties of intermediate protocol states (that were necessary in the original Mondex proof in [Mondex00]. The main invariance proof for CINV reduces to two main lemmas for LOCALINV: one, where the receiver of a message and the purse which LOCALINV talks about, are the same , and one, where they are different. Again getting the definitions of CINV and LOCALINV right is the hard part, and the proofs of the two main lemmas are rather big, but nearly fully automatic once everything is corretly defined.
  • In specification the full proof obligations for ASM refinement are shown. They are derived as instances of the generic ASM refinement theory there.
  • Finally, we proves security of the abstract level , and using invariance preservation we also prove security of the communication protocol .