Abstract
Mondex is a payment system that utilizes smart cards as electronic purses for financial transactions. This paper first reports on how the Mondex system can be modeled, specified and interactively verified using an equation-based method – the OTS/CafeOBJ method. Afterwards, the paper reports on, as a complementarity, a way of automatically falsifying the OTS/CafeOBJ specification of the Mondex system, and how the falsification can be used to facilitate the verification. Differently from related work, our work provides alternative ways of (1) modeling the Mondex system using an OTS (Observational Transition System), a kind of transition system, and (2) expressing and verifying (and falsifying) the desired security properties of the Mondex system directly in terms of invariants of the OTS.
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.
References
MasterCard International Inc. Mondex. URL: http://www.mondex.com/.
Mondex Case Study. URL: http://qpq.csl.sri.com/vsr/private/repository/MondexCaseStudy
UK Computing Research Committee, Grand Challenges in Computer Research. URL: http://www.ukcrc.org.uk/grand_challenges/index.cfm
Woodcock, J.: Grand Challenges 6: Dependable Systems Evolution. URL: http://www.fmnet.info/gc6/
Schellhorn, G., Grandy, H., Haneberg, D., Reif, W.: The Mondex challenge: machine checked proofs for an electronic purse. Technical Report, University of Augsburg (2006)
Schellhorn, G., Grandy, H., Haneberg, D., Reif, W.: The Mondex challenge: machine checked proofs for an electronic purse. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 16–31. Springer, Heidelberg (2006)
Haxthausen, A., George, C., Schütz, M.: Specification and proof of the Mondex electronic purse. In: AWCVS 2006, UNU-IIST Report No. 347, pp. 209–224 ( 2006)
Ramananandro, T.: Mondex, An Electronic Purse: Specification and refinement checks with the Alloy model-finding method. Internship Report (2006), http://www.eleves.ens.fr/home/ramanana/work/mondex/
Stepney, S., Cooper, D., Woodcock, J.: An electronic purse specification, refinement, and proof. Technical monograph PRG-126, Oxford University Computing Laboratory (July 2000)
Ogata, K., Futatsugi, K.: Proof scores in the OTS/CafeOBJ method. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 170–184. Springer, Heidelberg (2003)
CafeOBJ Web Site (2007), URL: http://www.ldl.jaist.ac.jp/cafeobj/
Diaconescu, R., Futatsugi, R.K.: CafeOBJ report. AMAST Series in Computing, vol. 6. World Scientific, Singapore (1998)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude manual (Version 2.2) (2007), URL: http://maude.cs.uiuc.edu/maude2-manual/
Nakamura, M., Kong, W., Ogata, K., Futatsugi, K.: A complete specification translation from OTS/CafeOBJ into OTS/Maude. In: IEICE TR, SS2006, vol. 13, pp. 1–6 (2006)
Kong, W., Ogata, K., Futatsugi, K.: A lightweight integration of theorem proving and model checking for system verification. In: APSEC 2005, pp. 59–66. IEEE CS, Washington, DC (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kong, W., Ogata, K., Futatsugi, K. (2007). Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System. In: Davies, J., Gibbons, J. (eds) Integrated Formal Methods. IFM 2007. Lecture Notes in Computer Science, vol 4591. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73210-5_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-73210-5_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73209-9
Online ISBN: 978-3-540-73210-5
eBook Packages: Computer ScienceComputer Science (R0)