| 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: 4402 |
| Download times: 3497 |
|
|
| 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 |
|
|
|
