{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T05:13:50Z","timestamp":1755839630159,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":76,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,11,15]],"date-time":"2023-11-15T00:00:00Z","timestamp":1700006400000},"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":[[2023,11,15]]},"DOI":"10.1145\/3576915.3623090","type":"proceedings-article","created":{"date-parts":[[2023,11,21]],"date-time":"2023-11-21T12:35:13Z","timestamp":1700570113000},"page":"1362-1376","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["CryptoBap: A Binary Analysis Platform for Cryptographic Protocols"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-3659-7755","authenticated-orcid":false,"given":"Faezeh","family":"Nasrabadi","sequence":"first","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0822-9283","authenticated-orcid":false,"given":"Robert","family":"K\u00fcnnemann","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9251-3679","authenticated-orcid":false,"given":"Hamed","family":"Nemati","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,11,21]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Mihail Aizatulin. 2011. Csec-Modex. https:\/\/github.com\/tari3x\/csec-modex."},{"key":"e_1_3_2_1_2_1","volume-title":"Verifying Cryptographic Security Implementations in C Using Automated Model Extraction. Ph.,D. Dissertation","author":"Aizatulin Mihail","year":"2001","unstructured":"Mihail Aizatulin. 2015. Verifying Cryptographic Security Implementations in C Using Automated Model Extraction. Ph.,D. Dissertation. The Open University. http:\/\/arxiv.org\/abs\/2001.00806"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046745"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382196.2382271"},{"volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning (Berlin","author":"Backes Michael","key":"e_1_3_2_1_5_1","unstructured":"Michael Backes, Matthias Berg, and Dominique Unruh. 2008. A Formal Language for Cryptographic Pseudocode. In Logic for Programming, Artificial Intelligence, and Reasoning (Berlin, Heidelberg), Iliano Cervesato, Helmut Veith, and Andrei Voronkov (Eds.). Springer, 353--376."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866351"},{"volume-title":"Advances in Cryptology - CRYPTO 2011 (Berlin","author":"Barthe Gilles","key":"e_1_3_2_1_7_1","unstructured":"Gilles Barthe, Benjamin Gregoire, Sylvain Heraud, and Santiago Zanella Beguelin. 2011. Computer-Aided Security Proofs for the Working Cryptographer. In Advances in Cryptology - CRYPTO 2011 (Berlin, Heidelberg), Phillip Rogaway (Ed.). Springer, 71--90."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/168588.168596"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_3_2_1_11_1","volume-title":"24th USENIX Security Symposium (USENIX Security 15)","author":"Beringer Lennart","year":"2015","unstructured":"Lennart Beringer, Adam Petcher, Q Ye Katherine, and Andrew W Appel. 2015a. Verified correctness and security of {OpenSSL}-{HMAC}. In 24th USENIX Security Symposium (USENIX Security 15). 207--221."},{"key":"e_1_3_2_1_12_1","volume-title":"Appel","author":"Beringer Lennart","year":"2015","unstructured":"Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. 2015b. Verified Correctness and Security of OpenSSL HMAC (SEC'15). USENIX Association, USA, 207--221."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.26"},{"key":"e_1_3_2_1_14_1","volume-title":"Everest: Towards a verified, drop-in replacement of HTTPS. In 2nd Summit on Advances in Programming Languages (SNAPL","author":"Bhargavan Karthikeyan","year":"2017","unstructured":"Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, et al. 2017. Everest: Towards a verified, drop-in replacement of HTTPS. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.14"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455770.1455828"},{"volume-title":"Third International Workshop, WS-FM 2006 Vienna, Austria, September 8-9, 2006, Proceedings. 88--106","author":"Bhargavan Karthikeyan","key":"e_1_3_2_1_17_1","unstructured":"Karthikeyan Bhargavan, C\u00e9dric Fournet, and Andrew D. Gordon. 2006. Verified Reference Implementations of WS-Security Protocols. In Web Services and Formal Methods, Third International Workshop, WS-FM 2006 Vienna, Austria, September 8-9, 2006, Proceedings. 88--106."},{"volume-title":"Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Bhargavan Karthikeyan","key":"e_1_3_2_1_18_1","unstructured":"Karthikeyan Bhargavan, C\u00e9dric Fournet, and Andrew D. Gordon. 2010. Modular Verification of Security Protocol Code by Typing. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Madrid, Spain) (POPL '10). Association for Computing Machinery, New York, NY, USA, 445--456."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1452044.1452049"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2001.930138"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2007.1005"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","unstructured":"Bruno Blanchet. 2011. Using Horn Clauses for Analyzing Security Protocols. (2011) 86--111. https:\/\/doi.org\/10.3233\/978-1-60750-714-7-86","DOI":"10.3233\/978-1-60750-714-7-86"},{"volume-title":"Physical-layer security: from information theory to security engineering","author":"Bloch Matthieu","key":"e_1_3_2_1_23_1","unstructured":"Matthieu Bloch and Joao Barros. 2011. Physical-layer security: from information theory to security engineering. Cambridge University Press."},{"key":"e_1_3_2_1_24_1","volume-title":"USENIX Security Symposium","volume":"152","author":"Bond Barry","year":"2017","unstructured":"Barry Bond, Chris Hawblitzel, Manos Kapritsos, K Rustan M Leino, Jacob R Lorch, Bryan Parno, Ashay Rane, Srinath TV Setty, and Laure Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code.. In USENIX Security Symposium, Vol. 152."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.comnet.2012.08.003"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ARES.2012.63"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.20"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00032"},{"volume-title":"Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security","author":"Cremers Cas","key":"e_1_3_2_1_29_1","unstructured":"Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, and Thyla van der Merwe. 2017-10-30. A Comprehensive Symbolic Analysis of TLS 1.3. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (New York, NY, USA) (CCS '17). Association for Computing Machinery, 1773--1788."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516702"},{"volume-title":"Proceedings of the 22nd Annual Symposium on Foundations of Computer Science (USA) (SFCS '81)","author":"Dolev D.","key":"e_1_3_2_1_31_1","unstructured":"D. Dolev and A. C. Yao. 1981. On the Security of Public Key Protocols. In Proceedings of the 22nd Annual Symposium on Foundations of Computer Science (USA) (SFCS '81). IEEE Computer Society, 350--357."},{"key":"e_1_3_2_1_32_1","volume-title":"WireGuard: Next Generation Kernel Network Tunnel. In 24th Annual Network and Distributed System Security Symposium, NDSS 2017","author":"Donenfeld Jason A.","year":"2017","unstructured":"Jason A. Donenfeld. 2017. WireGuard: Next Generation Kernel Network Tunnel. In 24th Annual Network and Distributed System Security Symposium, NDSS 2017, San Diego, California, USA, February 26 - March 1, 2017. https:\/\/www.ndss-symposium.org\/ndss2017\/ndss-2017-programme\/wireguard-next-generation-kernel-network-tunnel\/"},{"key":"e_1_3_2_1_33_1","unstructured":"Jason A Donenfeld and Kevin Milner. 2017. Formal verification of the WireGuard protocol. Technical Report Tech. Rep. (2017)."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-140508"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3421473.3421477"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.04.016"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90070-9"},{"key":"e_1_3_2_1_38_1","volume-title":"6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings. 363--379","author":"Goubault-Larrecq Jean","year":"2005","unstructured":"Jean Goubault-Larrecq and Fabrice Parrennes. 2005. Cryptographic Protocol Analysis on Real C Code. In Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17-19, 2005, Proceedings. 363--379."},{"key":"e_1_3_2_1_39_1","unstructured":"Shai Halevi. 2005. A plausible approach to computer-aided cryptographic proofs. https:\/\/eprint.iacr.org\/2005\/181"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2020.2971615"},{"key":"e_1_3_2_1_41_1","unstructured":"HOL development team. 2022. HOL Interactive Theorem Prover. https:\/\/hol-theorem-prover.org"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.08.009"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2019.00034"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-160556"},{"key":"e_1_3_2_1_46_1","volume-title":"ESORICS 2020, Guildford, UK, September 14-18, 2020, Proceedings, Part II. 525--545","author":"K\u00fcnnemann Robert","year":"2020","unstructured":"Robert K\u00fcnnemann and Hamed Nemati. 2020. MAC-in-the-Box: Verifying a Minimalistic Hardware Design for MAC Computation. In Computer Security - ESORICS 2020 - 25th European Symposium on Research in Computer Security, ESORICS 2020, Guildford, UK, September 14-18, 2020, Proceedings, Part II. 525--545."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455770.1455788"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.9"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"crossref","unstructured":"Adam Langley Mike Hamburg and Sean Turner. 2016. Elliptic curves for security. Technical Report.","DOI":"10.17487\/RFC7748"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_51_1","volume-title":"Proceedings of the Network and Distributed System Security Symposium, NDSS 2008","author":"Lin Zhiqiang","year":"2008","unstructured":"Zhiqiang Lin, Xuxian Jiang, Dongyan Xu, and Xiangyu Zhang. 2008. Automatic Protocol Format Reverse Engineering through Context-Aware Monitored Execution. In Proceedings of the Network and Distributed System Security Symposium, NDSS 2008, San Diego, California, USA, 10th February - 13th February 2009."},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2304.08848"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.01.001"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2019.00026"},{"volume-title":"Programming Languages and Systems (Berlin","author":"Lochbihler Andreas","key":"e_1_3_2_1_55_1","unstructured":"Andreas Lochbihler. 2016. Probabilistic Functions and Cryptographic Oracles in Higher Order Logic. In Programming Languages and Systems (Berlin, Heidelberg), Peter Thiemann (Ed.). Springer, 503--531."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(95)00144-2"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/794197.795075"},{"volume-title":"The TAMARIN Prover for the Symbolic Analysis of Security Protocols","author":"Meier Simon","key":"e_1_3_2_1_58_1","unstructured":"Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. 2013. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In Computer Aided Verification, David Hutchison, Takeo Kanade, Josef Kittler, Jon M. Kleinberg, Friedemann Mattern, John C. Mitchell, Moni Naor, Oscar Nierstrasz, C. Pandu Rangan, Bernhard Steffen, Madhu Sudan, Demetri Terzopoulos, Doug Tygar, Moshe Y. Vardi, Gerhard Weikum, Natasha Sharygina, and Helmut Veith (Eds.). Vol. 8044. Springer Berlin Heidelberg, Berlin, Heidelberg, 696--701."},{"key":"e_1_3_2_1_59_1","volume-title":"Workshop on formal methods and security protocols. Citeseer.","author":"Mitchell J","year":"1999","unstructured":"J Mitchell, A Scedrov, N Durgin, and P Lincoln. 1999. Undecidability of bounded security protocols. In Workshop on formal methods and security protocols. Citeseer."},{"key":"e_1_3_2_1_60_1","unstructured":"Jan Mojzis. 2018. The SSH Library. https:\/\/github.com\/janmojzis\/tinyssh."},{"key":"e_1_3_2_1_61_1","volume-title":"CryptoBap: A Binary Analysis Platform for Cryptographic Protocols. arXiv preprint arXiv","author":"Nasrabadi Faezeh","year":"2023","unstructured":"Faezeh Nasrabadi, Robert K\u00fcnnemann, and Hamed Nemati. 2023. CryptoBap: A Binary Analysis Platform for Cryptographic Protocols. arXiv preprint arXiv (2023). http:\/\/arxiv.org\/abs\/2308.14450"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359659"},{"key":"e_1_3_2_1_63_1","volume-title":"Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS-2008)","author":"O'Shea Nicholas","year":"2008","unstructured":"Nicholas O'Shea. 2008. Using Elyjah to analyse Java implementations of cryptographic protocols. In Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security (FCS-ARSPA-WITS-2008)."},{"key":"e_1_3_2_1_64_1","volume-title":"Why should anyone use colours? or, syntax highlighting beyond code snippets. arXiv preprint arXiv:2001.11334","author":"Patrignani Marco","year":"2020","unstructured":"Marco Patrignani. 2020. Why should anyone use colours? or, syntax highlighting beyond code snippets. arXiv preprint arXiv:2001.11334 (2020)."},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2015.36"},{"key":"e_1_3_2_1_66_1","volume-title":"Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties. In 2012 IEEE 25th Computer Security Foundations Symposium. 78--94","author":"Schmidt Benedikt","year":"2012","unstructured":"Benedikt Schmidt, Simon Meier, Cas Cremers, and David Basin. 2012-06. Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties. In 2012 IEEE 25th Computer Security Foundations Symposium. 78--94. ISSN: 2377--5459."},{"key":"e_1_3_2_1_67_1","unstructured":"Huzaifa Sidhpurwala. 2019. Security flaws caused by compiler optimizations. https:\/\/www.redhat.com\/en\/blog\/security-flaws-caused-compiler-optimizations"},{"key":"e_1_3_2_1_68_1","volume-title":"2018 IEEE European Symposium on Security and Privacy, Euro S&P 2018","author":"Simon Laurent","year":"2018","unstructured":"Laurent Simon, David Chisnall, and Ross J. Anderson. 2018. What You Get is What You C: Controlling Side Effects in Mainstream C Compilers. In 2018 IEEE European Symposium on Security and Privacy, Euro S&P 2018, London, United Kingdom, April 24-26, 2018. 1--15."},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336772"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522728"},{"key":"e_1_3_2_1_71_1","volume-title":"Testing Network Protocol Binary Software with Selective Symbolic Execution. In 12th International Conference on Computational Intelligence and Security, CIS 2016","author":"Wen Shameng","year":"2016","unstructured":"Shameng Wen, Chao Feng, Qingkun Meng, Bin Zhang, Ligeng Wu, and Chaojing Tang. 2016. Testing Network Protocol Binary Software with Selective Symbolic Execution. In 12th International Conference on Computational Intelligence and Security, CIS 2016, Wuxi, China, December 16-19, 2016. 318--322."},{"key":"e_1_3_2_1_72_1","volume-title":"Proceedings of the Network and Distributed System Security Symposium, NDSS 2008","author":"Wondracek Gilbert","year":"2008","unstructured":"Gilbert Wondracek, Paolo Milani Comparetti, Christopher Kr\u00fcgel, and Engin Kirda. 2008. Automatic Network Protocol Analysis. In Proceedings of the Network and Distributed System Security Symposium, NDSS 2008, San Diego, California, USA, 10th February - 13th February 2009."},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.3233\/JIFS-169067"},{"key":"e_1_3_2_1_74_1","volume-title":"Proceedings of the 32th USENIX Conference on Security Symposium (SEC '23)","author":"Xu Jianhao","year":"2023","unstructured":"Jianhao Xu, Kangjie Lu, Zhengjie Du, Zhu Ding, Linke Li, Qiushi Wu, Mathias Payer, and Bing Mao. 2023. Silent Bugs Matter: A Study of Compiler-Introduced Security Bugs. In Proceedings of the 32th USENIX Conference on Security Symposium (SEC '23). USENIX Association. https:\/\/www.usenix.org\/system\/files\/sec23fall-prepub-123-xu-jianhao.pdf"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3133974"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"event":{"name":"CCS '23: ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Copenhagen Denmark","acronym":"CCS '23"},"container-title":["Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576915.3623090","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3576915.3623090","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T01:36:22Z","timestamp":1755740182000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576915.3623090"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,15]]},"references-count":76,"alternative-id":["10.1145\/3576915.3623090","10.1145\/3576915"],"URL":"https:\/\/doi.org\/10.1145\/3576915.3623090","relation":{},"subject":[],"published":{"date-parts":[[2023,11,15]]},"assertion":[{"value":"2023-11-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}