{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:18:00Z","timestamp":1725491880720},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540732099"},{"type":"electronic","value":"9783540732105"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73210-5_17","type":"book-chapter","created":{"date-parts":[[2007,9,13]],"date-time":"2007-09-13T04:03:05Z","timestamp":1189656185000},"page":"313-332","source":"Crossref","is-referenced-by-count":7,"title":["Verifying Smart Card Applications: An ASM Approach"],"prefix":"10.1007","author":[{"given":"Dominik","family":"Haneberg","sequence":"first","affiliation":[]},{"given":"Holger","family":"Grandy","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","volume-title":"Workshop on Logical Aspects of Cryptographic Protocol Verification","author":"R. Accorsi","year":"2001","unstructured":"Accorsi, R., Basin, D., Vigan\u00f2, L.: Towards an awareness-based semantics for security protocol analysis. In: Goubault-Larrecq, J. (ed.) Workshop on Logical Aspects of Cryptographic Protocol Verification, Elsevier, Amsterdam (2001)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-58843-4","volume-title":"Computer Science Today: Recent Trends and Developments","author":"R.J. Anderson","year":"1995","unstructured":"Anderson, R.J., Needham, R.M.: Programming Satan\u2019s Computer. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol.\u00a01000, Springer, Heidelberg (1995)"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Burrows, M., Abadi, M., Needham, R.M.: A Logic of Authentication. Technical report, SRC Research Report 39 (1989)","DOI":"10.1145\/74850.74852"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45418-7_3","volume-title":"Smart Card Programming and Security","author":"G. Bella","year":"2001","unstructured":"Bella, G.: Mechanising a Protocol for Smart Cards. In: Attali, S., Jensen, T. (eds.) E-smart 2001. LNCS, vol.\u00a02140, Springer, Heidelberg (2001)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E.: The ASM Refinement Method. Formal Aspects of Computing, 15(1-2) (2003)","DOI":"10.1007\/s00165-003-0012-7"},{"issue":"12","key":"17_CR7","first-page":"1337","volume":"3","author":"G. Bella","year":"1997","unstructured":"Bella, G., Riccobene, E.: Formal Analysis of the Kerberos Authentication System. Journal of Universal Computer Science\u00a03(12), 1337\u20131381 (1997)","journal-title":"Journal of Universal Computer Science"},{"key":"17_CR8","unstructured":"Bella, G., Riccobene, E.: A Realistic Environment for Crypto-Protocol Aalyses by ASMs. In: Gl\u00e4sser, U., Schmitt, P. (eds.) Proc. 5th Int. Workshop on Abstract State Machines, Magdeburg University (1998)"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.S.E. (ed.) ETAPS 2000 and FASE 2000. LNCS, vol.\u00a01783, Springer, Heidelberg (2000)"},{"key":"17_CR10","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":"17_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"J. Derrick","year":"2003","unstructured":"Derrick, J., Wehrheim, H.: Using Coupled Simulations in Non-atomic Refinement. In: Bert, D., Bowen, J.P., King, S., Walden, M. (eds.) ZB 2003. LNCS, vol.\u00a02651, Springer, Heidelberg (2003)"},{"key":"17_CR12","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, IEEE, Los Alamitos (1981)"},{"key":"17_CR13","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"F.J.T. F\u00e1brega","year":"1999","unstructured":"F\u00e1brega, F.J.T., Herzog, J.C., Guttman, J.D.: Strand Spaces: Proving Security Protocols Correct. Journal of Computer Security\u00a07, 191\u2013230 (1999)","journal-title":"Journal of Computer Security"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11766155_9","volume-title":"Emerging Trends in Information and Communication Security","author":"H. Grandy","year":"2006","unstructured":"Grandy, H., Haneberg, D., Reif, W., Stenzel, K.: Developing Provably Secure M-Commerce Applications. In: M\u00fcller, G. (ed.) ETRICS 2006. LNCS, vol.\u00a03995, Springer, Heidelberg (2006)"},{"key":"17_CR15","unstructured":"Grandy, H., Stenzel, K., Reif, W.: A Refinement Method for Java Programs. Technical Report 2006-29, University of Augsburg (December 2006)"},{"key":"17_CR16","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, Oxford Univ. Press, New York (1995)"},{"key":"17_CR17","unstructured":"Haneberg, D.: Sicherheit von Smart Card \u2013 Anwendungen. PhD thesis, University of Augsburg, Augsburg, Germany (in German) (2006)"},{"key":"17_CR18","unstructured":"Haneberg, D., Grandy, H., Reif, W., Schellhorn, G.: Verifying Smart Card Applications: An ASM Approach. Technical Report 2006-08, Universit\u00e4t Augsburg (2006)"},{"key":"17_CR19","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":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2002)"},{"key":"17_CR21","unstructured":"Haneberg, D., Schellhorn, G., Grandy, H., Reif, W.: Verification of Mondex Electronic Purses with KIV: From Transactions to a Security Protocol. Technical Report 2006-32, University of Augsburg (December 2006)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45800-X_32","volume-title":"UML 2002 - The Unified Modeling Language 5th International Conference","author":"J. J\u00fcrjens","year":"2002","unstructured":"J\u00fcrjens, J.: UMLsec: Extending UML for Secure Systems Development. In: J\u00e9z\u00e9quel, J.-M., Hussmann, H., Cook, S. (eds.) UML 2002 - The Unified Modeling Language 5th International Conference. LNCS, vol.\u00a02460, Springer, Heidelberg (2002)"},{"key":"17_CR23","volume-title":"Secure Systems Development with UML","author":"J. J\u00fcrjens","year":"2005","unstructured":"J\u00fcrjens, J.: Secure Systems Development with UML. Springer, Heidelberg (2005)"},{"key":"17_CR24","unstructured":"Web presentation of KIV projects. URL: http:\/\/www.informatik.uniaugsburg.de\/swt\/projects\/"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45793-3_8","volume-title":"Computer Science Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, Springer, Heidelberg (2002)"},{"key":"17_CR27","unstructured":"The Object Management Group (OMG). OMG Unified Modeling Language Specification Version 1.5 (2003)"},{"key":"17_CR28","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. Journal of Computer Security\u00a06, 85\u2013128 (1998)","journal-title":"Journal of Computer Security"},{"key":"17_CR29","series-title":"Lecture Notes in Artificial Intelligence","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 (LNAI), vol.\u00a02083, Springer, Heidelberg (2001)"},{"key":"17_CR30","volume-title":"The Unified Modeling Language Reference Manual","author":"J. Rumbaugh","year":"1998","unstructured":"Rumbaugh, J., Jacobson, I., Booch, G.: The Unified Modeling Language Reference Manual. Addison-Wesley, Reading (1998)"},{"key":"17_CR31","volume-title":"The Modelling and Analysis of Security Protocols: the CSP Approach","author":"P.Y.A. Ryan","year":"2001","unstructured":"Ryan, P.Y.A., Schneider, S.A., Goldsmith, M.H., Lowe, G., Roscoe, B.: The Modelling and Analysis of Security Protocols: the CSP Approach. Addison-Wesley, Reading (2001)"},{"key":"17_CR32","volume-title":"Automated Deduction\u2014A Basis for Applications","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, Kluwer, Dordrecht (1998)"},{"issue":"11","key":"17_CR33","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:\/\/www.jucs.org","journal-title":"Journal of Universal Computer Science (J.UCS)"},{"issue":"2-3","key":"17_CR34","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":"17_CR35","unstructured":"Stepney, S., Cooper, D., Woodcock, J.: AN ELECTRONIC PURSE Specification, Refinement, and Proof. In: Technical monograph PRG-126, July 2000, Oxford University Computing Laboratory, Oxford (2000)"},{"key":"17_CR36","unstructured":"Schellhorn, G., Grandy, H., Haneberg, D., M\u00f6bius, N., Reif, W.: A systematic verification Approach for Mondex Electronic Purses using ASMs. Technical Report 2006-27, Universit\u00e4t Augsburg, Augsburg (2006)"},{"key":"17_CR37","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis","author":"G. Schellhorn","year":"2007","unstructured":"Schellhorn, G., Grandy, H., Haneberg, D., M\u00f6bius, N., Reif, W.: A Systematic Verification Approach for Mondex Electronic Purses using ASMs. In: Abrial, J.-R., Gl\u00e4sser, U. (eds.) Proceedings of the Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis. LNCS, Springer, Heidelberg (submitted, 2007)"},{"key":"17_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2006)"},{"key":"17_CR39","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73210-5_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:12:29Z","timestamp":1605762749000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73210-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540732099","9783540732105"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73210-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}