Verifying the Mondex Case Study

12 years 2 months ago
Verifying the Mondex Case Study
The Mondex Case study is still the most substantial contribution to the Grand Challenge repository. It has been the target of a number of formal verification efforts. Those efforts concentrated on correctness proofs for refinement steps of the specification in various specification formalisms using different verification tools. In this paper we report on a Java Card implementation of the Mondex protocol and on proving its correctness using the KeY tool. The security properties to be proved are formalised in the Java Modelling Language and follow as closely as possible the concrete layer of the previous Z specification. This work demonstrates that with an appropriate specification language and verification tool, it is possible to bridge the gap between specification and implementation ensuring a fully verified result.
Peter H. Schmitt, Isabel Tonin
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where SEFM
Authors Peter H. Schmitt, Isabel Tonin
Comments (0)