{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:41:12Z","timestamp":1725514872964},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540682356"},{"type":"electronic","value":"9783540682370"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68237-0_13","type":"book-chapter","created":{"date-parts":[[2008,6,4]],"date-time":"2008-06-04T05:36:00Z","timestamp":1212557760000},"page":"165-180","source":"Crossref","is-referenced-by-count":10,"title":["Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code"],"prefix":"10.1007","author":[{"given":"Holger","family":"Grandy","sequence":"first","affiliation":[]},{"given":"Markus","family":"Bischof","sequence":"additional","affiliation":[]},{"given":"Kurt","family":"Stenzel","sequence":"additional","affiliation":[]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48257-1_23","volume-title":"Applied Formal Methods - FM-Trends 98","author":"M. Balser","year":"1999","unstructured":"Balser, M., Reif, W., Schellhorn, G., Stenzel, K.: KIV 3.0 for Provably Correct Systems. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol.\u00a01641, Springer, Heidelberg (1999)"},{"key":"13_CR2","unstructured":"Banach, R., Jeske, C., Poppleton, M., Stepney, S.: Retrenching the purse: The balance enquiry quandary, and generalised and (1,1) forward refinements. Fundamenta Informaticae 77 (2006)"},{"key":"13_CR3","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"issue":"2","key":"13_CR4","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s00165-005-0079-4","volume":"18","author":"J. Bicarregui","year":"2006","unstructured":"Bicarregui, J., Hoare, C.A.R., Woodcock, J.C.P.: The verified software repository: a step towards the verifying compiler. Formal Aspects Computing\u00a018(2), 143\u2013151 (2006)","journal-title":"Formal Aspects Computing"},{"issue":"1\u20132","key":"13_CR5","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":"13_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines\u2014A Method for High-Level System Design and Analysis","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines\u2014A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Rustan, K., Leino, M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer\u00a07(3) (2005)","DOI":"10.1007\/s10009-004-0167-4"},{"key":"13_CR8","unstructured":"UK ITSEC Certification Body. UK ITSEC SCHEME CERTIFICATION REPORT No. P129 MONDEX Purse. Technical report, UK IT Security Evaluation and Certification Scheme (1999)"},{"key":"13_CR9","first-page":"350","volume-title":"Proc. 22th IEEE Symposium on Foundations of Computer Science","author":"D. Dolev","year":"1981","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. In: Proc. 22th IEEE Symposium on Foundations of Computer Science, pp. 350\u2013357. IEEE, Los Alamitos (1981)"},{"key":"13_CR10","volume-title":"The Java Language Specification","author":"J. Gosling","year":"1996","unstructured":"Gosling, J., Joy, B., Steele, G.: The Java Language Specification. Addison-Wesley, Reading (1996)"},{"key":"13_CR11","volume-title":"Software Engineering and Formal Methods, SEFM","author":"H. Grandy","year":"2007","unstructured":"Grandy, H., Bertossi, R., Stenzel, K., Reif, W.: ASN1-light: A Verified Message Encoding for Security Protocols. In: Software Engineering and Formal Methods, SEFM, IEEE Press, Los Alamitos (2007)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/978-3-540-72952-5_14","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"H. Grandy","year":"2007","unstructured":"Grandy, H., Stenzel, K., Reif, W.: A Refinement Method for Java Programs. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol.\u00a04468, pp. 221\u2013235. Springer, Heidelberg (2007)"},{"key":"13_CR13","unstructured":"Haneberg, D.: Sicherheit von Smart Card \u2013 Anwendungen. PhD thesis, University of Augsburg, Augsburg, Germany (in German) (2006)"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-540-73210-5_17","volume-title":"Integrated Formal Methods","author":"D. Haneberg","year":"2007","unstructured":"Haneberg, D., Grandy, H., Reif, W., Schellhorn, G.: Verifying Smart Card Applications: An ASM Approach. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 313\u2013332. Springer, Heidelberg (2007)"},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Haneberg, D., Schellhorn, G., Grandy, H., Reif, W.: Verification of Mondex Electronic Purses with KIV: From Transactions to a Security Protocol. Formal Aspects of Computing\u00a020(1) (January 2008)","DOI":"10.1007\/s00165-007-0057-0"},{"key":"13_CR16","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":"13_CR17","unstructured":"Haxthausen, A.E., George, C., Sch\u00fctz, M.: Specification and Proof of the Mondex Electronic Purse. In: 1st Asian Working Conference on Verified Software, AWCVS 2006, UNU-IIST Reports 348, Macau (2006)"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/11817963_4","volume-title":"Computer Aided Verification","author":"S.T. Hoare","year":"2006","unstructured":"Hoare, S.T.: The Ideal of Verified Software. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 5\u201316. Springer, Heidelberg (2006)"},{"key":"13_CR19","unstructured":"Web presentation of the Mondex case study in KIV. URL, http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/mondex.html"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-540-73210-5_21","volume-title":"Integrated Formal Methods","author":"W. Kong","year":"2007","unstructured":"Kong, W., Ogata, K., Futatsugi, K.: Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 393\u2013412. Springer, Heidelberg (2007)"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Leino, K.R.M., M\u00fcller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Aspects of Computing\u00a019(2) (June 2007)","DOI":"10.1007\/s00165-007-0026-7"},{"key":"13_CR22","unstructured":"MasterCard International Inc., http:\/\/www.mondex.com"},{"issue":"10","key":"13_CR23","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B. Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u201d. IEEE Computer\u00a025(10), 40\u201351 (1992)","journal-title":"IEEE Computer"},{"key":"13_CR24","volume-title":"International Conference on Software Engineering Advances 2007","author":"N. Moebius","year":"2007","unstructured":"Moebius, N., Haneberg, D., Schellhorn, G., Reif, W.: A Modeling Framework for the Development of Provably Secure E-Commerce Applications. In: International Conference on Software Engineering Advances 2007, IEEE Press, Los Alamitos (2007)"},{"key":"13_CR25","doi-asserted-by":"crossref","unstructured":"Ramananadro, T., Jackson, D.: Mondex, an electronic purse: specification and refinement checks with the alloy model-finding method (2006), http:\/\/www.eleves.ens.fr\/home\/ramanana\/work\/mondex\/","DOI":"10.1007\/s00165-007-0058-z"},{"key":"13_CR26","unstructured":"Schellhorn, G.: Verification of ASM Refinements Using Generalized Forward Simulation. Journal of Universal Computer Science (J.UCS)\u00a07(11) (2001)"},{"key":"13_CR27","unstructured":"Schellhorn, G.: ASM Refinement Preserving Invariants. In: Proceedings of the 14th International ASM Workshop, ASM 2007, Grimstad, Norway (2007)"},{"issue":"2-3","key":"13_CR28","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":"13_CR29","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Grandy, H., Haneberg, D., Moebius, N., Reif, W.: A Systematic Verification Approach for Mondex Electronic Purses using ASMs. In: Dagstuhl seminar on Rigorous Methods for Software Construction and Analysis, LNCS. Springer, to appear (older version available as Techn. Report 2006-27 at [19] (2008)","DOI":"10.1007\/978-3-642-11447-2_7"},{"key":"13_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/11813040_2","volume-title":"FM 2006: Formal Methods","author":"G. Schellhorn","year":"2006","unstructured":"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.\u00a04085, pp. 16\u201331. Springer, Heidelberg (2006)"},{"key":"13_CR31","volume-title":"Software Engineering and Formal Methods, SEFM","author":"P.H. Schmitt","year":"2007","unstructured":"Schmitt, P.H., Tonin, I.: Verifying the Mondex case study. In: Software Engineering and Formal Methods, SEFM, IEEE Press, Los Alamitos (2007)"},{"key":"13_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/978-3-540-27815-3_37","volume-title":"Algebraic Methodology and Software Technology","author":"K. Stenzel","year":"2004","unstructured":"Stenzel, K.: A Formally Verified Calculus for Full Java Card. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 491\u2013505. Springer, Heidelberg (2004)"},{"key":"13_CR33","unstructured":"Stenzel, K.: Verification of Java Card Programs. PhD thesis, Universit\u00e4t Augsburg, Fakult\u00e4t f\u00fcr Angewandte Informatik (2005)"},{"key":"13_CR34","unstructured":"Stepney, S., Cooper, D., Woodcock, J.: AN ELECTRONIC PURSE Specification, Refinement, and Proof. Technical monograph PRG-126, Oxford University Computing Laboratory (July 2000)"},{"key":"13_CR35","unstructured":"Sun Microsystems Inc. Java Card 2.2 Specification (2002), http:\/\/java.sun.com\/products\/javacard\/"},{"key":"13_CR36","unstructured":"Tonin, I.: Verifying the mondex case study. The KeY approach. Techischer Bericht 2007-4, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe (2007)"},{"issue":"10","key":"13_CR37","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1109\/MC.2006.340","volume":"39","author":"J. Woodcock","year":"2006","unstructured":"Woodcock, J.: First steps in the verified software grand challenge. IEEE Computer\u00a039(10), 57\u201364 (2006)","journal-title":"IEEE Computer"},{"key":"13_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/11921240_2","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"J. Woodcock","year":"2006","unstructured":"Woodcock, J., Freitas, L.: Z\/Eves and the Mondex Electronic Purse. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol.\u00a04281, pp. 15\u201334. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","FM 2008: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68237-0_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,11]],"date-time":"2021-09-11T15:18:35Z","timestamp":1631373515000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68237-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540682356","9783540682370"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68237-0_13","relation":{},"subject":[]}}