{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T16:00:16Z","timestamp":1783008016451,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T00:00:00Z","timestamp":1693526400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"SNSF for project RHINE","award":["200021_215318"],"award-info":[{"award-number":["200021_215318"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,9,10]]},"DOI":"10.1145\/3603269.3604870","type":"proceedings-article","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T16:16:29Z","timestamp":1693584989000},"page":"932-949","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["A Formal Framework for End-to-End DNS Resolution"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3578-7432","authenticated-orcid":false,"given":"Si","family":"Liu","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1162-2337","authenticated-orcid":false,"given":"Huayi","family":"Duan","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-0085-865X","authenticated-orcid":false,"given":"Lukas","family":"Heimes","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-9825-5578","authenticated-orcid":false,"given":"Marco","family":"Bearzi","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6816-5918","authenticated-orcid":false,"given":"Jodok","family":"Vieli","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2952-939X","authenticated-orcid":false,"given":"David","family":"Basin","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5280-5412","authenticated-orcid":false,"given":"Adrian","family":"Perrig","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"USENIX Security","author":"Afek Yehuda","year":"2020","unstructured":"Yehuda Afek, Anat Bremler-Barr, and Lior Shafir. 2020. NXNSAttack: Recursive DNS Ineffciencies and Vulnerabilities. In USENIX Security 2020. USENIX Association, 631--648. https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/afek"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158668"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.040"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22944-2_28"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC2308"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC4035"},{"key":"e_1_3_2_1_8_1","volume-title":"IMC'10","author":"Benson Theophilus","unstructured":"Theophilus Benson, Aditya Akella, and David A. Maltz. 2010. Network traffic characteristics of data centers in the wild. In IMC'10. ACM, 267--280."},{"key":"e_1_3_2_1_9_1","volume-title":"Survivability: design, formal modeling, and validation of cloud storage systems using Maude. Assured cloud computing","author":"Bobba Rakesh","year":"2018","unstructured":"Rakesh Bobba, Jon Grov, Indranil Gupta, Si Liu, Jos\u00e9 Meseguer, Peter Csaba \u00d6lveczky, and Stephen Skeirik. 2018. Survivability: design, formal modeling, and validation of cloud storage systems using Maude. Assured cloud computing (2018), 10--48."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC7816"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC9156"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC8020"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00470-5_7"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/GLOCOM.2012.6503217"},{"key":"e_1_3_2_1_15_1","volume-title":"Model checking","author":"Clarke Edmund M.","unstructured":"Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron A. Peled, and Helmut Veith. 2018. Model checking, 2nd Edition. MIT Press. https:\/\/mitpress.mit.edu\/books\/model-checking-second-edition","edition":"2"},{"key":"e_1_3_2_1_16_1","volume-title":"Program and Verify Systems in Rewriting Logic. LNCS","volume":"4350","author":"Clavel Manuel","unstructured":"Manuel Clavel, Francisco Dur\u00e1n, Steven Eker, Patrick Lincoln, Narciso Mart\u00ed-Oliet, Jos\u00e9 Meseguer, and Carolyn L. Talcott (Eds.). 2007. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. LNCS, Vol. 4350. Springer."},{"key":"e_1_3_2_1_17_1","unstructured":"PowerDNS contributors. Accessed 2022-06-01. DNS Camel. https:\/\/powerdns.org\/dns-camel\/."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2011.57"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_3_2_1_20_1","volume-title":"Proc. of USENIX Symposium on Networked Systems Design and Implementation (NSDI).","author":"Duan Huayi","year":"2023","unstructured":"Huayi Duan, Rub\u00e9n Fischer, Jie Lou, Si Liu, David Basin, and Adrian Perrig. 2023. RHINE: Robust and High-performance Internet Naming with E2E Authenticity. In Proc. of USENIX Symposium on Networked Systems Design and Implementation (NSDI)."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC2181"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ALLERTON.2018.8635877"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90302-V"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC6604"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387514.3405871"},{"key":"e_1_3_2_1_27_1","volume-title":"SCALE: Automatically Finding RFC Compliance Bugs in DNS Nameservers. In NSDI '22","author":"Reddy Kakarla Siva Kesava","year":"2022","unstructured":"Siva Kesava Reddy Kakarla, Ryan Beckett, Todd Millstein, and George Varghese. 2022. SCALE: Automatically Finding RFC Compliance Bugs in DNS Nameservers. In NSDI '22. USENIX Association, Renton, WA, 307--323. https:\/\/www.usenix.org\/conference\/nsdi22\/presentation\/kakarla"},{"key":"e_1_3_2_1_28_1","volume-title":"CAV'11 (LNCS","volume":"591","author":"Kwiatkowska M.","unstructured":"M. Kwiatkowska, G. Norman, and D. Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-time Systems. In CAV'11 (LNCS, Vol. 6806). Springer, 585--591."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC4592"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC5936"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563299"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2015.05.002"},{"key":"e_1_3_2_1_33_1","unstructured":"Florian Maury. 2015. The \"Indefinitely\" Delegating Name Servers (iDNS) Attack. https:\/\/indico.dns-oarc.net\/event\/21\/contributions\/301\/attachments\/272\/492\/slides.pdf. Accessed 2022-04-30."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/374742.374757"},{"key":"e_1_3_2_1_35_1","volume-title":"Conditional rewriting logic as a unified model of concurrency. Theoretical computer science 96, 1","author":"Meseguer Jos\u00e9","year":"1992","unstructured":"Jos\u00e9 Meseguer. 1992. Conditional rewriting logic as a unified model of concurrency. Theoretical computer science 96, 1 (1992), 73--155."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC1034"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC1035"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3487552.3487824"},{"key":"e_1_3_2_1_39_1","unstructured":"Olivier Poitrey. Accessed 2023-02-07. Consider disabling CNAME scrubbing for forwarded queries #132. https:\/\/github.com\/NLnetLabs\/unbound\/issues\/132."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC6672"},{"key":"e_1_3_2_1_41_1","volume-title":"Amplification Hell: Revisiting Network Protocols for DDoS Abuse. In NDSS 2014","author":"Rossow Christian","year":"2014","unstructured":"Christian Rossow. 2014. Amplification Hell: Revisiting Network Protocols for DDoS Abuse. In NDSS 2014. The Internet Society. https:\/\/www.ndss-symposium.org\/ndss2014\/amplification-hell-revisiting-network-protocols-ddos-abuse"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_26"},{"key":"e_1_3_2_1_43_1","volume-title":"Model-Checking DoS Amplification for VoIP Session Initiation. In ESORICS 2009 (LNCS","volume":"405","author":"Shankesi Ravinder","year":"2009","unstructured":"Ravinder Shankesi, Musab AlTurki, Ralf Sasse, Carl A. Gunter, and Jos\u00e9 Meseguer. 2009. Model-Checking DoS Amplification for VoIP Session Initiation. In ESORICS 2009 (LNCS, Vol. 5789). Springer, 390--405."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16161-2_27"},{"key":"e_1_3_2_1_45_1","unstructured":"Chuck Stearns Vicky Risk Suzanne Goldlust and Cathy Almond. [n.d.]. BIND Best Practices - Recursive. https:\/\/kb.isc.org\/docs\/bind-best-practices-recursive. Accessed 2022-07-19."},{"key":"e_1_3_2_1_46_1","unstructured":"Sam Thielman and Chris Johnston. Accessed 2023-02-07. Major cyber attack disrupts internet service across Europe and US. https:\/\/www.theguardian.com\/technology\/2016\/oct\/21\/ddos-attack-dyn-internet-denial-service."},{"key":"e_1_3_2_1_47_1","unstructured":"Uppaal. 2023. Uppaal 4.0.15. http:\/\/www.uppaal.org."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2019.00033"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.17487\/RFC2136"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFOCOM.2014.6847989"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5856306"},{"key":"e_1_3_2_1_52_1","unstructured":"Zack Whittaker. Accessed 2023-02-07. A DNS outage just took down a large chunk of the internet. https:\/\/techcrunch.com\/2021\/07\/22\/a-dns-outage-just-took-down-a-good-chunk-of-the-internet\/."}],"event":{"name":"ACM SIGCOMM '23: ACM SIGCOMM 2023 Conference","location":"New York NY USA","acronym":"ACM SIGCOMM '23","sponsor":["SIGCOMM ACM Special Interest Group on Data Communication"]},"container-title":["Proceedings of the ACM SIGCOMM 2023 Conference"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3603269.3604870","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3603269.3604870","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:43Z","timestamp":1750178803000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3603269.3604870"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9]]},"references-count":51,"alternative-id":["10.1145\/3603269.3604870","10.1145\/3603269"],"URL":"https:\/\/doi.org\/10.1145\/3603269.3604870","relation":{},"subject":[],"published":{"date-parts":[[2023,9]]},"assertion":[{"value":"2023-09-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}