{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:35:44Z","timestamp":1725543344670},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540372158"},{"type":"electronic","value":"9783540372165"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11813040_2","type":"book-chapter","created":{"date-parts":[[2006,8,7]],"date-time":"2006-08-07T10:51:03Z","timestamp":1154947863000},"page":"16-31","source":"Crossref","is-referenced-by-count":23,"title":["The Mondex Challenge: Machine Checked Proofs for an Electronic Purse"],"prefix":"10.1007","author":[{"given":"Gerhard","family":"Schellhorn","sequence":"first","affiliation":[]},{"given":"Holger","family":"Grandy","sequence":"additional","affiliation":[]},{"given":"Dominik","family":"Haneberg","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","unstructured":"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"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-39650-5_15","volume-title":"Computer Security \u2013 ESORICS 2003","author":"D. Basin","year":"2003","unstructured":"Basin, D., M\u00f6dersheim, S., Vigan\u00f2, L.: An On-the-Fly Model-Checker for Security Protocol Analysis. In: Snekkenes, E., Gollmann, D. (eds.) ESORICS 2003. LNCS, vol.\u00a02808, pp. 253\u2013270. Springer, Heidelberg (2003)"},{"issue":"1\u20132","key":"2_CR3","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s00165-003-0012-7","volume":"15","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E.: The ASM Refinement Method. Formal Aspects of Computing\u00a015(1\u20132), 237\u2013257 (2003)","journal-title":"Formal Aspects of Computing"},{"key":"2_CR4","series-title":"Studies in Computer Science and Artificial Intelligence","first-page":"20","volume-title":"Logic Programming: Formal Methods and Practical Applications","author":"E. B\u00f6rger","year":"1995","unstructured":"B\u00f6rger, E., Rosenzweig, D.: The WAM\u2014definition and compiler correctness. In: Beierle, C., Pl\u00fcmer, L. (eds.) Logic Programming: Formal Methods and Practical Applications. Studies in Computer Science and Artificial Intelligence, vol.\u00a011, pp. 20\u201390. North-Holland, Amsterdam (1995)"},{"key":"2_CR5","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines\u2014A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)","DOI":"10.1007\/978-3-642-18216-7"},{"key":"2_CR6","unstructured":"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"},{"key":"2_CR7","volume-title":"Proceedings of the 29th Annual Hawaii International Conference on Systems Sciences 1996","author":"E.K. Clemons","year":"1996","unstructured":"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"},{"key":"2_CR8","unstructured":"CoFI (The Common Framework Initiative). In: CASL Reference Manual. LNCS, vol.\u00a02960 (IFIP Series). Springer, Heidelberg (2004)"},{"key":"2_CR9","unstructured":"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"},{"key":"2_CR10","volume-title":"FACIT","author":"J. Derrick","year":"2001","unstructured":"Derrick, J., Boiten, E.: Refinement in Z and in Object-Z: Foundations and Advanced Applications. In: FACIT. Springer, Heidelberg (2001)"},{"key":"2_CR11","first-page":"9","volume-title":"Specification and Validation Methods","author":"Y. Gurevich","year":"1995","unstructured":"Gurevich, Y.: Evolving algebras 1993: Lipari guide. In: B\u00f6rger, E. (ed.) Specification and Validation Methods, pp. 9\u201336. Oxford Univ. Press, Oxford (1995)"},{"key":"2_CR12","unstructured":"Haneberg, D., Grandy, H., Reif, W., Schellhorn, G.: Verifying Security Protocols: An ASM Approach. In: Beauquier, D., B\u00f6rger, E., Slissenko, A. (eds.) 12th Int. Workshop on Abstract State Machines, ASM 2005, University Paris 12 \u2013 Val de Marne, Cr\u00e9teil, France (March 2005)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","first-page":"187","volume-title":"ESOP 86","author":"H. Jifeng","year":"1986","unstructured":"Jifeng, H., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol.\u00a0213, pp. 187\u2013196. Springer, Heidelberg (1986)"},{"key":"2_CR14","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"2_CR15","unstructured":"Web presentation of the mondex case study in KIV, URL: http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/mondex.html"},{"key":"2_CR16","first-page":"147","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: TACAS 1996, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"key":"2_CR17","unstructured":"MasterCard International Inc. Mondex. URL: http:\/\/www.mondex.com"},{"key":"2_CR18","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L.C. Paulson","year":"1998","unstructured":"Paulson, L.C.: The Inductive Approach to Verifying Cryptographic Protocols. J. Computer Security\u00a06, 85\u2013128 (1998)","journal-title":"J. Computer Security"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45744-5_2","volume-title":"Automated Reasoning","author":"L.C. Paulson","year":"2001","unstructured":"Paulson, L.C.: Verifying the SET Protocol. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS, vol.\u00a02083. Springer, Heidelberg (2001)"},{"key":"2_CR20","doi-asserted-by":"publisher","DOI":"10.1002\/047085670X","volume-title":"Smart Card Handbook","author":"W. Rankl","year":"2003","unstructured":"Rankl, W., Effing, W.: Smart Card Handbook, 3rd edn. John Wiley & Sons, Chichester (2003)","edition":"3"},{"key":"2_CR21","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/978-94-017-0435-9_1","volume-title":"Automated Deduction\u2014A Basis for Applications: Systems and Implementation Techniques, chapter 1: Interactive Theorem Proving","author":"W. Reif","year":"1998","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2014A Basis for Applications: Systems and Implementation Techniques, chapter 1: Interactive Theorem Proving, pp. 13\u201339. Kluwer Academic Publishers, Dordrecht (1998)"},{"issue":"4","key":"2_CR22","first-page":"377","volume":"3","author":"G. Schellhorn","year":"1997","unstructured":"Schellhorn, G., Ahrendt, W.: Reasoning about Abstract State Machines: The WAM Case Study. Journal of Universal Computer Science (J.UCS)\u00a03(4), 377\u2013413 (1997), URL: http:\/\/hyperg.iicm.tu-graz.ac.at\/jucs\/","journal-title":"Journal of Universal Computer Science (J.UCS)"},{"key":"2_CR23","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/978-94-017-0437-3_7","volume-title":"Automated Deduction\u2014A Basis for Applications","author":"G. Schellhorn","year":"1998","unstructured":"Schellhorn, G., Ahrendt, W.: The WAM Case Study: Verifying Compiler Correctness for Prolog with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2014A Basis for Applications, pp. 165\u2013194. Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"2_CR24","unstructured":"Schellhorn, G.: Verification of Abstract State Machines. PhD thesis, Universit\u00e4t Ulm, Fakult\u00e4t f\u00fcr Informatik (1999), URL: http:\/\/www.informatik.uni-augsburg.de\/lehrstuehle\/swt\/se\/publications\/"},{"issue":"11","key":"2_CR25","first-page":"952","volume":"7","author":"G. Schellhorn","year":"2001","unstructured":"Schellhorn, G.: Verification of ASM Refinements Using Generalized Forward Simulation. Journal of Universal Computer Science (J.UCS)\u00a07(11), 952\u2013979 (2001), URL: http:\/\/hyperg.iicm.tu-graz.ac.at\/jucs\/","journal-title":"Journal of Universal Computer Science (J.UCS)"},{"issue":"2-3","key":"2_CR26","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1016\/j.tcs.2004.11.013","volume":"336","author":"G. Schellhorn","year":"2005","unstructured":"Schellhorn, G.: ASM Refinement and Generalizations of Forward Simulation in Data Refinement: A Comparison. Journal of Theoretical Computer Science\u00a0336(2-3), 403\u2013435 (2005)","journal-title":"Journal of Theoretical Computer Science"},{"key":"2_CR27","unstructured":"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"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Grandy, H., Haneberg, D., Reif, W.: The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. Technical Report 2006-2, Universit\u00e4t Augsburg (2006)","DOI":"10.1007\/11813040_2"},{"key":"2_CR29","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edn. (1992)"},{"key":"2_CR30","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z: Specification, Proof and Refinement. Prentice Hall International Series in Computer Science (1996)"},{"key":"2_CR31","unstructured":"Woodcock, J.: Mondex case study (2006), URL: http:\/\/qpq.csl.sri.com\/vsr\/shared\/MondexCaseStudy\/"}],"container-title":["Lecture Notes in Computer Science","FM 2006: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11813040_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:14:20Z","timestamp":1605644060000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11813040_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540372158","9783540372165"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/11813040_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}