{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T11:03:41Z","timestamp":1777806221516,"version":"3.51.4"},"reference-count":70,"publisher":"SAGE Publications","issue":"3","license":[{"start":{"date-parts":[[2022,9,15]],"date-time":"2022-09-15T00:00:00Z","timestamp":1663200000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Journal of Computer Security"],"published-print":{"date-parts":[[2023,5,29]]},"abstract":"<jats:p>Today\u2019s Internet is built on decades-old networking protocols that lack scalability, reliability and security. In response, the networking community has developed path-aware Internet architectures that solve these problems while simultaneously empowering end hosts to exert some control on their packets\u2019 route through the network. In these architectures, autonomous systems authorize forwarding paths in accordance with their routing policies, and protect these paths using cryptographic authenticators. For each packet, the sending end host selects an authorized path and embeds it and its authenticators in the packet header. This allows routers to efficiently determine how to forward the packet. The central security property of the data plane, i.e., of forwarding, is that packets can only travel along authorized paths. This property, which we call path authorization, protects the routing policies of autonomous systems from malicious senders.<\/jats:p>\n                  <jats:p>The fundamental role of packet forwarding in the Internet\u2019s ecosystem and the complexity of the authentication mechanisms employed call for a formal analysis. We develop IsaNet, a parameterized verification framework for data plane protocols in Isabelle\/HOL. We first formulate an abstract model without an attacker for which we prove path authorization. We then refine this model by introducing a Dolev\u2013Yao attacker and by protecting authorized paths using (generic) cryptographic validation fields. This model is parametrized by the path authorization mechanism and assumes five simple verification conditions. We propose novel attacker models and different sets of assumptions on the underlying routing protocol. We validate our framework by instantiating it with nine concrete protocol variants and prove that they each satisfy the verification conditions (and hence path authorization). The invariants needed for the security proof are proven in the parametrized model instead of the instance models. Our framework thus supports low-effort security proofs for data plane protocols. In contrast to what could be achieved with state-of-the-art automated protocol verifiers, our results hold for arbitrary network topologies and sets of authorized paths.<\/jats:p>","DOI":"10.3233\/jcs-220021","type":"journal-article","created":{"date-parts":[[2022,9,16]],"date-time":"2022-09-16T13:57:44Z","timestamp":1663336664000},"page":"217-259","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":1,"title":["IsaNet: A framework for verifying secure data plane protocols"],"prefix":"10.1177","volume":"31","author":[{"given":"Tobias","family":"Klenze","sequence":"first","affiliation":[{"name":"Department of Computer Science, ETH Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Sprenger","sequence":"additional","affiliation":[{"name":"Department of Computer Science, ETH Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Basin","sequence":"additional","affiliation":[{"name":"Department of Computer Science, ETH Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2022,9,15]]},"reference":[{"key":"ref001","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.08.032"},{"key":"ref002","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"ref003","unstructured":"Anapaya Systems, SCION Header Specification, 2022, https:\/\/scion.docs.anapaya.net\/en\/latest\/protocols\/scion-header.html."},{"key":"ref004","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38082-2_2"},{"key":"ref005","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_6"},{"key":"ref006","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.07.004"},{"key":"ref007","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2017.22"},{"key":"ref008","doi-asserted-by":"publisher","DOI":"10.1145\/1282427.1282411"},{"key":"ref009","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9284-7"},{"key":"ref010","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP51992.2021.00042"},{"key":"ref011","doi-asserted-by":"publisher","DOI":"10.1145\/1452044.1452049"},{"key":"ref012","unstructured":"B.\u00a0Bhattacharjee, K.\u00a0Calvert, J.\u00a0Griffioen, N.\u00a0Spring and J.P.G.\u00a0Sterbenz, Postmodern internetwork architecture,\n                      NSF Nets FIND Initiative\n                      (2006)."},{"key":"ref013","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2001.930138"},{"key":"ref014","doi-asserted-by":"publisher","DOI":"10.1145\/3409796"},{"key":"ref015","doi-asserted-by":"crossref","unstructured":"R.\u00a0Bush, Origin Validation Operation Based on the Resource Public Key Infrastructure (RPKI), RFC, 7115, 2014. ISSN 2070-1721.","DOI":"10.17487\/rfc7115"},{"key":"ref016","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(4:19)2015"},{"key":"ref017","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-05288-0"},{"key":"ref018","doi-asserted-by":"publisher","DOI":"10.1145\/2535771.2535787"},{"key":"ref019","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28641-4_3"},{"key":"ref020","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9187-9"},{"key":"ref021","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_12"},{"key":"ref022","doi-asserted-by":"publisher","DOI":"10.1109\/ARES.2006.63"},{"key":"ref023","doi-asserted-by":"publisher","DOI":"10.1145\/1368310.1368324"},{"key":"ref024","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.012"},{"key":"ref025","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17138-4_7"},{"key":"ref026","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00033"},{"key":"ref027","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-191358"},{"key":"ref028","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"ref029","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.002"},{"key":"ref030","doi-asserted-by":"publisher","DOI":"10.1109\/90.974527"},{"key":"ref031","doi-asserted-by":"publisher","DOI":"10.1109\/90.974523"},{"key":"ref032","doi-asserted-by":"crossref","unstructured":"Y.\u00a0Gilad, A.\u00a0Cohen, A.\u00a0Herzberg, M.\u00a0Schapira and H.\u00a0Shulman, Are we there yet? On RPKI\u2019s deployment and security, in: 24th Annual Network and Distributed System Security Symposium, NDSS 2017, San Diego, California, USA, February 26\u2013March 1, 2017, The Internet Society, 2017, https:\/\/www.ndss-symposium.org\/ndss2017\/ndss-2017-programme\/are-we-there-yet-rpkis-deployment-and-security\/.","DOI":"10.14722\/ndss.2017.23123"},{"key":"ref033","doi-asserted-by":"crossref","unstructured":"P.B.\u00a0Godfrey, I.\u00a0Ganichev, S.\u00a0Shenker and I.\u00a0Stoica, Pathlet routing, in: Proceedings of ACM SIGCOMM, 2009.","DOI":"10.1145\/1592568.1592583"},{"key":"ref034","doi-asserted-by":"publisher","DOI":"10.1145\/316188.316231"},{"key":"ref035","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2005.861394"},{"key":"ref036","doi-asserted-by":"crossref","unstructured":"J.\u00a0Karlin, S.\u00a0Forrest and J.\u00a0Rexford, Pretty good BGP: Improving BGP by cautiously adopting routes, in: Proceedings of the IEEE International Conference on Network Protocols, IEEE, 2006.","DOI":"10.1109\/ICNP.2006.320179"},{"key":"ref037","doi-asserted-by":"publisher","DOI":"10.1145\/2342356.2342435"},{"key":"ref038","doi-asserted-by":"publisher","DOI":"10.1109\/49.839934"},{"key":"ref039","doi-asserted-by":"publisher","DOI":"10.1145\/2619239.2626323"},{"key":"ref040","doi-asserted-by":"crossref","unstructured":"T.\u00a0Klenze and C.\u00a0Sprenger, IsaNet: Formalization of a Verification Framework for Secure Data Plane Protocols, Archive of Formal Proofs, 2022, https:\/\/isa-afp.org\/entries\/IsaNet.html, Formal proof development.","DOI":"10.3233\/JCS-220021"},{"key":"ref041","doi-asserted-by":"crossref","unstructured":"T.\u00a0Klenze, C.\u00a0Sprenger and D.\u00a0Basin, Formal verification of secure forwarding protocols, in: 2021 IEEE 34rd Computer Security Foundations Symposium (CSF), IEEE, 2021.","DOI":"10.1109\/CSF51468.2021.00018"},{"key":"ref042","doi-asserted-by":"publisher","DOI":"10.1109\/EuroSP.2017.22"},{"key":"ref043","unstructured":"M.\u00a0Legner, T.\u00a0Klenze, M.\u00a0Wyss, C.\u00a0Sprenger and A.\u00a0Perrig, EPIC: Every packet is checked in the data plane of a path-aware Internet, in: 29th USENIX Security Symposium (USENIX Security), USENIX Association, 2020, pp.\u00a0541\u2013558, https:\/\/www.usenix.org\/conference\/usenixsecurity20\/presentation\/legner. ISBN 978-1-939133-17-5."},{"key":"ref044","doi-asserted-by":"publisher","DOI":"10.17487\/RFC8205"},{"key":"ref045","doi-asserted-by":"publisher","DOI":"10.3929\/ethz-a-010189168"},{"key":"ref046","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1134"},{"key":"ref047","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"ref048","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24638-1_8"},{"key":"ref049","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.26"},{"key":"ref050","doi-asserted-by":"crossref","unstructured":"J.\u00a0Naous, M.\u00a0Walfish, A.\u00a0Nicolosi, D.\u00a0Mazieres, M.\u00a0Miller and A.\u00a0Seehra, Verifying and enforcing network paths with ICING, in: Proceedings of the ACM International Conference on Emerging Networking EXperiments and Technologies (CoNEXT), 2011.","DOI":"10.1145\/2079296.2079326"},{"key":"ref051","doi-asserted-by":"publisher","DOI":"10.1145\/2079296.2079326"},{"key":"ref052","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"ref053","unstructured":"NIST, RPKI Monitor, 2020, https:\/\/rpki-monitor.antd.nist.gov."},{"key":"ref054","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1998-61-205"},{"key":"ref055","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67080-5"},{"key":"ref056","doi-asserted-by":"publisher","DOI":"10.1145\/1030194.1015487"},{"key":"ref057","unstructured":"T.\u00a0Ramananandro, A.\u00a0Delignat-Lavaud, C.\u00a0Fournet, N.\u00a0Swamy, T.\u00a0Chajed, N.\u00a0Kobeissi and J.\u00a0Protzenko, EverParse: Verified secure zero-copy parsers for authenticated message formats, in: 28th USENIX Security Symposium, USENIX Security 2019, Santa Clara, CA, USA, August 14\u201316, 2019, N.\u00a0Heninger and P.\u00a0Traynor, eds, USENIX Association, 2019, pp.\u00a01465\u20131482, https:\/\/www.usenix.org\/conference\/usenixsecurity19\/presentation\/delignat-lavaud."},{"key":"ref058","doi-asserted-by":"crossref","unstructured":"B.\u00a0Rothenberger, D.E.\u00a0Asoni, D.\u00a0Barrera and A.\u00a0Perrig, Internet kill switches demystified, in: Proceedings of the European Workshop on Systems Security (EuroSec), 2017.","DOI":"10.1145\/3065913.3065922"},{"key":"ref059","doi-asserted-by":"publisher","DOI":"10.1145\/3320269.3384743"},{"key":"ref060","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.6"},{"key":"ref061","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.25"},{"key":"ref062","doi-asserted-by":"publisher","DOI":"10.1145\/3428220"},{"key":"ref063","unstructured":"D.\u00a0Unruh, The impossibility of computationally sound XOR,\n                      IACR Cryptol. ePrint Arch.\n                      (2010), 389, http:\/\/eprint.iacr.org\/2010\/389."},{"key":"ref064","unstructured":"T.\u00a0van Deursen and S.\u00a0Radomirovic, Attacks on RFID Protocols,\n                      IACR Cryptology ePrint Archive 2008\n                      (2008), 310."},{"key":"ref065","unstructured":"T.\u00a0Wan, E.\u00a0Kranakis and P.C.\u00a0van Oorschot, Pretty Secure BGP, psBGP, 2005, in: NDSS."},{"issue":"5","key":"ref066","first-page":"47","volume":"33","author":"White R.","year":"2003","journal-title":"Business Communications Review"},{"key":"ref067","doi-asserted-by":"crossref","unstructured":"X.\u00a0Yang, D.\u00a0Clark and A.W.\u00a0Berger, NIRA: A New Inter-Domain Routing Architecture,\n                      IEEE\/ACM Transactions on Networking\n                      (2007).","DOI":"10.1109\/TNET.2007.893888"},{"key":"ref068","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660349"},{"key":"ref069","doi-asserted-by":"crossref","unstructured":"X.\u00a0Zhang, H.C.\u00a0Hsiao, G.\u00a0Hasker, H.\u00a0Chan, A.\u00a0Perrig and D.\u00a0Andersen, SCION: Scalability, control, and isolation on next-generation networks, in: Proceedings of the IEEE Symposium on Security and Privacy, 2011.","DOI":"10.21236\/ADA579930"},{"key":"ref070","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.45"}],"container-title":["Journal of Computer Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-220021","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/full-xml\/10.3233\/JCS-220021","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/JCS-220021","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T20:45:43Z","timestamp":1777495543000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/JCS-220021"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,15]]},"references-count":70,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,5,29]]}},"alternative-id":["10.3233\/JCS-220021"],"URL":"https:\/\/doi.org\/10.3233\/jcs-220021","relation":{},"ISSN":["0926-227X","1875-8924"],"issn-type":[{"value":"0926-227X","type":"print"},{"value":"1875-8924","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,9,15]]}}}