{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T00:07:57Z","timestamp":1725494877399},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540403258"},{"type":"electronic","value":"9783540448983"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44898-5_17","type":"book-chapter","created":{"date-parts":[[2007,11,11]],"date-time":"2007-11-11T03:21:25Z","timestamp":1194751285000},"page":"316-335","source":"Crossref","is-referenced-by-count":21,"title":["Computer-Assisted Verification of a Protocol for Certified Email"],"prefix":"10.1007","author":[{"given":"Mart\u00edn","family":"Abadi","sequence":"first","affiliation":[]},{"given":"Bruno","family":"Blanchet","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,5,13]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and B. Blanchet. Analyzing security protocols with secrecy types and logic programs. In 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u201902), pages 33\u201344, Portland, OR, Jan. 2002. ACM Press.","DOI":"10.1145\/503272.503277"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"M. Abadi, N. Glew, B. Horne, and B. Pinkas. Certified email with a light on-line trusted third party: Design and implementation. In 11th International World Wide Web Conference (WWW\u201902), Honolulu, Hawaii, USA, May 2002. ACM Press.","DOI":"10.1145\/511446.511497"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"G. Bella, F. Massacci, and L. C. Paulson. The verification of an industrial payment protocol: The SET purchase phase. In V. Atluri, editor, 9th ACM Conference on Computer and Communications Security (CCS\u201902), pages 12\u201320, Washington, DC, Nov. 2002. ACM Press.","DOI":"10.1145\/586111.586113"},{"key":"17_CR4","unstructured":"G. Bella and L. C. Paulson. Using Isabelle to prove properties of the Kerberos authentication system. In DIMACS Workshop on Design and Formal Verification of Security Protocols, Piscataway, NJ, Sept. 1997."},{"key":"17_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0055875","volume-title":"Computer Security-ESORICS 98","author":"G. Bella","year":"1998","unstructured":"G. Bella and L. C. Paulson. Kerberos version IV: inductive analysis of the secrecy goals. In J.-J. Quisquater et al., editors, Computer Security-ESORICS 98, volume 1485 of Lecture Notes in Computer Science, pages 361\u2013375, Louvain-la-Neuve, Belgium, Sept. 1998. Springer Verlag."},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"B. Blanchet. An efficient cryptographic protocol verifier based on Prolog rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 82\u201396, Cape Breton, Nova Scotia, Canada, June 2001. IEEE Computer Society.","DOI":"10.1109\/CSFW.2001.930138"},{"key":"17_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/3-540-45789-5_25","volume-title":"9th International Static Analysis Symposium (SAS\u201902)","author":"B. Blanchet","year":"2002","unstructured":"B. Blanchet. From secrecy to authenticity in security protocols. In M. Hermenegildo and G. Puebla, editors, 9th International Static Analysis Symposium (SAS\u201902), volume 2477 of Lecture Notes in Computer Science, pages 342\u2013359, Madrid, Spain, Sept. 2002. Springer Verlag."},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"A. Gordon and A. Jeffrey. Authenticity by typing for security protocols. In 14th IEEE Computer Security Foundations Workshop (CSFW-14), pages 145\u2013159, Cape Breton, Nova Scotia, Canada, June 2001. IEEE Computer Society.","DOI":"10.1109\/CSFW.2001.930143"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"A. Gordon and A. Jeffrey. Types and effects for asymmetric cryptographic protocols. In 15th IEEE Computer Security Foundations Workshop (CSFW-15), pages 77\u201391, Cape Breton, Nova Scotia, Canada, June 2002. IEEE Computer Society.","DOI":"10.1109\/CSFW.2002.1021808"},{"key":"17_CR10","unstructured":"H. Krawczyk. SKEME: A versatile secure key exchange mechanism for internet. In Proceedings of the Internet Society Symposium on Network and Distributed Systems Security (NDSS\u201996), San Diego, CA, Feb. 1996. Available at http:\/\/bilbo.isu.edu\/sndss\/sndss96.html."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"S. Kremer and J.-F. Raskin. Game analysis of abuse-free contract signing. In 15th IEEE Computer Security Foundations Workshop (CSFW-15), pages 206\u2013222, Cape Breton, Nova Scotia, Canada, June 2002. IEEE Computer Society.","DOI":"10.1109\/CSFW.2002.1021817"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"C. Meadows. Analysis of the Internet Key Exchange protocol using the NRL protocol analyzer. In IEEE Symposium on Security and Privacy, pages 216\u2013231, Oakland, CA, May 1999. IEEE Computer Society.","DOI":"10.21236\/ADA465466"},{"key":"17_CR13","unstructured":"J. C. Mitchell, V. Shmatikov, and U. Stern. Finite-state analysis of SSL 3.0. In 7th USENIX Security Symposium, pages 201\u2013216, San Antonio, TX, Jan. 1998."},{"issue":"3","key":"17_CR14","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1145\/322510.322530","volume":"2","author":"L. C. Paulson","year":"1999","unstructured":"L. C. Paulson. Inductive analysis of the Internet protocol TLS. ACM Transactions on Information and System Security, 2(3):332\u2013351, Aug. 1999.","journal-title":"ACM Transactions on Information and System Security"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"S. Schneider. Formal analysis of a non-repudiation protocol. In 11th IEEE Computer Security Foundations Workshop (CSFW-11), pages 54\u201365, Rockport, Massachusetts, June 1998. IEEE Computer Society.","DOI":"10.1109\/CSFW.1998.683155"},{"issue":"2","key":"17_CR16","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1016\/S0304-3975(01)00141-4","volume":"283","author":"V. Shmatikov","year":"2002","unstructured":"V. Shmatikov and J. C. Mitchell. Finite-state analysis of two contract signing protocols. Theoretical Computer Science, 283(2):419\u2013450, June 2002.","journal-title":"Theoretical Computer Science"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"T. Y. C. Woo and S. S. Lam. A semantic model for authentication protocols. In 1993 IEEE Symposium on Research on Security and Privacy, pages 178\u2013194, Oakland, CA, 1993. IEEE Computer Society.","DOI":"10.1109\/RISP.1993.287633"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44898-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T09:21:16Z","timestamp":1556961676000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44898-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540403258","9783540448983"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-44898-5_17","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}