The Mondex Case Study: From Specifications to Code

H. Grandy, N. Moebius, M. Bischof, D. Haneberg, G. Schellhorn, K. Stenzel, W. Reif

The Mondex Case Study: From Specifications to Code

In this paper we introduce three different implementations for the Mondex electronic purse verification challenge [Woo06] [SCW00]. In previous work ([SGHR06] [SGH+07] and [HSGR06]) we verified security and correctness properties of the Mondex money transfer protocol. Here we present a way to translate the formal specifications into running JavaCard code. We introduce three different ways to implement the protocol, one using symmetric cryptography, one using asymmetric cryptography and finally one using special datatypes for cryptographic protocols and symmetric cryptography. All implementations presented in this paper are able to run on a Gemplus GemxpressoRAD ProR3 SmartCard.

published 13.12.2006 in: Universit├Ąt Augsburg, Technical Report 2006-31 Technical Report, Institute of Computer Science, University of Augsburg, December 2006


For questions regarding the publication, please contact!