{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T04:16:35Z","timestamp":1743653795354,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642294198"},{"type":"electronic","value":"9783642294204"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29420-4_1","type":"book-chapter","created":{"date-parts":[[2012,6,25]],"date-time":"2012-06-25T13:12:33Z","timestamp":1340629953000},"page":"1-20","source":"Crossref","is-referenced-by-count":4,"title":["Verifying Cryptographic Code in C: Some Experience and the Csec Challenge"],"prefix":"10.1007","author":[{"given":"Mihhail","family":"Aizatulin","sequence":"first","affiliation":[]},{"given":"Fran\u00e7ois","family":"Dupressoir","sequence":"additional","affiliation":[]},{"given":"Andrew D.","family":"Gordon","sequence":"additional","affiliation":[]},{"given":"Jan","family":"J\u00fcrjens","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: ACM POPL, pp. 104\u2013115 (2001)","DOI":"10.1145\/373243.360213"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Aizatulin, M., Dupressoir, F., Gordon, A., J\u00fcrjens, J.: Verifying cryptographic code in C: Some experience and the Csec challenge. Technical Report MSR-TR-2011-118, Microsoft Research (November 2011a)","DOI":"10.1007\/978-3-642-29420-4_1"},{"key":"1_CR3","unstructured":"Aizatulin, M., Gordon, A., J\u00fcrjens, J.: Extracting and verifying cryptographic models from C protocol code by symbolic execution. In: 18th ACM Conference on Computer and Communications Security, CCS 2011 (2011), http:\/\/arxiv.org\/abs\/1107.1017"},{"key":"#cr-split#-1_CR4.1","doi-asserted-by":"crossref","unstructured":"Backes, M., Hofheinz, D., Unruh, D.: CoSP: A general framework for computational soundness proofs. In: ACM CCS 2009, pp. 66-78 (November 2009)","DOI":"10.1145\/1653662.1653672"},{"key":"#cr-split#-1_CR4.2","doi-asserted-by":"crossref","unstructured":"preprint on IACR ePrint 2009\/080","DOI":"10.1088\/1126-6708\/2009\/04\/080"},{"key":"1_CR5","unstructured":"Barbosa, M., Pinto, J., Filli\u00e2tre, J., Vieira, B.: 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). Electronic Communications of the EASST, vol.\u00a033. EASST (2010)"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. In: 21st IEEE Computer Security Foundations Symposium (CSF 2008), pp. 17\u201332 (2008)","DOI":"10.1109\/CSF.2008.27"},{"key":"1_CR7","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\/1707801.1706350"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: IEEE Computer Security Foundations Workshop (CSFW 2001), pp. 82\u201396 (2001)","DOI":"10.1109\/CSFW.2001.930138"},{"key":"1_CR9","unstructured":"Cadar, C., Dunbar, D., Engler, D.: 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 (December 2008)"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Chaki, S., Datta, A.: ASPIER: An automated framework for verifying security protocol implementations. In: Computer Security Foundations Workshop, pp. 172\u2013185 (2009), doi:10.1109\/CSF.2009.20","DOI":"10.1109\/CSF.2009.20"},{"key":"1_CR11","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":"1_CR12","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)"},{"key":"1_CR13","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, pp. 3\u201317 (2011)","DOI":"10.1109\/CSF.2011.8"},{"key":"1_CR14","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT Solver. Technical report (2006)"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Erk\u00f6k, L., Carlsson, M., Wick, A.: Hardware\/software co-verification of cryptographic algorithms using Cryptol. In: FMCAD (2009)","DOI":"10.1109\/FMCAD.2009.5351121"},{"key":"1_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-23082-0_3","volume-title":"Foundations of Security Analysis and Design VI","author":"C. Fournet","year":"2011","unstructured":"Fournet, C., Bhargavan, K., Gordon, A.D.: Cryptographic Verification by Typing for a Sample Protocol Implementation. In: Aldini, A., Gorrieri, R. (eds.) FOSAD 2011. LNCS, vol.\u00a06858, pp. 66\u2013100. Springer, Heidelberg (2011)"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Fournet, C., Kohlweiss, M., Strub, P.-Y.: Modular code-based cryptographic verification. In: 18th ACM Conference on Computer and Communications Security, CCS 2011 (2011) Technical report, sample code, and formal proofs available from, http:\/\/research.microsoft.com\/~fournet\/comp-f7\/","DOI":"10.1145\/2046707.2046746"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/3-540-46002-0_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Godefroid","year":"2002","unstructured":"Godefroid, P., Khurshid, S.: Exploring Very Large State Spaces using Genetic Algorithms. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 266\u2013280. Springer, Heidelberg (2002)"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Programming Language Design and Implementation (PLDI 2005), pp. 213\u2013223. ACM (2005)","DOI":"10.1145\/1065010.1065036"},{"key":"1_CR20","unstructured":"Godefroid, P., Levin, M.Y., Molnar, D.A.: Automated whitebox fuzz testing. In: Proceedings of the Network and Distributed System Security Symposium, NDSS 2008. The Internet Society (2008)"},{"key":"1_CR21","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":"1_CR22","unstructured":"Hri\u0163cu, C.: Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis. PhD thesis, Department of Computer Science, Saarland University (2011)"},{"issue":"7","key":"1_CR23","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"J.C. King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM\u00a019(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"1_CR24","unstructured":"McGrew, D.A., Viega, J.: Flexible and efficient message authentication in hardware and software. manuscript and software available at (2005), http:\/\/www.zork.org\/gcm"},{"key":"1_CR25","first-page":"213","volume-title":"Proceedings of the 11th International Conference on Compiler Construction, CC 2002","author":"G.C. Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: Proceedings of the 11th International Conference on Compiler Construction, CC 2002, pp. 213\u2013228. Springer, London (2002) ISBN 3-540-43369-4, http:\/\/portal.acm.org\/citation.cfm?id=647478.727796"},{"key":"1_CR26","unstructured":"PolarSSL. PolarSSL, http:\/\/polarssl.org"},{"key":"1_CR27","unstructured":"Polikarpova, N., Moskal, M.: Verifying implementations of security protocols by refinement. In: Verified Software: Theories, Tools and Experiments, VSTTE 2012 (to appear, 2012)"},{"key":"1_CR28","unstructured":"Project EVA. Security protocols open repository (2007), http:\/\/www.lsv.ens-cachan.fr\/spore\/"},{"key":"1_CR29","unstructured":"Udrea, O., Lumezanu, C., Foster, J.S.: Rule-Based static analysis of network protocol implementations. In: Proceedings of the 15Th Usenix Security Symposium, pp. 193\u2013208 (2006), http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.111.8168"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects of Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29420-4_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,2]],"date-time":"2025-04-02T14:59:17Z","timestamp":1743605957000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-29420-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642294198","9783642294204"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29420-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}