{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T06:39:58Z","timestamp":1743057598652,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"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_9","type":"book-chapter","created":{"date-parts":[[2007,5,4]],"date-time":"2007-05-04T00:42:13Z","timestamp":1178239333000},"page":"146-162","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Analysing a Stream Authentication Protocol Using Model Checking"],"prefix":"10.1007","author":[{"given":"Philippa","family":"Broadfoot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gavin","family":"Lowe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,26]]},"reference":[{"issue":"4","key":"9_CR1","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/302350.302353","volume":"32","author":"R. Anderson","year":"1998","unstructured":"R. Anderson, F. Bergadano, B. Crispo, J.-H. Lee, C. Manifavas, and R. Needham. A new family of authentication protocols. Operating Systems Review, 32(4):9\u201320, 1998.","journal-title":"Operating Systems Review"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"M. Archer. Proving correctness of the basic TESLA multicast stream authentication protocol with TAME. In Workshop on Issues in the Theory of Security, 2002.","DOI":"10.21236\/ADA464932"},{"issue":"8","key":"9_CR3","first-page":"198","volume":"29","author":"D. Dolev","year":"1983","unstructured":"D. Dolev and A. C. Yao. On the security of public-key protocols. Communications of the ACM, 29(8):198\u2013208, August 1983.","journal-title":"Communications of the ACM"},{"key":"9_CR4","unstructured":"Formal Systems (Europe) Ltd. Failures-Divergence Refinement\u2014FDR2 User Manual, 2000. At http:\/\/www.fsel.com\/fdr2manual.html ."},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"9_CR6","unstructured":"M. L. Hui. A CSP Approach to the Analysis of Security Protocols. PhD thesis, University of Leicester, 2001."},{"issue":"1 2","key":"9_CR7","first-page":"3","volume":"9","author":"M. L. Hui","year":"2001","unstructured":"M. L. Hui and G. Lowe. Fault-preserving simplifying transformations for security protocols. Journal of Computer Science, 9(1, 2):3\u201346, 2001.","journal-title":"Journal of Computer Science"},{"key":"9_CR8","unstructured":"R. Lazi\u0107. Theorems for mechanical verification of data-independent CSP. D.Phil, Oxford University, 1999."},{"key":"9_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Proceedings of TACAS","author":"G. Lowe","year":"1996","unstructured":"G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In Proceedings of TACAS, volume 1055 of Lecture Notes in Computer Science, pages 147\u2013166. Springer Verlag, 1996. Also in Software\u2014Concepts and Tools, 17:93-102, 1996."},{"issue":"10","key":"9_CR10","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/32.637148","volume":"23","author":"G. Lowe","year":"1997","unstructured":"G. Lowe and B. Roscoe. Using CSP to detect errors in the TMN protocol. IEEE Transactions on Software Engineering, 23(10):659\u2013669, 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"A. Perrig, R. Canetti, J. D. Tygar, and D.X. Song. Efficient authentication and signing of multicast streams over lossy channels. In IEEE Symposium on Security and Privacy, pages 56\u201373, May 2000.","DOI":"10.1109\/SECPRI.2000.848446"},{"key":"9_CR12","unstructured":"A.W. Roscoe. The Theory and Practice of Concurrency. Prentice Hall, 1997."},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"A.W. Roscoe. Proving security protocols with model checkers by data independence techniques. In 11th IEEE Computer Security Foundations Workshop, pages 84\u201395, 1998.","DOI":"10.1109\/CSFW.1998.683158"},{"issue":"2 3","key":"9_CR14","doi-asserted-by":"crossref","first-page":"147","DOI":"10.3233\/JCS-1999-72-303","volume":"7","author":"A. W. Roscoe","year":"1999","unstructured":"A. W. Roscoe and P. J. Broadfoot. Proving security protocols with model checkers by data independence techniques. Journal of Computer Security, 7(2, 3):147\u2013190, 1999.","journal-title":"Journal of Computer Security"},{"key":"9_CR15","unstructured":"A.W. Roscoe and M. H. Goldsmith. The perfect\u2019 spy\u2019 for model-checking crypto-protocols. In Proceedings of DIM ACS workshop on the design and formal verification of cryptographic protocols, 1997."},{"key":"9_CR16","unstructured":"P. Ryan, S. Schneider, M. Goldsmith, G. Lowe, and B. Roscoe. Modelling and Analysis of Security Protocols. Pearson Education, 2001."}],"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_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T01:54:59Z","timestamp":1736992499000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45853-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540443452","9783540458531"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-45853-0_9","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"}}]}}