{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T11:00:53Z","timestamp":1790420453023,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,10,16]],"date-time":"2012-10-16T00:00:00Z","timestamp":1350345600000},"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":[[2012,10,16]]},"DOI":"10.1145\/2382196.2382271","type":"proceedings-article","created":{"date-parts":[[2012,10,15]],"date-time":"2012-10-15T17:13:12Z","timestamp":1350321192000},"page":"712-723","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Computational verification of C protocol implementations by symbolic execution"],"prefix":"10.1145","author":[{"given":"Mihhail","family":"Aizatulin","sequence":"first","affiliation":[{"name":"Open University, Milton Keynes, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrew D.","family":"Gordon","sequence":"additional","affiliation":[{"name":"Microsoft Research Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan","family":"J\u00fcrjens","sequence":"additional","affiliation":[{"name":"TU Dortmund & Fraunhofer ISST, Dortmund, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2012,10,16]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_5"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/647318.723498"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368310"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29420-4_1"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046745"},{"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":"Proceedings of the Fourth International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010","volume":"33","author":"Barbosa M.","year":"2010","unstructured":"M. Barbosa , J. Pinto , J. Filli\u00e2tre , and B. Vieira . A deductive verification platform for cryptographic software . In Proceedings of the Fourth International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010 ), volume 33 of Electronic Communications of the EASST. EASST , 2010 . M. Barbosa, J. Pinto, J. Filli\u00e2tre, and B. Vieira. A deductive verification platform for cryptographic software. In Proceedings of the Fourth International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010), volume 33 of Electronic Communications of the EASST. EASST, 2010."},{"key":"e_1_3_2_1_10_1","series-title":"Lecture Notes in Computer Science","volume-title":"Advances in Cryptology -- CRYPTO","author":"Barthe G.","year":"2011","unstructured":"G. Barthe , B. Gr\u00e9goire , S. Heraud , and S. Zanella B\u00e9guelin . Computer-aided security proofs for the working cryptographer . In Advances in Cryptology -- CRYPTO 2011 , Lecture Notes in Computer Science . Springer , 2011. G. Barthe, B. Gr\u00e9goire, S. Heraud, and S. Zanella B\u00e9guelin. Computer-aided security proofs for the working cryptographer. In Advances in Cryptology -- CRYPTO 2011, Lecture Notes in Computer Science. Springer, 2011."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.27"},{"key":"e_1_3_2_1_12_1","volume-title":"Oct.","author":"Bhargavan K.","year":"2009","unstructured":"K. Bhargavan , R. Corin , C. Fournet , and E. Zalinescu . Automated computational verification for cryptographic protocol implementations. Unpublished draft , Oct. 2009 . K. Bhargavan, R. Corin, C. Fournet, and E. Zalinescu. Automated computational verification for cryptographic protocol implementations. Unpublished draft, Oct. 2009."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455770.1455828"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706350"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368310.1368330"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2006.32"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873511"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2007.16"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2007.1005"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368310.1368326"},{"key":"e_1_3_2_1_21_1","volume-title":"USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008","author":"Cadar C.","year":"2008","unstructured":"C. Cadar , D. Dunbar , and D. Engler . KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs . In USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008 ), San Diego, CA , Dec. 2008 . C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008), San Diego, CA, Dec. 2008."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARES.2012.63"},{"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.5555\/1946341.1946348"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9187-9"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2011.8"},{"key":"e_1_3_2_1_28_1","volume-title":"Computer Science Laboratory","author":"Dutertre B.","year":"2006","unstructured":"B. Dutertre and L. D. Moura . The Yices SMT Solver. Technical report , Computer Science Laboratory , SRI International , 2006 . B. Dutertre and L. D. Moura. The Yices SMT Solver. Technical report, Computer Science Laboratory, SRI International, 2006."},{"key":"e_1_3_2_1_29_1","series-title":"Lecture Notes in Computer Science","volume-title":"Foundations of Security and Design VI (FOSAD","author":"Fournet C.","year":"2010","unstructured":"C. Fournet , K. Bhargavan , and A. D. Gordon . Cryptographic verification by typing for a sample protocol implementation . In Foundations of Security and Design VI (FOSAD 2010 ), Lecture Notes in Computer Science . Springer , 2011. To appear. C. Fournet, K. Bhargavan, and A. D. Gordon. Cryptographic verification by typing for a sample protocol implementation. In Foundations of Security and Design VI (FOSAD 2010), Lecture Notes in Computer Science. Springer, 2011. To appear."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046746"},{"key":"e_1_3_2_1_31_1","unstructured":"http:\/\/frama-c.cea.fr\/ 2009.  http:\/\/frama-c.cea.fr\/ 2009."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/646486.694632"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90070-9"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.43"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_24"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1103576.1103580"},{"key":"e_1_3_2_1_38_1","unstructured":"C. Hritcu. Union Intersection and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis. PhD thesis Department of Computer Science Saarland University 2011.  C. Hritcu. Union Intersection and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis. PhD thesis Department of Computer Science Saarland University 2011."},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis","author":"Jeffrey A.","year":"2006","unstructured":"A. Jeffrey and R. Ley-Wild . Dynamic model checking of C cryptographic protocol implementations . In Proceedings of Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis , 2006 . A. Jeffrey and R. Ley-Wild. Dynamic model checking of C cryptographic protocol implementations. In Proceedings of Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis, 2006."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9188-8"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.9"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1653662.1653674"},{"key":"e_1_3_2_1_44_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"776","DOI":"10.1007\/3-540-48119-2_43","volume-title":"World Congress on Formal Methods","author":"Lincoln P.","year":"1999","unstructured":"P. Lincoln , J. C. Mitchell , M. Mitchell , and A. Scedrov . Probabilistic polynomial-time equivalence and security analysis . In J. M. Wing, J. Woodcock, and J. Davies, editors, World Congress on Formal Methods , volume 1708 of Lecture Notes in Computer Science , pages 776 -- 793 . Springer , 1999 . P. Lincoln, J. C. Mitchell, M. Mitchell, and A. Scedrov. Probabilistic polynomial-time equivalence and security analysis. In J. M. Wing, J. Woodcock, and J. Davies, editors, World Congress on Formal Methods, volume 1708 of Lecture Notes in Computer Science, pages 776--793. Springer, 1999."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/647478.727796"},{"key":"e_1_3_2_1_46_1","unstructured":"PolarSSL. http:\/\/polarssl.org.  PolarSSL. http:\/\/polarssl.org."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_5"},{"key":"e_1_3_2_1_48_1","volume-title":"Security protocols open repository","author":"EVA.","year":"2007","unstructured":"Project EVA. Security protocols open repository , 2007 . http:\/\/www.lsv.ens-cachan.fr\/spore\/. Project EVA. Security protocols open repository, 2007. http:\/\/www.lsv.ens-cachan.fr\/spore\/."},{"key":"e_1_3_2_1_50_1","first-page":"193","volume-title":"Rule-Based static analysis of network protocol implementations. IN PROCEEDINGS OF THE 15TH USENIX SECURITY SYMPOSIUM","author":"Udrea O.","year":"2006","unstructured":"O. Udrea , C. Lumezanu , and J. S. Foster . Rule-Based static analysis of network protocol implementations. IN PROCEEDINGS OF THE 15TH USENIX SECURITY SYMPOSIUM , pages 193 -- 208 , 2006 . O. Udrea, C. Lumezanu, and J. S. Foster. Rule-Based static analysis of network protocol implementations. IN PROCEEDINGS OF THE 15TH USENIX SECURITY SYMPOSIUM, pages 193--208, 2006."},{"key":"e_1_3_2_1_51_1","volume-title":"July","author":"Unruh D.","year":"2010","unstructured":"D. Unruh . The impossibility of computationally sound XOR , July 2010 . Preprint on IACR ePrint 2010\/389. D. Unruh. The impossibility of computationally sound XOR, July 2010. Preprint on IACR ePrint 2010\/389."}],"event":{"name":"CCS'12: the ACM Conference on Computer and Communications Security","location":"Raleigh North Carolina USA","acronym":"CCS'12","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2012 ACM conference on Computer and communications security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2382196.2382271","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2382196.2382271","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:34:48Z","timestamp":1750239288000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2382196.2382271"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,16]]},"references-count":49,"alternative-id":["10.1145\/2382196.2382271","10.1145\/2382196"],"URL":"https:\/\/doi.org\/10.1145\/2382196.2382271","relation":{},"subject":[],"published":{"date-parts":[[2012,10,16]]},"assertion":[{"value":"2012-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}