Abstract
The Mondex case study about the specification and refinement of an electronic purse as defined in [SCJ00] has recently been proposed as a challenge for formal system-supported verification. This paper reports on the successful verification of the major part of the case study using the KIV specification and verification system. We demonstrate that even though the hand-made proofs were elaborated to an enormous level of detail, we still could find small errors in the underlying data refinement theory as well as the formal proofs of the case study.
We also provide an alternative formalisation of the communication protocol using abstract state machines.
Finally the Mondex case study verifies functional correctness assuming a suitable security protocol. Therefore we propose to extend the case study to include the verification of a suitable security protocol.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bellare, M., Garay, J., Jutla, C., Yung, M.: VarietyCash: a Multi-purpose Electronic Payment System. In: Proceedings of the 3rd USENIX Workshop on Electronic Commerce, USENIX (September 1998), http://citeseer.ist.psu.edu/bellare98varietycash.html
Basin, D., Mödersheim, S., Viganò, L.: An On-the-Fly Model-Checker for Security Protocol Analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol. 2808, pp. 253–270. Springer, Heidelberg (2003)
Börger, E.: The ASM Refinement Method. Formal Aspects of Computing 15(1–2), 237–257 (2003)
Börger, E., Rosenzweig, D.: The WAM—definition and compiler correctness. In: Beierle, C., Plümer, L. (eds.) Logic Programming: Formal Methods and Practical Applications. Studies in Computer Science and Artificial Intelligence, vol. 11, pp. 20–90. North-Holland, Amsterdam (1995)
Börger, E., Stärk, R.F.: Abstract State Machines—A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
UK ITSEC Certification Body. UK ITSEC SCHEME CERTIFICATION REPORT No. P129 MONDEX Purse. Technical report, UK IT Security Evaluation and Certification Scheme (1999), URL: http://www.cesg.gov.uk/site/iacs/itsec/media/certreps/CRP129.pdf
Clemons, E.K., Croson, D.C., Weber, B.W.: Reengineering Money: The Mondex Stored Value Card and Beyond. In: Proceedings of the 29th Annual Hawaii International Conference on Systems Sciences 1996. IEEE, Los Alamitos (1996), URL: http://doi.ieeecomputersociety.org/10.1109/HICSS.1996.495345
CoFI (The Common Framework Initiative). In: CASL Reference Manual. LNCS, vol. 2960 (IFIP Series). Springer, Heidelberg (2004)
Cooper, D., Stepney, S., Woodcock, J.: Derivation of Z Refinement Proof Rules: forwards and backwards rules incorporating input/output refinement. Technical Report YCS-2002-347, University of York (2002), URL: http://www-users.cs.york.ac.uk/~susan/bib/ss/z/zrules.htm
Derrick, J., Boiten, E.: Refinement in Z and in Object-Z: Foundations and Advanced Applications. In: FACIT. Springer, Heidelberg (2001)
Gurevich, Y.: Evolving algebras 1993: Lipari guide. In: Börger, E. (ed.) Specification and Validation Methods, pp. 9–36. Oxford Univ. Press, Oxford (1995)
Haneberg, D., Grandy, H., Reif, W., Schellhorn, G.: Verifying Security Protocols: An ASM Approach. In: Beauquier, D., Börger, E., Slissenko, A. (eds.) 12th Int. Workshop on Abstract State Machines, ASM 2005, University Paris 12 – Val de Marne, Créteil, France (March 2005)
Jifeng, H., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Web presentation of the mondex case study in KIV, URL: http://www.informatik.uni-augsburg.de/swt/projects/mondex.html
Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: TACAS 1996, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
MasterCard International Inc. Mondex. URL: http://www.mondex.com
Paulson, L.C.: The Inductive Approach to Verifying Cryptographic Protocols. J. Computer Security 6, 85–128 (1998)
Paulson, L.C.: Verifying the SET Protocol. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol. 2083. Springer, Heidelberg (2001)
Rankl, W., Effing, W.: Smart Card Handbook, 3rd edn. John Wiley & Sons, Chichester (2003)
Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction—A Basis for Applications: Systems and Implementation Techniques, chapter 1: Interactive Theorem Proving, pp. 13–39. Kluwer Academic Publishers, Dordrecht (1998)
Schellhorn, G., Ahrendt, W.: Reasoning about Abstract State Machines: The WAM Case Study. Journal of Universal Computer Science (J.UCS) 3(4), 377–413 (1997), URL: http://hyperg.iicm.tu-graz.ac.at/jucs/
Schellhorn, G., Ahrendt, W.: The WAM Case Study: Verifying Compiler Correctness for Prolog with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction—A Basis for Applications, pp. 165–194. Kluwer Academic Publishers, Dordrecht (1998)
Schellhorn, G.: Verification of Abstract State Machines. PhD thesis, Universität Ulm, Fakultät für Informatik (1999), URL: http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/publications/
Schellhorn, G.: Verification of ASM Refinements Using Generalized Forward Simulation. Journal of Universal Computer Science (J.UCS) 7(11), 952–979 (2001), URL: http://hyperg.iicm.tu-graz.ac.at/jucs/
Schellhorn, G.: ASM Refinement and Generalizations of Forward Simulation in Data Refinement: A Comparison. Journal of Theoretical Computer Science 336(2-3), 403–435 (2005)
Stepney, S., Cooper, D., Woodcock, J.: An Electronic Purse Specification, Refinement, and Proof. Technical monograph PRG-126, Oxford University Computing Laboratory (July 2000), URL: http://www-users.cs.york.ac.uk/~susan/bib/ss/z/monog.htm
Schellhorn, G., Grandy, H., Haneberg, D., Reif, W.: The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. Technical Report 2006-2, Universität Augsburg (2006)
Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edn. (1992)
Woodcock, J.C.P., Davies, J.: Using Z: Specification, Proof and Refinement. Prentice Hall International Series in Computer Science (1996)
Woodcock, J.: Mondex case study (2006), URL: http://qpq.csl.sri.com/vsr/shared/MondexCaseStudy/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schellhorn, G., Grandy, H., Haneberg, D., Reif, W. (2006). The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. In: Misra, J., Nipkow, T., Sekerinski, E. (eds) FM 2006: Formal Methods. FM 2006. Lecture Notes in Computer Science, vol 4085. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11813040_2
Download citation
DOI: https://doi.org/10.1007/11813040_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37215-8
Online ISBN: 978-3-540-37216-5
eBook Packages: Computer ScienceComputer Science (R0)