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 Javacard 
implementation of the Mondex protocol and on proving its correctness 
using the KeY tool. The safety  properties to be proved are formalized in
the Java Modeling Language and follow as closely as possible the concrete
layer of the previous Z specification.