Abstract
This paper describes how the communication protocol of Mondex electronic purses can be specified and verified against desired security properties. The specification is developed by stepwise refinement using the RAISE formal specification language, RSL, and the proofs are made by translation to PVS and SAL. The work is part of a year-long project contributing to the international grand challenge in verified software engineering.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Ahn U, George C (2000) C++ Translator for RAISE Specification Language. Technical Report 331, UNU-IIST, P.O.Box 3058, Macau, November 2000
Bicarregui J, Hoare CAR, Woodcock JCP (2006) The verified software repository: a step towards the verifying compiler. Formal Aspects Comput 18(2):143–151
Dasso A, George CW (2002) Transforming RSL into PVS. Technical Report 256, UNU/IIST, P.O. Box 3058, Macau, May 2002
de Moura L, Owre S, Shankar N (2003) The SAL language manual. Technical Report SRI-CSL-01-02, SRI International, 2003. Available from http://sal.csl.sri.com
The Mondex Challenge Project. Special Issue. Formal Aspects Comput J
George C, Haxthausen AE (2007) Specification, proof, and model checking of the Mondex Electronic Purse using RAISE. Technical Report 352, UNU-IIST, P.O.Box 3058, Macau, February 2007
Hoare T, Milner R (2005) Grand challenges for computing research. Comput J 48(1):49–52
Hoare CAR (2003) The verifying compiler: a grand challenge for computing research. J ACM 50(1):63–69
Hoare T (2006) The ideal of verified software. In 18th international conference on computer aided verification (CAV2006), vol 4144 of Lecture Notes in Computer Science, Seattle, August 2006. Springer, Heidelberg
Ives B, Earl M (1997) Mondex international: Reengineering money. Technical Report CRIM CS97/2, London Business School
MasterCard International Incorporated. Mondex
Jones C, O’Hearn PW, Woodcock J (2006) Verified software: a grand challenge. IEEE Comput 39(4):93–95
Mondex’s Pilot System Broken. http://jya.com/mondex-hack.htm, September 1997
Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: Kapur D (ed) 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence. Saratoga, June 1992. Springer, Heidelberg, pp 748–752
Perna JI, George C (2006) Model checking RAISE specifications. Technical Report 331, UNU-IIST, P.O.Box 3058, Macau, November 2006
The RAISE Language Group (1992) The RAISE specification language. BCS Practitioner Series. Prentice Hall, Englewood Cliffs
The RAISE Method Group (1995) The RAISE development method. BCS Practitioner series. Prentice Hall, Englewood Cliffs. Available by ftp from ftp://ftp.iist.unu.edu/pub/RAISE/method_book
Stepney S, Cooper D, Woodcock JCP (2000) An electronic purse: specification, refinement, and proof. Technical Monograph PRG-126, Oxford University Computing Laboratory
Spivey JM (1992) The Z Notation: a reference manual, 2nd edn. Prentice Hall International Series in Computer Science, Englewood Cliffs
Woodcock J, Freitas L (2006) Z/Eves and the Mondex electronic purse. In: Theoretical aspects of computing—ICTAC 2006, third international colloquium, vol 4281 of Lecture Notes in Computer Science, Tunis, November 2006. Springer, Heidelberg, pp 15–34
Woodcock J (2006) First steps in the verified software grand challenge. IEEE Comput 39(10):57–64
Author information
Authors and Affiliations
Corresponding author
Additional information
J. C. P. Woodcock
Rights and permissions
About this article
Cite this article
George, C., Haxthausen, A.E. Specification, proof, and model checking of the Mondex electronic purse using RAISE. Form Asp Comp 20, 101–116 (2008). https://doi.org/10.1007/s00165-007-0054-3
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-007-0054-3