{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:08:49Z","timestamp":1725484129696},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439288"},{"type":"electronic","value":"9783540456148"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_18","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:45:28Z","timestamp":1179377128000},"page":"310-329","source":"Crossref","is-referenced-by-count":12,"title":["Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation"],"prefix":"10.1007","author":[{"given":"Michael","family":"Backes","sequence":"first","affiliation":[]},{"given":"Christian","family":"Jacobi","sequence":"additional","affiliation":[]},{"given":"Birgit","family":"Pfitzmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148\/1","author":"M. Abadi","year":"1999","unstructured":"M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation 148\/1 (1999) 1\u201370.","journal-title":"Information and Computation"},{"key":"18_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/3-540-44929-9_1","volume-title":"IFIP Intern. Conf. on Theoretical Computer Science (TCS 2000)","author":"M. Abadi","year":"2000","unstructured":"M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). IFIP Intern. Conf. on Theoretical Computer Science (TCS 2000), LNCS 1872, Springer-Verlag, 2000, 3\u201322."},{"key":"18_CR3","unstructured":"M. Backes. Cryptographically sound analysis of security protocols. Ph.D thesis, Computer Science Department, Saarland University, 2002."},{"key":"18_CR4","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29\/2","author":"D. Dolev","year":"1983","unstructured":"D. Dolev and A. C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory 29\/2 (1983) 198\u2013208.","journal-title":"IEEE Transactions on Information Theory"},{"key":"18_CR5","first-page":"160","volume-title":"1998 IEEE Symposium on Security and Privacy","author":"F. J. T. Fabrega","year":"1998","unstructured":"F. J. T. Fabrega, J. C. Herzog, and J. D. Guttman. Strand spaces: Why is a security protocol correct? 1998 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, Los Alamitos 1998, 160\u2013171."},{"key":"18_CR6","series-title":"International Series in Computer Science","volume-title":"Communicating sequential processes","author":"C. A. R. Hoare","year":"1985","unstructured":"C. A. R. Hoare. Communicating sequential processes. International Series in Computer Science, Prentice Hall, Hemel Hempstead 1985."},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"P. Lincoln, J. Mitchell, M. Mitchell, and A. Scedrov. A probabilistic poly-time framework for protocol analysis. 5th ACM Conference on Computer and Communications Security, San Francisco, November 1998, 112\u2013121.","DOI":"10.1145\/288090.288117"},{"key":"18_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"776","DOI":"10.1007\/3-540-48119-2_43","volume-title":"Formal Methods\u2019 99","author":"P. Lincoln","year":"1999","unstructured":"P. Lincoln, J. Mitchell, M. Mitchell, and A. Scedrov. Probabilistic polynomial-time equivalence and security analysis. Formal Methods\u2019 99, LNCS 1708, Springer-Verlag, 1999, 776\u2013793."},{"key":"18_CR9","series-title":"Lect Notes Comput Sci","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 (TACAS)","author":"G. Lowe","year":"1996","unstructured":"G. Lowe. Breaking and fixing the needham-schroeder public-key protocol using FDR. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 1055, Springer-Verlag, Berlin 1996, 147\u2013166."},{"key":"18_CR10","volume-title":"Distributed algorithms","author":"N. Lynch","year":"1996","unstructured":"N. Lynch. Distributed algorithms. Morgan Kaufmann Publishers, San Francisco 1996."},{"key":"18_CR11","doi-asserted-by":"crossref","unstructured":"N. Lynch. I\/O automaton models and proofs for shared-key communication systems. 12th Computer Security Foundations Workshop (CSFW), IEEE, 1999, 14\u201329.","DOI":"10.1109\/CSFW.1999.779759"},{"key":"18_CR12","unstructured":"S. Owre and N. Shankar. Abstract datatypes in PVS. Technical report, Computer Science Laboratory, SRI International, 1993."},{"key":"18_CR13","doi-asserted-by":"crossref","unstructured":"S. Owre, N. Shankar, and J. M. Rushby. PVS: A prototype verification system. In CADE 11, volume 607 of LNAI, pages 748\u2013752. Springer, 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"issue":"1","key":"18_CR14","doi-asserted-by":"crossref","first-page":"85","DOI":"10.3233\/JCS-1998-61-205","volume":"6","author":"L. Paulson","year":"1998","unstructured":"L. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6(1):85\u2013128, 1998.","journal-title":"Journal of Computer Security"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"B. Pfitzmann and M. Waidner. Composition and integrity preservation of secure reactive systems. 7th ACM Conference on Computer and Communications Security, Athens, November 2000, 245\u2013254.","DOI":"10.1145\/352600.352639"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"B. Pfitzmann and M. Waidner. A model for asynchronous reactive systems and its application to secure message transmission. IEEE Symposium on Security and Privacy, Oakland, May 2001, 184\u2013202.","DOI":"10.1109\/SECPRI.2001.924298"},{"key":"18_CR17","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1109\/SECPRI.1996.502680","volume-title":"1996 IEEE Symposium on Security and Privacy","author":"S. Schneider","year":"1996","unstructured":"S. Schneider. Security properties and CSP. 1996 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, Washington 1996, 174\u2013187."},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"A. C. Yao. Protocols for secure computations. 23rd Symposium on Foundations of Computer Science (FOCS) 1982, IEEE Computer Society, 1982, 160\u2013164.","DOI":"10.1109\/SFCS.1982.38"}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T18:51:56Z","timestamp":1550343116000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_18","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}