Mondex: Engineering a Provable Secure Electronic Purse
    Download PDF
Dominik Haneberg,Nina Moebius,Wolfgang Reif,Gerhard Schellhorn, and Kurt Stenzel,Kurt Stenzel. Mondex: Engineering a Provable Secure Electronic Purse. International Journal of Software and Informatics, 2011,5(1-2Part1):159~184
Hits: 4005
Download times: 2686
Abstract:Mondex electronic purses are used to replace cash payment by electronic payment with a smart card. Tool-based proofs of an abstract specification of the security protocol used by Mondex cards has been proposed as a challenge for mechanized verification. This paper extends the challenge and describes a comprehensive formal approach for developing Mondex that starts with the abstract specification that was used to certify Mondex, and ends with correct Java code. The development was verified with the theorem prover KIV using several refinements. Mondex cards can also be viewed as a challenge for software engineering a security-critical application. We describe a model-driven tool-supported approach, that uses UML models enhanced with security aspects, and generates correct and secure Java Card code. The UML models can also be used to generate the formal specifications used in KIV.
keywords:electronic purse  security  Mondex  refinement  abstract state machines
View Full Text  View/Add Comment  Download reader



Top Paper  |  FAQ  |  Guest Editors  |  Email Alert  |  Links  |  Copyright  |  Contact Us

© Copyright by Institute of Software, the Chinese Academy of Sciences

京公网安备 11040202500065号