- Suche

- Kontakt

The Mondex Case Study using KIV

Mondex Verification using KIV

The KIV group did a verification of the Mondex case study, which is following and extending the original verification effort of Stepney, Cooper and Woodcock (using Z and pen-and-paper proofs) from 2000.

First we specified two layers of abstraction (A-World and C-World in the orginal work) using Abstract State Machines. We did two refinement proofs for those two layers: One closely following the original work (using the original invariant) and one by developing a more systematic approach to finding invariants.

After establishing correctness on the protocol layer we extended our verification by to more levels, adding cryptography and also adding a real implementation of Mondex using JavaCard. This results in a refinement structure as the figure below:

mondex-layers

The specification on Level 3 follows the Prosecco specification methodology already described here. Publications covering Prosecco in general are also given on this site.

Level 4 is a real implementation of Mondex running on Smart Cards using JavaCard as the implementation language. We also developed a refinement framework for JavaCard implementations, which allows us to carry over security properties proven on the abstract level to the implementation level. A publication describing the refinement framework in general is here.

The different refinement proofs are covered by different publications:

Level 1 to 2: The Mondex Challenge: Machine Checked Proofs for an Electronic Purse (covers verification using the original data refinement and backward simulation) and

A Systematic Verification Approach for Mondex Electronic Purses using ASMs (covers verification using ASM Refinement and a generalized forward simulation) and

A Concept-Driven Construction of the Mondex Protocol using Three Refinements (covers verification as three ASM refinements, each introducing one concept)

Level 2 to 3:Verification of Mondex electronic purses with KIV: from transactions to a security protocol (also covers the extension of the data refinement proof for the refinement from level 1 to 2 to using an archive of exception logs)

Level 3 to 4:Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code

The specific ASM refinement theory used to verify the three refinements of Monex is described in: ASM Refinement Preserving Invariants

You can also view all publications of the GoCard project on this site.

The formal proofs done in those papers are available below.

KIV Projects for Mondex

For all projects done with the KIV system regarding the Mondex case study we provide XML representations of the specifications, theorems and proofs. The project pages can be viewed with most modern web browsers. Best view is provided when using Firefox 2.0, Internet Explorer may have some problems displaying unicode characters for logical symbols.
Currently available projects:

Projects for the refinement from Transactions to the communication protocol:

A technical report describing the Mondex ASM refinement in more detail can be found here .

Projects for the refinement from the communication protocol to the security protocol:

A technical report describing the Prosecco refinement in more detail can be found here .

Projects for the refinement from the security protocol to Java Code:

A technical report describing the implementations in more detail can be found here .

Used basic libraries:

Here you can find all our publications .
Back to the overview of all KIV projects .
For general informations on KIV and a download site for the whole system refer to this page.