{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T18:08:36Z","timestamp":1763748516060,"version":"3.45.0"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,11,12]],"date-time":"2021-11-12T00:00:00Z","timestamp":1636675200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"National Science Foundation","award":["CNS-2006556"],"award-info":[{"award-number":["CNS-2006556"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,11,12]]},"DOI":"10.1145\/3460120.3484793","type":"proceedings-article","created":{"date-parts":[[2021,11,13]],"date-time":"2021-11-13T12:05:34Z","timestamp":1636805134000},"page":"1388-1404","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["On Re-engineering the X.509 PKI with Executable Specification for Better Implementation Guarantees"],"prefix":"10.1145","author":[{"given":"Joyanta","family":"Debnath","sequence":"first","affiliation":[{"name":"The University of Iowa, Iowa City, IA, USA"}]},{"given":"Sze Yiu","family":"Chau","sequence":"additional","affiliation":[{"name":"The Chinese University of Hong Kong, Hong Kong, Hong Kong"}]},{"given":"Omar","family":"Chowdhury","sequence":"additional","affiliation":[{"name":"The University of Iowa, Iowa City, IA, USA"}]}],"member":"320","published-online":{"date-parts":[[2021,11,13]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"2014. stringprep: Implements the \"StringPrep\" algorithm. https:\/\/hackage.haskell.org\/package\/stringprep."},{"key":"e_1_3_2_2_2_1","unstructured":"2020. SSL certificate chain resolver. https:\/\/github.com\/zakjan\/cert-chain-resolver."},{"key":"e_1_3_2_2_3_1","unstructured":"2021. GnuTLS. https:\/\/www.gnutls.org\/."},{"key":"e_1_3_2_2_4_1","unstructured":"2021. mbedTLS. https:\/\/tls.mbed.org\/."},{"key":"e_1_3_2_2_5_1","unstructured":"2021. OpenSSL. https:\/\/www.openssl.org\/."},{"key":"e_1_3_2_2_6_1","unstructured":"2021. parsec 3.8. https:\/\/pypi.org\/project\/parsec\/."},{"volume-title":"Understanding PKI: concepts, standards, and deployment considerations","author":"Adams Carlisle","key":"e_1_3_2_2_7_1","unstructured":"Carlisle Adams and Steve Lloyd. 2003. Understanding PKI: concepts, standards, and deployment considerations. Addison-Wesley Professional."},{"key":"e_1_3_2_2_8_1","volume-title":"Prague, Czechoslovakia, June 4--13","author":"Alblas Henk","year":"1991","unstructured":"Henk Alblas and Borivoj Melichar. 1991. Attribute Grammars, Applications and Systems: International Summer School SAGA, Prague, Czechoslovakia, June 4--13, 1991. Proceedings. Vol. 545. Springer Science & Business Media."},{"key":"e_1_3_2_2_9_1","volume-title":"Nail: A Practical Tool for Parsing and Generating Data Formats. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI '14)","author":"Bangert Julian","year":"2014","unstructured":"Julian Bangert and Nickolai Zeldovich. 2014. Nail: A Practical Tool for Parsing and Generating Data Formats. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI '14). 615--628."},{"key":"e_1_3_2_2_10_1","volume-title":"Systematic parsing of X. 509: eradicating security issues with a parse tree. Journal of Computer Security","author":"Barenghi Alessandro","year":"2018","unstructured":"Alessandro Barenghi, Nicholas Mainardi, and Gerardo Pelosi. 2018. Systematic parsing of X. 509: eradicating security issues with a parse tree. Journal of Computer Security (2018), 817--849."},{"key":"e_1_3_2_2_11_1","volume-title":"SMT Workshop.","author":"Barrett Clark","year":"2010","unstructured":"Clark Barrett, Aaron Stump, Cesare Tinelli, et al. 2010. The smt-lib standard: Version 2.0. In SMT Workshop."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","unstructured":"Clark W. Barrett Christopher L. Conway Morgan Deters Liana Hadarean Dejan Jovanovic Tim King Andrew Reynolds and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification (Lecture Notes in Computer Science). 171--177. https:\/\/doi.org\/10.1007\/978--3--642--22110--1_14","DOI":"10.1007\/978--3--642--22110--1_14"},{"key":"e_1_3_2_2_13_1","volume-title":"Vale: Verifying High-Performance Cryptographic Assembly Code. In 26th USENIX Security Symposium (SEC'17)","author":"Bond Barry","year":"2017","unstructured":"Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code. In 26th USENIX Security Symposium (SEC'17). 917--934."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.15"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.40"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2019.23430"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786835"},{"key":"e_1_3_2_2_18_1","volume-title":"Int. Res.","author":"Cimatti Alessandro","year":"2011","unstructured":"Alessandro Cimatti, Alberto Griggio, and Roberto Sebastiani. 2011. Computing Small Unsatisfiable Cores in Satisfiability modulo Theories. J. Artif. Int. Res. (2011), 701--728."},{"key":"e_1_3_2_2_19_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. Technical Report. http:\/\/www.rfc-editor.org\/rfc\/rfc5280.txt","DOI":"10.17487\/rfc5280"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978--3--642--33826--7_16"},{"key":"e_1_3_2_2_21_1","volume-title":"Sze Yiu Chau, and Omar Chowdhury","author":"Debnath Joyanta","year":"2021","unstructured":"Joyanta Debnath, Sze Yiu Chau, and Omar Chowdhury. 2021. Source Code for CERES. https:\/\/github.com\/joyantaDebnath\/CERES."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341686"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813703"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2504730.2504755"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1667053.1667059"},{"key":"e_1_3_2_2_26_1","volume-title":"SMT Workshop.","author":"Gario Marco","year":"2015","unstructured":"Marco Gario and Andrea Micheli. 2015. PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms. In SMT Workshop."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"crossref","unstructured":"P. Hoffman and M. Blanchet. 2002. Preparation of Internationalized Strings (?string-prep\"). Technical Report. https:\/\/tools.ietf .org\/rfc\/rfc3454.txt","DOI":"10.17487\/rfc3454"},{"key":"e_1_3_2_2_28_1","volume-title":"Canonical Encoding Rules (CER) and Distinguished Encoding Rules (DER).","author":"ITU-T.","year":"2021","unstructured":"ITU-T. 2021. X.690 : Information technology - ASN.1 encoding rules: Specification of Basic Encoding Rules (BER), Canonical Encoding Rules (CER) and Distinguished Encoding Rules (DER). (2021)."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706347"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Burt Kaliski. 1998. PKCS# 1: RSA encryption version 1.5. Technical Report. https:\/\/tools.ietf .org\/rfc\/rfc2313.txt","DOI":"10.17487\/rfc2313"},{"key":"e_1_3_2_2_31_1","volume-title":"24th USENIX Security Symposium (SEC'15)","author":"Mehnert Hannes","year":"2015","unstructured":"Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell. 2015. Not-Quite-So-Broken TLS: Lessons in Re-Engineering a Security Protocol Specification and Implementation. In 24th USENIX Security Symposium (SEC'15). 223--238."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Dan Kaminsky Meredith L. Patterson and Len Sassaman. 2010. PKI Layer Cake: New Collision Attacks against the Global X.509 Infrastructure. In Financial Cryptography and Data Security. 289--303.","DOI":"10.1007\/978-3-642-14577-3_22"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"crossref","unstructured":"Donald E. Knuth. 1968. Semantics of Context-Free Languages. In In Mathematical Systems Theory. 127--145.","DOI":"10.1007\/BF01692511"},{"key":"e_1_3_2_2_34_1","unstructured":"Ulrich K\u00fchn A. Pyshkin E. Tews and R. Weinmann. 2008. Variants of Bleichenbacher's Low-Exponent Attack on PKCS#1 RSA Signatures. (2008)."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00015"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190231"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1670412.1670414"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1177080.1177119"},{"key":"e_1_3_2_2_39_1","unstructured":"Terence Parr. 2013. The definitive ANTLR 4 reference. Pragmatic Bookshelf."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00114"},{"key":"e_1_3_2_2_41_1","volume-title":"EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In 28th USENIX Security Symposium (SEC'19)","author":"Ramananandro Tahina","year":"2019","unstructured":"Tahina Ramananandro, Antoine Delignat-Lavaud, Cedric Fournet, Nikhil Swamy, Tej Chajed, Nadim Kobeissi, and Jonathan Protzenko. 2019. EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats. In 28th USENIX Security Symposium (SEC'19). 1465--1482."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.46"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2991079.2991100"},{"volume-title":"30th USENIX Security Symposium (USENIX Security 21)","author":"Tao Zhe","key":"e_1_3_2_2_44_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--1107. https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/tao"},{"key":"e_1_3_2_2_45_1","unstructured":"Sebastian Andreas Ullrich. 2016. Simple Verification of Rust Programs via Functional Purification."},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428261"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385985"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"crossref","unstructured":"K Zeilenga. 2006. Lightweight Directory Access Protocol (LDAP): Internationalized String Preparation. Technical Report. https:\/\/www.rfc-editor.org\/rfc\/rfc4518.txt","DOI":"10.17487\/rfc4518"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"event":{"name":"CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Virtual Event Republic of Korea","acronym":"CCS '21"},"container-title":["Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460120.3484793","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460120.3484793","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460120.3484793","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T20:53:24Z","timestamp":1763499204000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460120.3484793"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,12]]},"references-count":49,"alternative-id":["10.1145\/3460120.3484793","10.1145\/3460120"],"URL":"https:\/\/doi.org\/10.1145\/3460120.3484793","relation":{},"subject":[],"published":{"date-parts":[[2021,11,12]]},"assertion":[{"value":"2021-11-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}