Title :
Verifying the Mondex Case Study
Author :
Schmitt, Peter H. ; Tonin, Isabel
Author_Institution :
Univ. Karlsruhe Inst., Karlsruhe
Abstract :
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.
Keywords :
Java; formal specification; program verification; safety-critical software; security of data; specification languages; Java modelling language; Mondex protocol; Z specification language; data security; formal specification; formal verification; software reliability; Computer science; Concrete; Contracts; Cryptographic protocols; Formal verification; Java; Software engineering; Software safety; Specification languages; Writing;
Conference_Titel :
Software Engineering and Formal Methods, 2007. SEFM 2007. Fifth IEEE International Conference on
Conference_Location :
London
Print_ISBN :
978-0-7695-2884-7
DOI :
10.1109/SEFM.2007.47