More Web Proxy on the site http://driver.im/

research-article

Open access

Specification, proof, and model checking of the Mondex electronic purse using RAISE

Authors:

Anne E. HaxthausenAuthors Info & Claims

Formal Aspects of Computing, Volume 20, Issue 1

Pages 101 - 116

https://doi.org/10.1007/s00165-007-0054-3

Published: 01 January 2008 Publication History

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.

References

References

[1]

Ahn U, George C (2000) C++ Translator for RAISE Specification Language. Technical Report 331, UNU-IIST, P.O.Box 3058, Macau, November 2000

[2]

Bicarregui J, Hoare CAR, and Woodcock JCP The verified software repository: a step towards the verifying compiler Formal Aspects Comput 2006 18 2 143-151

Digital Library

[3]

Dasso A, George CW (2002) Transforming RSL into PVS. Technical Report 256, UNU/IIST, P.O. Box 3058, Macau, May 2002

[4]

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

[5]

The Mondex Challenge Project. Special Issue. Formal Aspects Comput J

[6]

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

[7]

Hoare T and Milner R Grand challenges for computing research Comput J 2005 48 1 49-52

Digital Library

[8]

Hoare CAR The verifying compiler: a grand challenge for computing research J ACM 2003 50 1 63-69

Digital Library

[9]

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

[10]

Ives B, Earl M (1997) Mondex international: Reengineering money. Technical Report CRIM CS97/2, London Business School

[11]

MasterCard International Incorporated. Mondex

[12]

ITSEC. http://en.wikipedia.org/wiki/ITSEC

[13]

Jones C, O’Hearn PW, and Woodcock J Verified software: a grand challenge IEEE Comput 2006 39 4 93-95

Digital Library

[14]

Mondex’s Pilot System Broken. http://jya.com/mondex-hack.htm, September 1997

[15]

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

[16]

Perna JI, George C (2006) Model checking RAISE specifications. Technical Report 331, UNU-IIST, P.O.Box 3058, Macau, November 2006

[17]

The RAISE Language Group (1992) The RAISE specification language. BCS Practitioner Series. Prentice Hall, Englewood Cliffs

[18]

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

[19]

Stepney S, Cooper D, Woodcock JCP (2000) An electronic purse: specification, refinement, and proof. Technical Monograph PRG-126, Oxford University Computing Laboratory

[20]

Spivey JM The Z Notation: a reference manual 1992 2 Englewood Cliffs Prentice Hall International Series in Computer Science

Digital Library

[21]

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

[22]

Woodcock J First steps in the verified software grand challenge IEEE Comput 2006 39 10 57-64

Digital Library

Cited By

Cornejo CRegis GAguirre NFrias M(2023)A Study of the Electrum and DynAlloy Dynamic Behavior NotationsIEEE Transactions on Software Engineering10.1109/TSE.2023.332062549:11(4946-4963)Online publication date: 29-Sep-2023
https://dl.acm.org/doi/10.1109/TSE.2023.3320625
Zhang MOgata K(2018)From hidden to visible: A unified framework for transforming behavioral theories into rewrite theoriesTheoretical Computer Science10.1016/j.tcs.2018.01.006722(52-75)Online publication date: Apr-2018
https://doi.org/10.1016/j.tcs.2018.01.006
Ogata K(2017)Model checking the i KP electronic payment protocolsJournal of Information Security and Applications10.1016/j.jisa.2017.08.00636(101-111)Online publication date: Oct-2017
https://doi.org/10.1016/j.jisa.2017.08.006
Show More Cited By

Recommendations

Verification of Mondex electronic purses with KIV: from transactions to a security protocol
Abstract
The Mondex case study about the specification and refinement of an electronic purse as defined in the Oxford Technical Monograph PRG-126 has recently been proposed as a challenge for formal system-supported verification. In this paper we report on ...
Model Checking LTL Formulae in RAISE with FDR
IFM '09: Proceedings of the 7th International Conference on Integrated Formal Methods

The Raise Specification Language (RSL) is a modeling language which supports various specification styles. To apply model checking to RSL concurrent descriptions, we translate RSL specifications into the input language CSPM of FDR. FDR is the model ...
The certification of the Mondex electronic purse to ITSEC Level E6
Abstract.
Ten years ago the Mondex electronic purse was certified to ITSEC Level E6, the highest level of assurance for secure systems. This involved building formal models in the Z notation, linking them with refinement, and proving that they correctly ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 20, Issue 1

Jan 2008

134 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© British Computer Society 2007.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 January 2008

Accepted: 29 October 2007

Revision received: 19 June 2007

Received: 19 January 2007

Published in FAC Volume 20, Issue 1

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

16
Total Citations
View Citations
52
Total Downloads

Downloads (Last 12 months)28
Downloads (Last 6 weeks)6

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Cornejo CRegis GAguirre NFrias M(2023)A Study of the Electrum and DynAlloy Dynamic Behavior NotationsIEEE Transactions on Software Engineering10.1109/TSE.2023.332062549:11(4946-4963)Online publication date: 29-Sep-2023
https://dl.acm.org/doi/10.1109/TSE.2023.3320625
Zhang MOgata K(2018)From hidden to visible: A unified framework for transforming behavioral theories into rewrite theoriesTheoretical Computer Science10.1016/j.tcs.2018.01.006722(52-75)Online publication date: Apr-2018
https://doi.org/10.1016/j.tcs.2018.01.006
Ogata K(2017)Model checking the i KP electronic payment protocolsJournal of Information Security and Applications10.1016/j.jisa.2017.08.00636(101-111)Online publication date: Oct-2017
https://doi.org/10.1016/j.jisa.2017.08.006
Cheng SWoodcock JD’Souza D(2015)Using formal reasoning on a model of tasks for FreeRTOSFormal Aspects of Computing10.1007/s00165-014-0308-927:1(167-192)Online publication date: 1-Jan-2015
https://dl.acm.org/doi/10.1007/s00165-014-0308-9
Woodcock JCavalcanti AFitzgerald JFoster SLarsen P(2014)Contracts in CMLLeveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications10.1007/978-3-662-45231-8_5(54-73)Online publication date: 2014
https://doi.org/10.1007/978-3-662-45231-8_5
Perna JGeorge C(2013)Model checking RAISE applicative specificationsFormal Aspects of Computing10.1007/s00165-011-0217-025:3(365-388)Online publication date: 1-May-2013
https://dl.acm.org/doi/10.1007/s00165-011-0217-0
Banach RJeske CHall AStepney S(2013)Atomicity failure and the retrenchment atomicity patternFormal Aspects of Computing10.1007/s00165-011-0216-125:3(439-464)Online publication date: 1-May-2013
https://dl.acm.org/doi/10.1007/s00165-011-0216-1
OGATA KFUTATSUGI K(2012)PROOF SCORE APPROACH TO ANALYSIS OF ELECTRONIC COMMERCE PROTOCOLSInternational Journal of Software Engineering and Knowledge Engineering10.1142/S021819401000471220:02(253-287)Online publication date: 30-Apr-2012
https://doi.org/10.1142/S0218194010004712
da Costa UMoreira AMusicante MSouza Neto P(2012)JCMLScience of Computer Programming10.1016/j.scico.2010.03.00377:4(533-550)Online publication date: 1-Apr-2012
https://dl.acm.org/doi/10.1016/j.scico.2010.03.003
Kordzakhia GL.Shengelia Tvauri GTatishvili MMkurnalidze I(2011)Remote sensing for early warning of natural meteorological and hydrological disasters and provision of transportation safety over the Black Sea in GeorgiaProcedia - Social and Behavioral Sciences10.1016/j.sbspro.2011.05.16619(532-536)Online publication date: 2011
https://doi.org/10.1016/j.sbspro.2011.05.166
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents