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.
The article Mondex: engineering a provable secure electronic purse is a summary over all our work.
Work started by specifying the 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 two more levels, adding cryptography and also adding a real implementation of Mondex using JavaCard. This results in a refinement structure as the figure below:
The specification on Level 3 follows the general approach developed in the Go!Card and project to verify security critical smart card applications.
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 Mondex is described in: ASM Refinement Preserving InvariantsMondex has been used as an example for our Model Driven Development Approach for Security Protocols called SecureMDD. You can jump to the Mondex Models directly.
The formal proofs done in those papers are available below.
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: