{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:24:06Z","timestamp":1779074646465,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540206934","type":"print"},{"value":"9783540409816","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-40981-6_4","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T19:17:45Z","timestamp":1277234265000},"page":"15-32","source":"Crossref","is-referenced-by-count":7,"title":["Interacting State Machines: A Stateful Approach to Proving Security"],"prefix":"10.1007","author":[{"given":"David","family":"von Oheimb","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: assigning programs to meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-book: assigning programs to meanings. Cambridge University Press, Cambridge (1996)"},{"key":"4_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4613-0091-5","volume-title":"Specification and development of interactive systems","author":"M. Broy","year":"2001","unstructured":"Broy, M., St\u00f8len, K.: Specification and development of interactive systems. Springer, Heidelberg (2001)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1007\/3-540-48119-2_28","volume-title":"FM\u201999 - Formal Methods","author":"M. Butler","year":"1999","unstructured":"Butler, M.: csp2B: A practical approach to combining CSP and B. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 490\u2013508. Springer, Heidelberg (1999)"},{"key":"4_CR4","unstructured":"Common Criteria for Information Technology Security Evaluation (CC), Version 2.1, ISO\/IEC 15408 (1999)"},{"key":"4_CR5","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1109\/CSFW.2000.856933","volume-title":"13th IEEE Computer Security Foundations Workshop \u2014 CSFW 2000","author":"E. Cohen","year":"2000","unstructured":"Cohen, E.: Taps: A first-order verifier for cryptographic protocols. In: 13th IEEE Computer Security Foundations Workshop \u2014 CSFW 2000, Cambridge, UK, July 3-5, pp. 144\u2013158. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"4_CR6","unstructured":"Fischer, C.: Combination and implementation of processes and data: from CSP-OZ to Java. PhD thesis, Univ. of Oldenburg (2000)"},{"key":"4_CR7","unstructured":"Gurevich, Y.: Draft of the asm guide. Technical Report CSE-TR-336-97, EECS Dept., University of Michigan (1997)"},{"key":"4_CR8","unstructured":"Hamberger, T.: Integrating theorem proving and model checking in Isabelle\/IOA. Technical report, TU M\u00fcnchen (1999)"},{"key":"4_CR9","first-page":"229","volume-title":"On the construction of programs \u2013 an advanced course","author":"C.A.R. Hoare","year":"1980","unstructured":"Hoare, C.A.R.: Communicating sequential processes. In: McKeag, R.M., Macnaghten, A.M. (eds.) On the construction of programs \u2013 an advanced course, pp. 229\u2013254. Cambridge University Press, Cambridge (1980)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1007\/3-540-61648-9_58","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"F. Huber","year":"1996","unstructured":"Huber, F., Sch\u00e4tz, B., Schmidt, A., Spies, K.: Autofocus - a tool for distributed systems specification. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol.\u00a01135, pp. 467\u2013470. Springer, Heidelberg (1996), See also \n                    \n                      http:\/\/autofocus.in.tum.de\/index-e.html"},{"key":"4_CR11","unstructured":"Information Technology Security Evaluation Criteria, ITSEC (1991)"},{"key":"4_CR12","unstructured":"J\u00fcrjens, J.: Algebraic state machines: Concepts and applications to security (2002) (submitted for publication )"},{"key":"4_CR13","unstructured":"J\u00fcrjens, J.: Principles for Secure Systems Design. PhD thesis, Oxford University Computing Laboratory, Trinity Term (2002)"},{"key":"4_CR14","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)"},{"issue":"3","key":"4_CR15","first-page":"219","volume":"2","author":"N. Lynch","year":"1989","unstructured":"Lynch, N., Tuttle, M.: An introduction to input\/output automata. CWI Quarterly\u00a02(3), 219\u2013246 (1989), \n                    \n                      http:\/\/theory.lcs.mit.edu\/tds\/papers\/Lynch\/CWI89.html","journal-title":"CWI Quarterly"},{"key":"4_CR16","unstructured":"Maia, M., Iorio, V., Bigonha, R.: Interacting Abstract State Machines. In: Proceedings of the 28th Annual Conference of the German Society of Computer Science. Technical Report, Magdeburg University (1998)"},{"issue":"1","key":"4_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R. Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes - parts i+ii. Information and Computation\u00a0100(1), 1\u201377 (1992)","journal-title":"Information and Computation"},{"key":"4_CR18","unstructured":"M\u00fcller, O.: A Verification Environment for I\/O Automata Based on Formalized Meta-Theory. PhD thesis, Technische Univerit\u00e4t M\u00fcnchen (1998), See also \n                    \n                      http:\/\/isabelle.in.tum.de\/IOA\/"},{"key":"4_CR19","unstructured":"Nanz, S.: Integration of CASE Tools and Theorem Provers: A Framework for System Modeling and Verification with AutoFocus and Isabelle. Master\u2019s thesis, TU M\u00fcnchen (2002), \n                    \n                      http:\/\/home.in.tum.de\/nanz\/csthesis\/"},{"key":"4_CR20","unstructured":"Nanz, S., von Oheimb, D.: ISM Framework: Manual and distribution (2002), \n                    \n                      http:\/\/ddvo.net\/ISM\/"},{"key":"4_CR21","unstructured":"von Oheimb, D.: The Isabelle\/HOL implementation of Interacting State Machines, Technical documentation, available on request (2002)"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/3-540-45853-0_13","volume-title":"Computer Security - ESORICS 2002","author":"D. Oheimb von","year":"2002","unstructured":"von Oheimb, D., Lotz, V.: Formal Security Analysis with Interacting State Machines. In: Gollmann, D., Karjoth, G., Waidner, M. (eds.) ESORICS 2002. LNCS, vol.\u00a02502, p. 212. Springer, Heidelberg (2002), \n                    \n                      http:\/\/ddvo.net\/papers\/FSA_ISM.html"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994), For an up-to-date description, see \n                    \n                      http:\/\/isabelle.in.tum.de\/"},{"key":"4_CR24","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":"4_CR25","unstructured":"Slotosch, O., et al.: Validas Model Validation AG, \n                    \n                      http:\/\/www.validas.de\/"},{"key":"4_CR26","volume-title":"Proceedings of the 10th Computer Security Foundations Workshop (CSFW)","author":"S. Schneider","year":"1997","unstructured":"Schneider, S.: Verifying authentication protocols with CSP. In: Proceedings of the 10th Computer Security Foundations Workshop (CSFW). IEEE Computer Society Press, Los Alamitos (June 1997)"},{"key":"4_CR27","unstructured":"Mike Spivey, J.: The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edn. (1992)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-40981-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,15]],"date-time":"2019-03-15T00:52:57Z","timestamp":1552611177000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-40981-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540206934","9783540409816"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-40981-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}