{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T05:19:58Z","timestamp":1725599998157},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642230813"},{"type":"electronic","value":"9783642230820"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-23082-0_3","type":"book-chapter","created":{"date-parts":[[2011,8,9]],"date-time":"2011-08-09T08:24:32Z","timestamp":1312878272000},"page":"66-100","source":"Crossref","is-referenced-by-count":2,"title":["Cryptographic Verification by Typing for a Sample Protocol Implementation"],"prefix":"10.1007","author":[{"given":"C\u00e9dric","family":"Fournet","sequence":"first","affiliation":[]},{"given":"Karthikeyan","family":"Bhargavan","sequence":"additional","affiliation":[]},{"given":"Andrew D.","family":"Gordon","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"3_CR1","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/1044731.1044735","volume":"52","author":"M. Abadi","year":"2005","unstructured":"Abadi, M., Blanchet, B.: Analyzing security protocols with secrecy types and logic programs. JACM\u00a052(1), 102\u2013146 (2005)","journal-title":"JACM"},{"key":"3_CR2","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\u201370 (1999)","journal-title":"Information and Computation"},{"key":"3_CR3","unstructured":"Acar, T., Fournet, C., Shumow, D.: DKM: Design and verification of a crypto-agile distributed key manager (2011), http:\/\/research.microsoft.com\/en-us\/um\/people\/fournet\/dkm\/"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Aizatulin, M., Gordon, A.D., J\u00fcrjens, J.: Extracting and verifying cryptographic models from C protocol code by symbolic execution (in submission, 2011)","DOI":"10.1145\/2046707.2046745"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Albrecht, M., Paterson, K., Watson, G.: Plaintext recovery attacks against SSH. In: 2009 30th IEEE Symposium on Security and Privacy, pp. 16\u201326 (May 2009)","DOI":"10.1109\/SP.2009.5"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Backes, M., Maffei, M., Unruh, D.: Computationally sound verification of source code. In: ACM CCS, pp. 387\u2013398 (2010)","DOI":"10.1145\/1866307.1866351"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Backes, M., Hri\u0163cu, C., Maffei, M.: Union and intersection types for secure protocol implementations. In: TOSCA (2011)","DOI":"10.1007\/978-3-642-27375-9_1"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Baltopoulos, I., Gordon, A.D.: Secure compilation of a multi-tier web language. In: ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI 2009), pp. 27\u201338 (2009)","DOI":"10.1145\/1481861.1481866"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Baltopoulos, I., Borgstr\u00f6m, J., Gordon, A.D.: Maintaining database integrity with refinement types. In: ECOOP 2011 (2011)","DOI":"10.1007\/978-3-642-22655-7_23"},{"key":"3_CR10","unstructured":"Bellare, M., Rogaway, P.: Introduction to modern cryptography. In: UCSD CSE 207 Course Notes (2005)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Advances in Cryptology - CRYPTO \u201996","author":"M. Bellare","year":"1996","unstructured":"Bellare, M., Canetti, R., Krawczyk, H.: Keying hash functions for message authentication. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol.\u00a01109, pp. 1\u201315. Springer, Heidelberg (1996)"},{"key":"3_CR12","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/1368310.1368330","volume-title":"Proceedings of the ACM Symposium on Information, Computer and Communications Security (ASIACCS 2008)","author":"K. Bhargavan","year":"2008","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.D., Swamy, N.: Verified implementations of the Information Card federated identity-management protocol. In: Proceedings of the ACM Symposium on Information, Computer and Communications Security (ASIACCS 2008), pp. 123\u2013135. ACM Press, New York (2008)"},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1452044.1452049","volume":"31","author":"K. Bhargavan","year":"2008","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.D., Tse, S.: Verified interoperable implementations of security protocols. ACM TOPLAS\u00a031, 5:1\u20135:61 (2008)","journal-title":"ACM TOPLAS"},{"key":"3_CR14","first-page":"124","volume-title":"CSF","author":"K. Bhargavan","year":"2009","unstructured":"Bhargavan, K., Corin, R., Deni\u00e9lou, P.-M., Fournet, C., Leifer, J.J.: Cryptographic protocol synthesis and verification for multiparty sessions. In: CSF, pp. 124\u2013140. IEEE Computer Society, Los Alamitos (2009)"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1109\/CSF.2009.26","volume-title":"22nd IEEE Computer Security Foundations Symposium (CSF 2009)","author":"K. Bhargavan","year":"2009","unstructured":"Bhargavan, K., Corin, R., Deni\u00e9lou, P.-M., Fournet, C., Leifer, J.J.: Cryptographic protocol synthesis and verification for multiparty sessions. In: 22nd IEEE Computer Security Foundations Symposium (CSF 2009), pp. 124\u2013140. IEEE Computer Society, Los Alamitos (2009)"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Fournet, C., Gordon, A.D.: Modular verification of security protocol code by typing. In: ACM Symposium on Principles of Programming Languages (POPL 2010), pp. 445\u2013456 (2010)","DOI":"10.1145\/1706299.1706350"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055716","volume-title":"Advances in Cryptology - CRYPTO \u201998","author":"D. Bleichenbacher","year":"1998","unstructured":"Bleichenbacher, D.: Chosen ciphertext attacks against protocols based on the RSA encryption standard PKCS #1. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol.\u00a01462, pp. 1\u201312. Springer, Heidelberg (1998)"},{"issue":"2","key":"3_CR18","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1017\/S0956796810000134","volume":"21","author":"J. Borgstr\u00f6m","year":"2011","unstructured":"Borgstr\u00f6m, J., Gordon, A.D., Pucella, R.: Roles, stacks, histories: A triple for Hoare. Journal of Functional Programming\u00a021(2), 159\u2013207 (2011)","journal-title":"Journal of Functional Programming"},{"issue":"2-4","key":"3_CR19","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1016\/j.ic.2007.05.005","volume":"206","author":"I. Cervesato","year":"2008","unstructured":"Cervesato, I., Jaggard, A.D., Scedrov, A., Tsay, J.-K., Walstad, C.: Breaking and fixing public-key Kerberos. Information and Computation\u00a0206(2-4), 402\u2013424 (2008)","journal-title":"Information and Computation"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Chaki, S., Datta, A.: ASPIER: An automated framework for verifying security protocol implementations. In: IEEE Computer Security Foundations Symposium, pp. 172\u2013185 (2009)","DOI":"10.1109\/CSF.2009.20"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-19125-1_5","volume-title":"Engineering Secure Software and Systems","author":"R. Corin","year":"2011","unstructured":"Corin, R., Manzano, F.A.: Efficient symbolic execution for analysing cryptographic protocol implementations. In: Erlingsson, \u00da., Wieringa, R., Zannone, N. (eds.) ESSoS 2011. LNCS, vol.\u00a06542, pp. 58\u201372. Springer, Heidelberg (2011)"},{"issue":"2","key":"3_CR23","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"IT-29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory\u00a0IT-29(2), 198\u2013208 (1983)","journal-title":"IEEE Transactions on Information Theory"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Dupressoir, F., Gordon, A., J\u00fcrjens, J., Naumann, D.: Guiding a general-purpose C verifier to prove cryptographic protocols. In: 24th IEEE Computer Security Foundations Symposium (to appear, 2011)","DOI":"10.1109\/CSF.2011.8"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Eastlake, D., Jones, P.: US Secure Hash Algorithm 1 (SHA1). RFC 3174 (2001)","DOI":"10.17487\/rfc3174"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Fournet, C., Kohlweiss, M., Strub, P.-Y.: Modular code-based cryptographic verification. Technical report, sample code, and formal proofs (2011), http:\/\/research.microsoft.com\/~fournet\/comp-f7\/","DOI":"10.1145\/2046707.2046746"},{"issue":"2","key":"3_CR27","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1137\/0217017","volume":"17","author":"S. Goldwasser","year":"1988","unstructured":"Goldwasser, S., Micali, S., Rivest, R.: A digital signature scheme secure against adaptive chosen-message attack. SIAM Journal on Computing\u00a017(2), 281\u2013308 (1988)","journal-title":"SIAM Journal on Computing"},{"key":"3_CR28","volume-title":"Logics and Languages for Reliability and Security","author":"A.D. Gordon","year":"2010","unstructured":"Gordon, A.D., Fournet, C.: Principles and applications of refinement types. In: Esparza, J., Spanfelner, B., Grumberg, O. (eds.) Logics and Languages for Reliability and Security. IOS Press, Amsterdam (2010); Available as Microsoft Research Technical Report MSR\u2013TR\u20132009\u2013147"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-30579-8_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"J. Goubault-Larrecq","year":"2005","unstructured":"Goubault-Larrecq, J., Parrennes, F.: Cryptographic protocol analysis on real C code. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 363\u2013379. Springer, Heidelberg (2005)"},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-04444-1_11","volume-title":"Computer Security \u2013 ESORICS 2009","author":"N. Guts","year":"2009","unstructured":"Guts, N., Fournet, C., Zappa Nardelli, F.: Reliable evidence: Auditability by typing. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol.\u00a05789, pp. 168\u2013183. Springer, Heidelberg (2009)"},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Krawczyk, H., Bellare, M., Canetti, R.: HMAC: Keyed-hashing for message authentication. RFC 2104 (1997)","DOI":"10.17487\/rfc2104"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-61042-1_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Lowe","year":"1996","unstructured":"Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol.\u00a01055, pp. 147\u2013166. Springer, Heidelberg (1996)"},{"key":"3_CR33","volume-title":"Communicating and Mobile Systems: the \u03c0-Calculus","author":"R. Milner","year":"1999","unstructured":"Milner, R.: Communicating and Mobile Systems: the \u03c0-Calculus. Cambridge University Press, Cambridge (1999)"},{"issue":"12","key":"3_CR34","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1145\/359657.359659","volume":"21","author":"R. Needham","year":"1978","unstructured":"Needham, R., Schroeder, M.: Using encryption for authentication in large networks of computers. Commun. ACM\u00a021(12), 993\u2013999 (1978)","journal-title":"Commun. ACM"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-642-11747-3_7","volume-title":"Engineering Secure Software and Systems","author":"A. Pironti","year":"2010","unstructured":"Pironti, A., J\u00fcrjens, J.: Formally-based black-box monitoring of security protocols. In: Massacci, F., Wallach, D., Zannone, N. (eds.) ESSoS 2010. LNCS, vol.\u00a05965, pp. 79\u201395. Springer, Heidelberg (2010)"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1007\/978-3-642-11957-6_28","volume-title":"Programming Languages and Systems","author":"N. Swamy","year":"2010","unstructured":"Swamy, N., Chen, J., Chugh, R.: Enforcing stateful authorization and information flow policies in fine. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 529\u2013549. Springer, Heidelberg (2010)"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Swamy, N., Chen, J., Fournet, C., Strub, P.-Y., Bhargavan, K., Yang, J.: Secure distributed programming with value-dependent types. In: International Conference on Functional Programming, ICFP 2011 (to appear, 2011)","DOI":"10.1145\/2034773.2034811"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1007\/3-540-46035-7_35","volume-title":"Advances in Cryptology - EUROCRYPT 2002","author":"S. Vaudenay","year":"2002","unstructured":"Vaudenay, S.: Security flaws induced by CBC padding - applications to SSL, IPSEC, WTLS... In: Knudsen, L.R. (ed.) EUROCRYPT 2002. LNCS, vol.\u00a02332, pp. 534\u2013545. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Security Analysis and Design VI"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23082-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,30]],"date-time":"2021-11-30T01:27:24Z","timestamp":1638235644000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23082-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642230813","9783642230820"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23082-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}