{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:47:32Z","timestamp":1725544052714},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540346401"},{"type":"electronic","value":"9783540346425"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11766155_9","type":"book-chapter","created":{"date-parts":[[2006,5,31]],"date-time":"2006-05-31T15:35:00Z","timestamp":1149089700000},"page":"115-129","source":"Crossref","is-referenced-by-count":6,"title":["Developing Provable Secure M-Commerce Applications"],"prefix":"10.1007","author":[{"given":"Holger","family":"Grandy","sequence":"first","affiliation":[]},{"given":"Dominik","family":"Haneberg","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[]},{"given":"Kurt","family":"Stenzel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0015258","volume-title":"Computer Science Today","author":"R. Anderson","year":"1995","unstructured":"Anderson, R., Needham, R.: Programming Satan\u2019s Computer. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol.\u00a01000, Springer, Heidelberg (1995)"},{"doi-asserted-by":"crossref","unstructured":"Burrows, M., Abadi, M., Needham, R.: A logic of authentication. Proceedings of the Royal Society of London (Series A, 426, 1871) (1989)","key":"9_CR2","DOI":"10.1145\/74850.74852"},{"key":"9_CR3","first-page":"273","volume-title":"Proceedings of the International conference of Integrated Formal Methods (IFM)","author":"C. Bolton","year":"1999","unstructured":"Bolton, C., Davies, J., Woodcock, J.C.P.: On the refinement and simulation of data types and processes. In: Araki, K., Galloway, A., Taguchi, K. (eds.) Proceedings of the International conference of Integrated Formal Methods (IFM), pp. 273\u2013292. Springer, Heidelberg (1999)"},{"unstructured":"Tickets on your Mobile (last seen March 16, 2006), \n                    \n                      http:\/\/www.beep.nl","key":"9_CR4"},{"key":"9_CR5","first-page":"180","volume-title":"MobiCom 2001: Proceedings of the 7th annual international conference on Mobile computing and networking","author":"N. Borisov","year":"2001","unstructured":"Borisov, N., Goldberg, I., Wagner, D.: Intercepting Mobile Mommunications: The Insecurity of 802.11. In: MobiCom 2001: Proceedings of the 7th annual international conference on Mobile computing and networking, pp. 180\u2013189. ACM Press, New York (2001)"},{"key":"9_CR6","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":"9_CR7","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":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-46428-X_25","volume-title":"Fundamental Approaches to Software Engineering","author":"M. Balser","year":"2000","unstructured":"Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal System Development with KIV. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol.\u00a01783, p. 363. Springer, Heidelberg (2000)"},{"key":"9_CR9","doi-asserted-by":"publisher","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":"9_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":"9_CR11","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511663079","volume-title":"Data Refinement: Model-Oriented Proof Methods and their Comparison","author":"W. Roever de","year":"1998","unstructured":"de Roever, W., Engelhardt, K.: Methods of Algorithmic Language Implementation. Cambridge Tracts in Theoretical Computer Science, vol.\u00a047. Cambridge University Press, Cambridge (1998)"},{"doi-asserted-by":"crossref","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory\u00a029 (1983)","key":"9_CR12","DOI":"10.1109\/TIT.1983.1056650"},{"key":"9_CR13","volume-title":"SEFM 2005 \u2013 3rd IEEE International Conference on Software Engineering and Formal Methods","author":"H. Grandy","year":"2005","unstructured":"Grandy, H., Stenzel, K., Reif, W.: Object-Oriented Verification Kernels for Secure Java Applications. In: Aichering, B., Beckert, B. (eds.) SEFM 2005 \u2013 3rd IEEE International Conference on Software Engineering and Formal Methods. IEEE Press, Los Alamitos (2005)"},{"key":"9_CR14","first-page":"9","volume-title":"Specification and Validation Methods","author":"M. Gurevich","year":"1995","unstructured":"Gurevich, M.: Evolving algebras 1993: Lipari guide. In: B\u00f6rger, E. (ed.) Specification and Validation Methods, pp. 9\u201336. Oxford University Press, Oxford (1995)"},{"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":"9_CR15"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-16442-1_14","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":"9_CR17","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":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/3-540-45719-4_22","volume-title":"Algebraic Methodology and Software Technology","author":"D. Haneberg","year":"2002","unstructured":"Haneberg, D., Reif, W., Stenzel, K.: A Method for Secure Smartcard Applications. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, p. 319. Springer, Heidelberg (2002)"},{"unstructured":"Web presentation of KIV projects, \n                    \n                      http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/","key":"9_CR19"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"issue":"2","key":"9_CR21","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0743-1066(95)00095-X","volume":"26","author":"C. Meadows","year":"1996","unstructured":"Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming\u00a026(2), 113\u2013131 (1996)","journal-title":"Journal of Logic Programming"},{"key":"9_CR22","doi-asserted-by":"publisher","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. Journal of Computer Security\u00a06, 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"issue":"11","key":"9_CR23","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), \n                    \n                      http:\/\/hyperg.iicm.tu-graz.ac.at\/jucs\/","journal-title":"Journal of Universal Computer Science (J.UCS)"},{"issue":"2-3","key":"9_CR24","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":"9_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"unstructured":"Stenzel, K.: Verification of Java Card Programs. PhD thesis, Universit\u00e4t Augsburg, Fakult\u00e4t f\u00fcr Angewandte Informatik (2005), \n                    \n                      http:\/\/www.opus-bayern.de\/uni-augsburg\/volltexte\/2005\/122\/","key":"9_CR26"},{"unstructured":"Sun Microsystems Inc. Java Micro Edition, \n                    \n                      http:\/\/java.sun.com\/j2me\/index.jsp","key":"9_CR27"},{"unstructured":"Woodcock, J.C.P., Davies, J.: Using Z: Specification, Proof and Refinement. Prentice Hall International Series in Computer Science (1996)","key":"9_CR28"},{"unstructured":"Wagner, D., Schneier, B.: Analysis of the SSL 3.0 protocol. In: 2nd USENIX Workshop on Electronic Commerce, (November 1996) (A revised version is available at), \n                    \n                      http:\/\/www.schneier.com\/paper-ssl.html","key":"9_CR29"}],"container-title":["Lecture Notes in Computer Science","Emerging Trends in Information and Communication Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11766155_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,11]],"date-time":"2019-03-11T23:20:31Z","timestamp":1552346431000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11766155_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540346401","9783540346425"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/11766155_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}