{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T20:34:14Z","timestamp":1742934854247,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540443452"},{"type":"electronic","value":"9783540458531"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45853-0_13","type":"book-chapter","created":{"date-parts":[[2007,5,3]],"date-time":"2007-05-03T20:42:13Z","timestamp":1178224933000},"page":"212-229","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Formal Security Analysis with Interacting State Machines"],"prefix":"10.1007","author":[{"given":"David","family":"von Oheimb","sequence":"first","affiliation":[]},{"given":"Volkmar","family":"Lotz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,26]]},"reference":[{"key":"13_CR1","unstructured":"Atmel, Hitachi Europe, Infineon Technologies, and Philips Semiconductors. Smartcard IC Platform Protection Profile, Version 1.0, July 2001."},{"key":"13_CR2","unstructured":"David Aspinall, Healfdene Goguen, Thomas Kleymann, and Dilip Sequeira. Proof General, 1999."},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Michael Butler. csp2B: A practical approach to combining CSP and B. In Proceedings of FM\u201999: World Congress on Formal Methods, pages 490\u2013508, 1999. \n                  http:\/\/www.dsse.ecs.soton.ac.uk\/techreports\/99-2.html\n                  \n                .","DOI":"10.1007\/3-540-48119-2_28"},{"key":"13_CR4","unstructured":"Common Criteria for Information Technology Security Evaluation (CC), Version 2.1, 1999. ISO\/IEC 15408."},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Danny Dolev and Andrew C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT-29(12):198\u2013208, March 1983.","DOI":"10.1109\/TIT.1983.1056650"},{"key":"13_CR6","unstructured":"Clemens Fischer. Combination and implementation of processes and data: from CSP-OZ to Java. PhD thesis, University of Oldenburg, 2000."},{"key":"13_CR7","unstructured":"Stephen J. Garland and Nancy A. Lynch. The IOA language and toolset: Support for designing, analyzing, and building distributed systems. Technical Report MIT\/LCS\/TR-762, Laboratory for Computer Science, MIT, August 1998."},{"key":"13_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1007\/3-540-61648-9_58","volume-title":"Proceedings FTRTFT\u201996-Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"F. Huber","year":"1996","unstructured":"Franz Huber, Bernhard Sch\u00e4tz, Alexander Schmidt, and Katharina Spies. Autofocus-a tool for distributed systems specification. In Proceedings FTRTFT\u201996-Formal Techniques in Real-Time and Fault-Tolerant Systems, volume 1135 of LNCS, pages 467\u2013470. Springer-Verlag, 1996. See also \n                  http:\/\/autofocus.in.tum.de\/index-e.html\n                  \n                ."},{"key":"13_CR9","unstructured":"Information Technology Security Evaluation Criteria (ITSEC), June 1991."},{"key":"13_CR10","unstructured":"Jan J\u00fcrjens and Guido Wimmel. Formally testing fail-safety of electronic purse protocols. In Automated Software Engineering. IEEE Computer Society, 2001."},{"key":"13_CR11","unstructured":"Dilsun Kirli Kaynar. IOA language and toolset, 2001. \n                  http:\/\/theory.lcs.mit.edu\/tds\/ioa.html\n                  \n                ."},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Volkmar Lotz, Volker Kessler, and Georg Walter. A Formal Security Model for Microprocessor Hardware. In IEEE Transactions on Software Engineering, volume 26, pages 702\u2013712, August 2000. \n                  http:\/\/www.computer.org\/tse\/ts2000\/e8toc.htm\n                  \n                .","DOI":"10.1109\/32.879809"},{"key":"13_CR13","first-page":"147","volume":"1055","author":"G. Lowe","year":"1996","unstructured":"Gavin Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Proceedings of TACAS, volume 1055, pages 147\u2013166. Springer-Verlag, 1996.","journal-title":"Proceedings of TACAS"},{"key":"13_CR14","unstructured":"Gavin Lowe. A hierarchy of authentication specifications. In PCSFW: Proceedings of The 10th Computer Security Foundations Workshop. IEEE Computer Society Press, 1997."},{"issue":"3","key":"13_CR15","first-page":"219","volume":"2","author":"N. Lynch","year":"1989","unstructured":"Nancy Lynch and Mark Tuttle. An introduction to input\/output automata. CWI Quarterly, 2(3):219\u2013246, 1989. \n                  http:\/\/theory.lcs.mit.edu\/tds\/papers\/Lynch\/CWI89.html\n                  \n                .","journal-title":"CWI Quarterly"},{"key":"13_CR16","unstructured":"David von Oheimb. Interacting State Machines, 2002. Submitted for publication."},{"key":"13_CR17","unstructured":"David von Oheimb. The Isabelle\/HOL implementation of Interacting State Machines, 2002. Technical documentation, available on request."},{"key":"13_CR18","unstructured":"David von Oheimb, Volkmar Lotz, and Gerog Walter. An interpretation of the LKW model according to the SLE66CX322P security target. Unpublished, January 2002."},{"key":"13_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer-Verlag, 1994. For an up-to-date description, see \n                  http:\/\/isabelle.in.tum.de\/\n                  \n                ."},{"key":"13_CR20","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L. C. Paulson","year":"1998","unstructured":"Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85\u2013128, 1998.","journal-title":"Journal of Computer Security"},{"key":"13_CR21","unstructured":"Lawrence C. Paulson, Tobias Nipkow, Markus Wenzel, et al. The Isabelle\/HOL library. \n                  http:\/\/isabelle.in.tum.de\/library\/HOL\/\n                  \n                ."},{"key":"13_CR22","unstructured":"Oscar Slotosch et al. Validas Model Validation AG. \n                  http:\/\/www.validas.de\/\n                  \n                ."},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Guido Wimmel and Alexander Wisspeintner. Extended description techniques for security engineering. In M. Dupuy and P. Paradinas, editors, International Conference on Information Security (IFIP\/SEC). Kluwer Academic Publishers, 2001.","DOI":"10.1007\/0-306-46998-7_32"}],"container-title":["Lecture Notes in Computer Science","Computer Security \u2014 ESORICS 2002"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45853-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,2]],"date-time":"2019-06-02T20:08:41Z","timestamp":1559506121000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45853-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540443452","9783540458531"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-45853-0_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"26 September 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}