{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:11:58Z","timestamp":1725466318079},"publisher-location":"New York","reference-count":18,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"0387240500"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/0-387-24098-5_10","type":"book-chapter","created":{"date-parts":[[2005,10,3]],"date-time":"2005-10-03T17:34:04Z","timestamp":1128360844000},"page":"129-144","source":"Crossref","is-referenced-by-count":1,"title":["Complementing Computational Protocol Analysis with Formal Specifications"],"prefix":"10.1007","author":[{"given":"Kim-Kwang Raymond","family":"Choo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Colin","family":"Boyd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yvonne","family":"Hitchcock","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Greg","family":"Maitland","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and A.D. Gordon. A Calculus for Cryptographic Protocols: The Spi Calculus. In 4th ACM Conference on Computer and Communications Security, pages 36\u201347. ACM Press, 1997.","DOI":"10.1145\/266420.266432"},{"key":"10_CR2","unstructured":"M. Abadi and P. Rogaway. Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption). In IFIP International Conference on Theoretical Computer Science-IFIP TCS2000, pages 3\u201322. Springer-Verlag, 2000."},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"M. Backes and C. Jacobi. Cryptographically Sound and Machine-Assisted Verification of Security Protocols. In 20th International Symposium on Theoretical Aspects of Computer Science-STACS 2003, pages 310\u2013329. Springer-Verlag, 2003.","DOI":"10.1007\/3-540-36494-3_59"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"M. Backes, C. Jacobi, and B. Pfitzmann. Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation. In Formal Methods-Getting IT Right, pages 310\u2013329. Springer-Verlag, 2002.","DOI":"10.1007\/3-540-45614-7_18"},{"key":"10_CR5","first-page":"139","volume":"1807","author":"B. M","year":"2000","unstructured":"M. Bellare, D. Pointcheval, and P. Rogaway. Authenticated Key Exchange Secure Against Dictionary Attacks. In Advances in Cryptology \u2014 Eurocrypt, pages 139\u2013155. Springer-Verlag, 2000. LNCS Volume 1807\/2000.","journal-title":"Advances in Cryptology \u2014 Eurocrypt"},{"key":"10_CR6","first-page":"110","volume":"773","author":"M. Bellare","year":"1993","unstructured":"M. Bellare and P. Rogaway. Entity Authentication and Key Distribution. In Advances in Cryptology, pages 110\u2013125. Springer-Verlag, 1993. LNCS Volume 773\/1993.","journal-title":"Advances in Cryptology"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"M. Bellare and P. Rogaway. Provably Secure Session Key Distribution: The Three Party Case. In 27th ACM Symposium on the Theory of Computing, pages 57\u201366. ACM Press, 1995.","DOI":"10.1145\/225058.225084"},{"key":"10_CR8","unstructured":"C. Boyd and K. Viswanathan. Towards a Formal Specification of the Bellare-Rogaway Model for Protocol Analysis. In Formal Aspects of Security-FASec 2002, pages 209\u2013223. British Computer Society Press, Dec 2002."},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"R. Canetti. Universally Composable Security: A New Paradigm for Cryptographic Protocols. Cryptology ePrint Archive, Report 2000\/067, 2000.","DOI":"10.1109\/SFCS.2001.959888"},{"key":"10_CR10","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1007\/3-540-44987-6_28","volume":"2045","author":"R. Canetti","year":"2001","unstructured":"R. Canetti and H. Krawczyk. Analysis of Key-Exchange Protocols and Their Use for Building Secure Channels. In Advances in Cryptology-Eurocrypt 2001:, pages 453\u2013474. Springer-Verlag, May 2001. LNCS Volume 2045\/2001.","journal-title":"Advances in Cryptology-Eurocrypt 2001"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"R. Canetti and H. Krawczyk. Universally Composable Notions of Key Exchange and Secure Channels (Extended Version). Cryptology ePrint Archive, Report 2002\/059, 2002.","DOI":"10.1007\/3-540-46035-7_22"},{"issue":"2","key":"10_CR12","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"D. Dolev and A.C. Yao. On the Security of Public Key Protocols. IEEE Transaction of Information Technology, 29(2):198\u2013208, 1983.","journal-title":"IEEE Transaction of Information Technology"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"M. Jakobsson and D. Pointcheval. Mutual Authentication and Key Exchange Protocol for Low Power Devices. In Financial Cryptography, pages 178\u2013195. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-46088-8_17"},{"key":"10_CR14","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1080\/095281300454829","volume":"12","author":"P. Ochsenschlager","year":"2000","unstructured":"P. Ochsenschlager, J. Repp, and R. Rieke. Abstraction and a Verification Method for Cooperating Systems. Journal of Experimental and Theoretical Artificial Intelligence, 12:447\u2013159, Jun 2000.","journal-title":"Journal of Experimental and Theoretical Artificial Intelligence"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"B. Pfitzmann, M. Schunter, and M. Waidner. Cryptographic Security of Reactive Systems. In Steve Schneider and Peter Ryan, editors, Electronic Notes in Theoretical Computer Science, volume 32. Reed Elsevier, 2000.","DOI":"10.1016\/S1571-0661(04)00095-7"},{"key":"10_CR16","unstructured":"R. Rieke. Implementing the APA Model for the Symmetric Needham-Schroeder Protocol in State Transition Pattern Notation in the SH Verification Tool. Technical report, Fraunhofer Institute for Secure Telecooperation SIT, 26 July 2002."},{"key":"10_CR17","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/3-540-44647-8_15","volume":"2139","author":"V. Shoup","year":"2001","unstructured":"V. Shoup. OAEP Reconsidered. In Advances in Cryptology-CRYPTO 2001, pages 239\u2013259. Springer-Verlag, 2001. LNCS Volume 2139\/2001.","journal-title":"Advances in Cryptology-CRYPTO 2001"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"D.S. Wong and A.H. Chan. Efficient and Mutually Authenticated Key Exchange for Low Power Computing Devices. In Advances in Cryptology-Asiacrypt 2001. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-45682-1_17"}],"container-title":["IFIP International Federation for Information Processing","Formal Aspects in Security and Trust"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/0-387-24098-5_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:58:12Z","timestamp":1605643092000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/0-387-24098-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["0387240500"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/0-387-24098-5_10","relation":{},"subject":[]}}