{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:21:23Z","timestamp":1770283283076,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,10,17]],"date-time":"2011-10-17T00:00:00Z","timestamp":1318809600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2011,10,17]]},"DOI":"10.1145\/2046707.2046746","type":"proceedings-article","created":{"date-parts":[[2011,10,18]],"date-time":"2011-10-18T13:02:00Z","timestamp":1318942920000},"page":"341-350","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":52,"title":["Modular code-based cryptographic verification"],"prefix":"10.1145","author":[{"given":"C\u00e9dric","family":"Fournet","sequence":"first","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}]},{"given":"Markulf","family":"Kohlweiss","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}]},{"given":"Pierre-Yves","family":"Strub","sequence":"additional","affiliation":[{"name":"MSR-INRIA Joint Centre, Orsay, France"}]}],"member":"320","published-online":{"date-parts":[[2011,10,17]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/324133.324266"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1044731.1044735"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-001-0014-7"},{"issue":"3","key":"e_1_3_2_1_4_1","volume":"4","author":"Backes M.","year":"2005","unstructured":"M. Backes , B. Pfitzmann , and M. Waidner . Symmetric authentication in a simulatable Dolev-Yao-style cryptographic library. Int. J. Inf. Sec. , 4 ( 3 ), 2005 . M. Backes, B. Pfitzmann, and M. Waidner. Symmetric authentication in a simulatable Dolev-Yao-style cryptographic library. Int. J. Inf. Sec., 4 (3), 2005.","journal-title":"Symmetric authentication in a simulatable Dolev-Yao-style cryptographic library. Int. J. Inf. Sec."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.05.002"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-007-0046-6"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1653662.1653672"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866351"},{"key":"e_1_3_2_1_9_1","volume-title":"FAST 2008","author":"Barthe G.","year":"2008","unstructured":"G. Barthe , B. Gr\u00e9goire , S. Heraud , and S. Z. B\u00e9guelin . Formal certification of ElGamal encryption . In FAST 2008 , 2008 . G. Barthe, B. Gr\u00e9goire, S. Heraud, and S. Z. B\u00e9guelin. Formal certification of ElGamal encryption. In FAST 2008, 2008."},{"key":"e_1_3_2_1_10_1","volume-title":"Advances in Cryptology -- CRYPTO","author":"Barthe G.","year":"2011","unstructured":"easycrypt2011 G. Barthe , B. Gregoire , S. Heraud , and S. Zanella B\u00e9guelin . Computer-aided security proofs for the working cryptographer . In Advances in Cryptology -- CRYPTO 2011 , 2011. easycrypt2011G. Barthe, B. Gregoire, S. Heraud, and S. Zanella B\u00e9guelin. Computer-aided security proofs for the working cryptographer. In Advances in Cryptology -- CRYPTO 2011, 2011."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00145-008-9026-x"},{"key":"e_1_3_2_1_12_1","volume-title":"UCSD CSE 207 Course Notes","author":"Bellare M.","year":"2005","unstructured":"M. Bellare and P. Rogaway . Introduction to modern cryptography . In UCSD CSE 207 Course Notes , 2005 . M. Bellare and P. Rogaway. Introduction to modern cryptography. In UCSD CSE 207 Course Notes, 2005."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11761679_25"},{"key":"e_1_3_2_1_14_1","volume-title":"Advances in Cryptology -- CRYPTO '96","author":"Bellare M.","year":"1996","unstructured":"M. Bellare , R. Canetti , and H. Krawczyk . Keying hash functions for message authentication . In Advances in Cryptology -- CRYPTO '96 , 1996 . M. Bellare, R. Canetti, and H. Krawczyk. Keying hash functions for message authentication. In Advances in Cryptology -- CRYPTO '96, 1996."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455770.1455828"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368310.1368330"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.26"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706350"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.1"},{"key":"e_1_3_2_1_21_1","volume-title":"Automated verification of selected equivalences for security protocols. JLAP, 75 (1)","author":"Blanchet B.","year":"2008","unstructured":"B. Blanchet , M. Abadi , and C. Fournet . Automated verification of selected equivalences for security protocols. JLAP, 75 (1) , 2008 . B. Blanchet, M. Abadi, and C. Fournet. Automated verification of selected equivalences for security protocols. JLAP, 75 (1), 2008."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/874063.875553"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.20"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_2"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.012"},{"key":"e_1_3_2_1_27_1","author":"Dolev D.","year":"1983","unstructured":"D. Dolev and A. Yao . On the security of public key protocols. IEEE Transactions on Information Theory, IT--29 (2) , 1983 . D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, IT--29 (2), 1983.","journal-title":"On the security of public key protocols. IEEE Transactions on Information Theory, IT--29 (2)"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2011.8"},{"key":"e_1_3_2_1_29_1","volume-title":"A compositional logic for proving security properties of protocols. JCS, 11 (4)","author":"Durgin N. A.","year":"2003","unstructured":"N. A. Durgin , J. C. Mitchell , and D. Pavlovic . A compositional logic for proving security properties of protocols. JCS, 11 (4) , 2003 . N. A. Durgin, J. C. Mitchell, and D. Pavlovic. A compositional logic for proving security properties of protocols. JCS, 11 (4), 2003."},{"key":"e_1_3_2_1_30_1","volume-title":"FOSAD","author":"Fournet C.","year":"2011","unstructured":"C. Fournet , K. Bhargavan , and A. Gordon . Cryptographic verification of protocol implementations by typechecking . In FOSAD , 2011 . C. Fournet, K. Bhargavan, and A. Gordon. Cryptographic verification of protocol implementations by typechecking. In FOSAD, 2011."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1137\/0217017"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_24"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539794263452"},{"key":"e_1_3_2_1_36_1","first-page":"2104","author":"Krawczyk H.","year":"1997","unstructured":"H. Krawczyk , M. Bellare , and R. Canetti . HMAC: Keyed-hashing for message authentication , 1997 . RFC 2104 . H. Krawczyk, M. Bellare, and R. Canetti. HMAC: Keyed-hashing for message authentication, 1997. RFC 2104.","journal-title":"HMAC: Keyed-hashing for message authentication"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.30"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.18"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/645395.651928"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1102120.1102126"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328479"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/361932.361937"},{"key":"e_1_3_2_1_43_1","volume-title":"Advances in Cryptology -- CRYPTO'91","author":"Rackoff C.","year":"1991","unstructured":"C. Rackoff and D. R. Simon . Non-interactive zero-knowledge proof of knowledge and chosen ciphertext attack . In Advances in Cryptology -- CRYPTO'91 , 1991 . C. Rackoff and D. R. Simon. Non-interactive zero-knowledge proof of knowledge and chosen ciphertext attack. In Advances in Cryptology -- CRYPTO'91, 1991."},{"key":"e_1_3_2_1_44_1","volume-title":"IFIP Congress","author":"Reynolds J. C.","year":"1983","unstructured":"J. C. Reynolds . Types, abstraction and parametric polymorphism . In IFIP Congress , 1983 . J. C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP Congress, 1983."},{"key":"e_1_3_2_1_45_1","volume-title":"Inductive trace properties for computational security. JCS, 18 (6)","author":"Roy A.","year":"2010","unstructured":"A. Roy , A. Datta , A. Derek , and J. C. Mitchell . Inductive trace properties for computational security. JCS, 18 (6) , 2010 . A. Roy, A. Datta, A. Derek, and J. C. Mitchell. Inductive trace properties for computational security. JCS, 18 (6), 2010."},{"key":"e_1_3_2_1_46_1","volume-title":"The Coq Proof Assistant Reference Manual -- Version V8.3","author":"Development Team The Coq","year":"2011","unstructured":"The Coq Development Team . The Coq Proof Assistant Reference Manual -- Version V8.3 , 2011 . The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.3, 2011."}],"event":{"name":"CCS'11: the ACM Conference on Computer and Communications Security","location":"Chicago Illinois USA","acronym":"CCS'11","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 18th ACM conference on Computer and communications security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2046707.2046746","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2046707.2046746","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:48:42Z","timestamp":1750240122000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2046707.2046746"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,10,17]]},"references-count":43,"alternative-id":["10.1145\/2046707.2046746","10.1145\/2046707"],"URL":"https:\/\/doi.org\/10.1145\/2046707.2046746","relation":{},"subject":[],"published":{"date-parts":[[2011,10,17]]},"assertion":[{"value":"2011-10-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}