{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T07:15:04Z","timestamp":1763968504230,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T00:00:00Z","timestamp":1673395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,11]]},"DOI":"10.1145\/3573105.3575684","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"275-289","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["ASN1*: Provably Correct, Non-malleable Parsing for ASN.1 DER"],"prefix":"10.1145","author":[{"given":"Haobin","family":"Ni","sequence":"first","affiliation":[{"name":"Cornell University, USA"}]},{"given":"Antoine","family":"Delignat-Lavaud","sequence":"additional","affiliation":[{"name":"Microsoft Research, UK"}]},{"given":"C\u00e9dric","family":"Fournet","sequence":"additional","affiliation":[{"name":"Microsoft Research, UK"}]},{"given":"Tahina","family":"Ramananandro","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]},{"given":"Nikhil","family":"Swamy","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Verified Software Toolchain","author":"Appel Andrew W.","year":"1971","unstructured":"Andrew W. Appel. 2011. Verified Software Toolchain. In Programming Languages and Systems, Gilles Barthe (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 1\u201317. isbn:978-3-642-19718-5"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159789.1159792"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.05.004"},{"key":"e_1_3_2_1_4_1","volume-title":"Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. In 11th International Conference on Mathematics of Program Construction (Lecture Notes in Computer Science","volume":"6","author":"Barthe Gilles","year":"2012","unstructured":"Gilles Barthe, Benjamin Gr\u00e9goire, and Santiago Zanella-B\u00e9guelin. 2012. Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. In 11th International Conference on Mathematics of Program Construction (Lecture Notes in Computer Science, Vol. 7342). Springer, 1\u20136. http:\/\/hal.inria.fr\/docs\/00\/76\/58\/64\/PDF\/main.pdf"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.15"},{"key":"e_1_3_2_1_7_1","unstructured":"Sze Yiu Chau. 2019. A Decade After Bleichenbacher\u201906 RSA Signature Forgery Still Works. Black Hat USA."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.40"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786835"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786835"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"D. Cooper S. Santesson S. Farrell S. Boeyen R. Housley and W. Polk. 2008. Internet X.509 Public Key Infrastructure Certificate and Certificate Revocation List (CRL) Profile. https:\/\/www.ietf.org\/rfc\/rfc5280.txt","DOI":"10.17487\/rfc5280"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341686"},{"volume-title":"Constructing Semantic Models of Programs with the Software Analysis Workbench","author":"Dockins Robert","key":"e_1_3_2_1_14_1","unstructured":"Robert Dockins, Adam Foltzer, Joe Hendrix, Brian Huffman, Dylan McNamee, and Aaron Tomb. 2016. Constructing Semantic Models of Programs with the Software Analysis Workbench. In Verified Software. Theories, Tools, and Experiments, Sandrine Blazy and Marsha Chechik (Eds.). Springer International Publishing, Cham. 56\u201372. isbn:978-3-319-48869-1"},{"key":"e_1_3_2_1_15_1","unstructured":"Hal Finney. 2006. Bleichenbacher\u2019s RSA signature forgery based on implementation error. http:\/\/imc.org\/ietf-openpgp\/mail-archive\/msg14307.html"},{"key":"e_1_3_2_1_16_1","unstructured":"Electronic Frontier Foundation. 2010. The EFF SSL Observatory. https:\/\/www.eff.org\/observatory"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2093548.2093564"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167090"},{"key":"e_1_3_2_1_19_1","unstructured":"ITU. 2021. Abstract Syntax Notation One ASN.1: Specification of basic notation. https:\/\/www.itu.int\/rec\/t-rec-x.680\/en"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2017.14"},{"key":"e_1_3_2_1_21_1","volume-title":"SICHERHEIT","author":"K\u00fchn Ulrich","year":"2008","unstructured":"Ulrich K\u00fchn, Andrei Pyshkin, Erik Tews, and Ralf-Philipp Weinmann. 2008. Variants of Bleichenbacher\u2019s low-exponent attack on PKCS# 1 RSA signatures. SICHERHEIT 2008."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451167"},{"key":"e_1_3_2_1_23_1","unstructured":"Moxie Marlinspike. 2009. Null Prefix attack against TLS Server Certificates. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2009-2510"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73408-6_10"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.27"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SPW50608.2020.00065"},{"key":"e_1_3_2_1_27_1","volume-title":"Proceedings of the 28th USENIX Conference on Security Symposium (USENIX Security 2019","author":"Ramananandro Tahina","year":"2019","unstructured":"Tahina Ramananandro, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019. EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In Proceedings of the 28th USENIX Conference on Security Symposium (USENIX Security 2019). USENIX Association, USA. 1465\u20131482. isbn:9781939133069"},{"key":"e_1_3_2_1_28_1","unstructured":"Christian Rinderknecht. 1998. Une formalisation d\u2019ASN.1 - Application d\u2019une m\u00e9thode formelle \u00e0 un langage de sp\u00e9cification t\u00e9l\u00e9com. Ph. D. Dissertation."},{"key":"e_1_3_2_1_29_1","unstructured":"Michael Scire Melissa Mears Devon Maloney Matthew Norman Shaun Tux and Phoebe Monroe. 2018. Attacking the Nintendo 3DS Boot ROMs. arXiv preprint arXiv:1802.00359."},{"key":"e_1_3_2_1_30_1","unstructured":"Paul Steckler. 2007. A Formal Semantics for ASN.1. High-Confidence Software and Systems (HCSS)."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523708"},{"volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Tao Zhe","key":"e_1_3_2_1_33_1","unstructured":"Zhe Tao, Aseem Rastogi, Naman Gupta, Kapil Vaswani, and Aditya V. Thakur. 2021. DICE*: A Formally Verified Implementation of DICE Measured Boot. In 30th USENIX Security Symposium (USENIX Security 21). USENIX Association, 1091\u20131107. isbn:978-1-939133-24-3 https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/tao"},{"volume-title":"Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System","author":"Tullsen Mark","key":"e_1_3_2_1_34_1","unstructured":"Mark Tullsen, Lee Pike, Nathan Collins, and Aaron Tomb. 2018. Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System. In Computer Aided Verification, Hana Chockler and Georg Weissenbacher (Eds.). Springer International Publishing, Cham. 413\u2013429. isbn:978-3-319-96142-2"},{"key":"e_1_3_2_1_35_1","unstructured":"Lev Walkin. 2003\u20132021. asn1c. https:\/\/github.com\/vlm\/asn1c\/"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294105"}],"event":{"name":"CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Boston MA USA","acronym":"CPP '23"},"container-title":["Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575684","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575684","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:38Z","timestamp":1750178738000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575684"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":36,"alternative-id":["10.1145\/3573105.3575684","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575684","relation":{},"subject":[],"published":{"date-parts":[[2023,1,11]]},"assertion":[{"value":"2023-01-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}