{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T23:45:02Z","timestamp":1743119102148,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642005893"},{"type":"electronic","value":"9783642005909"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-00590-9_17","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T08:05:58Z","timestamp":1238141158000},"page":"222-236","source":"Crossref","is-referenced-by-count":1,"title":["Type-Based Automated Verification of Authenticity in Cryptographic Protocols"],"prefix":"10.1007","author":[{"given":"Daisuke","family":"Kikuchi","sequence":"first","affiliation":[]},{"given":"Naoki","family":"Kobayashi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1016\/S0304-3975(02)00333-X","volume":"300","author":"A.D. Gordon","year":"2003","unstructured":"Gordon, A.D., Jeffrey, A.: Typing correspondence assertions for communication protocols. Theor. Comput. Sci.\u00a0300, 379\u2013409 (2003)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"17_CR2","doi-asserted-by":"publisher","first-page":"451","DOI":"10.3233\/JCS-2003-11402","volume":"11","author":"A.D. Gordon","year":"2003","unstructured":"Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. Journal of Computer Security\u00a011(4), 451\u2013520 (2003)","journal-title":"Journal of Computer Security"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Gordon, A.D., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. In: 15th IEEE Computer Security Foundations Workshop (CSFW-15), pp. 77\u201391 (2002)","DOI":"10.1109\/CSFW.2002.1021808"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Woo, T.Y., Lam, S.S.: A semantic model for authentication protocols. In: RSP: IEEE Computer Society Symposium on Research in Security and Privacy, pp. 178\u2013193 (1993)","DOI":"10.1109\/RISP.1993.287633"},{"key":"17_CR5","unstructured":"Haack, C., Jeffrey, A.: Cryptyc (2004), http:\/\/www.cryptyc.org\/"},{"key":"17_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-540-76637-7_13","volume-title":"Programming Languages and Systems","author":"D. Kikuchi","year":"2007","unstructured":"Kikuchi, D., Kobayashi, N.: Type-based verification of correspondence assertions for communication protocols. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol.\u00a04807, pp. 191\u2013205. Springer, Heidelberg (2007)"},{"issue":"3-4","key":"17_CR7","doi-asserted-by":"publisher","first-page":"435","DOI":"10.3233\/JCS-2004-123-406","volume":"12","author":"A.D. Gordon","year":"2004","unstructured":"Gordon, A.D., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. Journal of Computer Security\u00a012(3-4), 435\u2013483 (2004)","journal-title":"Journal of Computer Security"},{"issue":"1","key":"17_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1998.2740","volume":"148","author":"M. Abadi","year":"1999","unstructured":"Abadi, M., Gordon, A.D.: A Calculus for Cryptographic Protocols: The Spi Calculus. Information and Computation\u00a0148(1), 1\u201370 (1999)","journal-title":"Information and Computation"},{"key":"17_CR9","unstructured":"GNU Linear Programming Kit, http:\/\/www.gnu.org\/software\/glpk"},{"key":"17_CR10","unstructured":"Gordon, A.D., H\u00fcttel, H., Hansen, R.R.: Type inference for correspondence types. In: 6th International Workshop on Security Issues in Concurrency (SecCo 2008) (2008)"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-540-24725-8_11","volume-title":"Programming Languages and Systems","author":"M. Bugliesi","year":"2004","unstructured":"Bugliesi, M., Focardi, R., Maffei, M.: Compositional analysis of authentication protocols. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 140\u2013154. Springer, Heidelberg (2004)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Bugliesi, M., Focardi, R., Maffei, M.: Authenticity by tagging and typing. In: Proceedings of the 2004 ACM Workshop on Formal Methods in Security Engineering (FMSE 2004), pp. 1\u201312 (2004)","DOI":"10.1145\/1029133.1029135"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Focardi, R., Maffei, M., Placella, F.: Inferring authentication tags. In: Proceedings of the Workshop on Issues in the Theory of Security (WITS 2005), pp. 41\u201349 (2005)","DOI":"10.1145\/1045405.1045410"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. In: Proceedings of the 21st IEEE Computer Security Foundations Symposium (CSF 2008), pp. 17\u201332 (2008)","DOI":"10.1109\/CSF.2008.27"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-45789-5_25","volume-title":"Static Analysis","author":"B. Blanchet","year":"2002","unstructured":"Blanchet, B.: From Secrecy to Authenticity in Security Protocols. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 342\u2013359. Springer, Heidelberg (2002)"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: Computationally sound mechanized proofs of correspondence assertions. In: 20th IEEE Computer Security Foundations Symposium (CSF 2007), pp. 97\u2013111 (2007)","DOI":"10.1109\/CSF.2007.16"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J. Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 55\u201372. Springer, Heidelberg (2003)"},{"key":"17_CR18","first-page":"105","volume-title":"Proc. of ICFP","author":"T. Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Witnessing side-effects. In: Proc. of ICFP, pp. 105\u2013115. ACM, New York (2005)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Terauchi, T., Aiken, A.: A capability calculus for concurrency and determinism. ACM Trans. Prog. Lang. Syst.\u00a030(5) (2008)","DOI":"10.1145\/1387673.1387676"},{"key":"17_CR20","doi-asserted-by":"crossref","unstructured":"Terauchi, T.: Checking race freedom via linear programming. In: Proc. of PLDI, pp. 1\u201310 (2008)","DOI":"10.1145\/1375581.1375583"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00590-9_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T00:23:30Z","timestamp":1558225410000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00590-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642005893","9783642005909"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00590-9_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}