{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T10:17:55Z","timestamp":1775470675185,"version":"3.50.1"},"reference-count":87,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2018,1,3]],"date-time":"2018-01-03T00:00:00Z","timestamp":1514937600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Comission","doi-asserted-by":"crossref","award":["653884"],"award-info":[{"award-number":["653884"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]},{"name":"BMBF","award":["16BP12304"],"award-info":[{"award-number":["16BP12304"]}]},{"name":"BMBF","award":["16KIS0472"],"award-info":[{"award-number":["16KIS0472"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10817-017-9445-1","type":"journal-article","created":{"date-parts":[[2018,1,3]],"date-time":"2018-01-03T10:42:12Z","timestamp":1514976132000},"page":"191-242","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Verified iptables Firewall Analysis and Verification"],"prefix":"10.1007","volume":"61","author":[{"given":"Cornelius","family":"Diekmann","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8442-856X","authenticated-orcid":false,"given":"Lars","family":"Hupel","sequence":"additional","affiliation":[]},{"given":"Julius","family":"Michaelis","sequence":"additional","affiliation":[]},{"given":"Maximilian","family":"Haslbeck","sequence":"additional","affiliation":[]},{"given":"Georg","family":"Carle","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,1,3]]},"reference":[{"key":"9445_CR1","doi-asserted-by":"publisher","unstructured":"Al-Shaer, E., Alsaleh, M.: ConfigChecker: a tool for comprehensive security configuration analytics. In: Configuration Analytics and Automation (SAFECONFIG), pp. 1\u20132. IEEE (2011). https:\/\/doi.org\/10.1109\/SafeConfig.2011.6111667","DOI":"10.1109\/SafeConfig.2011.6111667"},{"key":"9445_CR2","doi-asserted-by":"publisher","unstructured":"Al-Shaer, E., Hamed, H.: Discovery of policy anomalies in distributed firewalls. In: Annual Joint Conference of the IEEE Computer and Communications Societies (INFOCOM), vol. 4, pp. 2605\u20132616 (2004). https:\/\/doi.org\/10.1109\/INFCOM.2004.1354680","DOI":"10.1109\/INFCOM.2004.1354680"},{"key":"9445_CR3","unstructured":"Analyzed firewall rulesets (raw data). https:\/\/github.com\/diekmann\/net-network. Accompanying material"},{"key":"9445_CR4","doi-asserted-by":"publisher","unstructured":"Anderson, C.J., Foster, N., Guha, A., Jeannin, J.B., Kozen, D., Schlesinger, C., Walker, D.: NetKAT: semantic foundations for networks. In: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201914, pp. 113\u2013126. ACM, San Diego (2014). https:\/\/doi.org\/10.1145\/2535838.2535862","DOI":"10.1145\/2535838.2535862"},{"key":"9445_CR5","doi-asserted-by":"crossref","unstructured":"Baker, F., Savola, P.: Ingress filtering for multihomed networks. RFC 3704 (Best Current Practice) (2004)","DOI":"10.17487\/rfc3704"},{"key":"9445_CR6","doi-asserted-by":"publisher","unstructured":"Bartal, Y., Mayer, A., Nissim, K., Wool, A.: Firmato: a novel firewall management toolkit. In: IEEE Symposium on Security and Privacy, pp. 17\u201331. IEEE (1999). https:\/\/doi.org\/10.1109\/SECPRI.1999.766714","DOI":"10.1109\/SECPRI.1999.766714"},{"issue":"2","key":"9445_CR7","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1145\/2602204.2602211","volume":"44","author":"G Bianchi","year":"2014","unstructured":"Bianchi, G., Bonola, M., Capone, A., Cascone, C.: OpenState: programming platform-independent stateful openflow applications inside the switch. ACM SIGCOMM Comput. Commun. Rev. 44(2), 44\u201351 (2014). https:\/\/doi.org\/10.1145\/2602204.2602211","journal-title":"ACM SIGCOMM Comput. Commun. Rev."},{"key":"9445_CR8","doi-asserted-by":"publisher","unstructured":"Brucker, A.D., Br\u00fcgger, L., Kearney, P., Wolff, B.: Verified firewall policy transformations for test case generation. In: 3rd International Conference on Software Testing, Verification and Validation, pp. 345\u2013354. IEEE (2010). https:\/\/doi.org\/10.1109\/ICST.2010.50","DOI":"10.1109\/ICST.2010.50"},{"key":"9445_CR9","doi-asserted-by":"crossref","unstructured":"Brucker, A.D., Br\u00fcgger, L., Wolff, B.: Model-based firewall conformance testing. In: Suzuki, K., Higashino, T., Ulrich, A., Hasegawa, T. (eds.) Testing of Software and Communicating Systems, pp. 103\u2013118. Springer (2008)","DOI":"10.1007\/978-3-540-68524-1_9"},{"key":"9445_CR10","doi-asserted-by":"publisher","unstructured":"Brucker, A.D., Br\u00fcgger, L., Wolff, B.: Formal firewall conformance testing: an application of test and proof techniques. Softw. Test. Verif. Reliab. (STVR) 25(1), 34\u201371 (2015). https:\/\/doi.org\/10.1002\/stvr.1544, https:\/\/www.brucker.ch\/bibliography\/abstract\/brucker.ea-formal-fw-testing-2014","DOI":"10.1002\/stvr.1544"},{"key":"9445_CR11","unstructured":"Brucker, A.D., Br\u00fcgger, L., Wolff, B.: Formal network models and their application to firewall policies. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/UPF_Firewall.shtml. Formal proof development"},{"key":"9445_CR12","doi-asserted-by":"publisher","unstructured":"Byma, S., Tarafdar, N., Xu, T., Bannazadeh, H., Leon-Garcia, A., Chow, P.: Expanding OpenFlow capabilities with virtualized reconfigurable hardware. In: ACM\/SIGDA International Symposium on Field-Programmable Gate Arrays, FPGA \u201915, pp. 94\u201397. ACM, Monterey (2015). https:\/\/doi.org\/10.1145\/2684746.2689086","DOI":"10.1145\/2684746.2689086"},{"key":"9445_CR13","doi-asserted-by":"publisher","unstructured":"Capretta, V., Stepien, B., Felty, A., Matwin, S.: Formal correctness of conflict detection for firewalls. In: Workshop on Formal Methods in Security Engineering, pp. 22\u201330. ACM (2007). https:\/\/doi.org\/10.1145\/1314436.1314440","DOI":"10.1145\/1314436.1314440"},{"key":"9445_CR14","unstructured":"Cisco IOS firewall\u2014configuring IP access lists. Document ID: 23602 (2007). http:\/\/www.cisco.com\/c\/en\/us\/support\/docs\/security\/ios-firewall\/23602-confaccesslists.html"},{"key":"9445_CR15","doi-asserted-by":"crossref","unstructured":"Cotton, M., Vegoda, L., Bonica, R., Haberman, B.: Special-purpose IP address registries. RFC 6890 (Best Current Practice) (2013)","DOI":"10.17487\/rfc6890"},{"key":"9445_CR16","unstructured":"CrazyCat: iptables multiport and negation. Server Fault Question (2016). http:\/\/serverfault.com\/questions\/793631\/iptables-multiport-and-negation\/"},{"key":"9445_CR17","unstructured":"Deering, S., Hinden, R.: Internet protocol, version 6 (IPv6) specification. RFC 2460 (Draft Standard) (1998). Updated by RFCs 5095, 5722, 5871, 6437, 6564, 6935, 6946, 7045, 7112"},{"key":"9445_CR18","unstructured":"Diekmann, C.: Naming network interfaces. In: PoC||GTFO: Pastor Laphroaig Races the Runtime Relinker and Other True Tales of Cleverness and Craft, vol. 16, no. 08, pp. 45\u201346 (2017)"},{"key":"9445_CR19","unstructured":"Diekmann, C., Hupel, L.: Iptables semantics. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/Iptables_Semantics.shtml. Formal proof development"},{"key":"9445_CR20","doi-asserted-by":"publisher","unstructured":"Diekmann, C., Hupel, L., Carle, G.: Directed security policies: a stateful network implementation. In: Electronic Proceedings in Theoretical Computer Science on Engineering Safety and Security Systems (ESSS), vol. 150, pp. 20\u201334. Open Publishing Association, Singapore (2014). https:\/\/doi.org\/10.4204\/EPTCS.150.3","DOI":"10.4204\/EPTCS.150.3"},{"key":"9445_CR21","doi-asserted-by":"publisher","unstructured":"Diekmann, C., Korsten, A., Carle, G.: Demonstrating topoS: theorem-prover-based synthesis of secure network configurations. In: 11th International Conference on Network and Service Management (CNSM), pp. 366\u2013371. Barcelona (2015). https:\/\/doi.org\/10.1109\/CNSM.2015.7367384","DOI":"10.1109\/CNSM.2015.7367384"},{"key":"9445_CR22","unstructured":"Diekmann, C., Michaelis, J., Haslbeck, M.: Simple firewall. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/Simple_Firewall.shtml. Formal proof development"},{"key":"9445_CR23","doi-asserted-by":"crossref","unstructured":"Diekmann, C., Michaelis, J., Haslbeck, M., Carle, G.: Verified iptables firewall analysis. In: IFIP Networking 2016. Vienna (2016)","DOI":"10.1109\/IFIPNetworking.2016.7497196"},{"key":"9445_CR24","unstructured":"Diekmann, C., Michaelis, J., Hupel, L.: IP addresses. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/IP_Addresses.shtml. Formal proof development"},{"key":"9445_CR25","doi-asserted-by":"publisher","unstructured":"Diekmann, C., Posselt, S.A., Niedermayer, H., Kinkelin, H., Hanka, O., Carle, G.: Verifying security policies using host attributes. In: Formal Techniques for Distributed Objects, Components, and Systems: 34th IFIP WG 6.1 International Conference, FORTE, pp. 133\u2013148. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-662-43613-4_9","DOI":"10.1007\/978-3-662-43613-4_9"},{"key":"9445_CR26","doi-asserted-by":"publisher","unstructured":"Diekmann, C., Schwaighofer, L., Carle, G.: Certifying spoofing-protection of firewalls. In: 11th International Conference on Network and Service Management (CNSM), pp. 168\u2013172. Barcelona (2015). https:\/\/doi.org\/10.1109\/CNSM.2015.7367354","DOI":"10.1109\/CNSM.2015.7367354"},{"key":"9445_CR27","unstructured":"diekmann\/Iptables_Semantics: Issue #113\u2014Port numbers belong to a specific protocol. github (2016). https:\/\/github.com\/diekmann\/Iptables_Semantics\/issues\/113"},{"key":"9445_CR28","unstructured":"Eastep, T.M.: iptables made ease\u2014shorewall (2014). http:\/\/shorewall.net\/"},{"key":"9445_CR29","unstructured":"Engelhardt, J.: Towards the perfect ruleset (2011). http:\/\/inai.de\/documents\/Perfect_Ruleset.pdf"},{"key":"9445_CR30","doi-asserted-by":"publisher","unstructured":"Foster, N., Kozen, D., Milano, M., Silva, A., Thompson, L.: A coalgebraic decision procedure for NetKAT. In: 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201915, pp. 343\u2013355. ACM, Mumbai (2015). https:\/\/doi.org\/10.1145\/2676726.2677011","DOI":"10.1145\/2676726.2677011"},{"key":"9445_CR31","doi-asserted-by":"crossref","unstructured":"Fuller, V., Li, T.: Classless inter-domain routing (CIDR): the internet address assignment and aggregation plan. RFC 4632 (Best Current Practice) (2006)","DOI":"10.17487\/rfc4632"},{"key":"9445_CR32","unstructured":"Gartenmeister, M.: Iptables vs. Cisco PIX (2005). http:\/\/lists.netfilter.org\/pipermail\/netfilter\/2005-April\/059714.html"},{"key":"9445_CR33","doi-asserted-by":"publisher","unstructured":"Guha, A., Reitblatt, M., Foster, N.: Machine-verified network controllers. In: 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201913, pp. 483\u2013494. ACM, Seattle (2013). https:\/\/doi.org\/10.1145\/2462156.2462178","DOI":"10.1145\/2462156.2462178"},{"key":"9445_CR34","unstructured":"Haftmann, F., Bulwahn, L.: Code generation from Isabelle\/HOL theories (2016)"},{"key":"9445_CR35","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming, pp. 103\u2013117. Springer (2010)","DOI":"10.1007\/978-3-642-12251-4_9"},{"issue":"3","key":"9445_CR36","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1109\/MCOM.2006.1607877","volume":"44","author":"H Hamed","year":"2006","unstructured":"Hamed, H., Al-Shaer, E.: Taxonomy of conflicts in network security policies. IEEE Commun. Mag. 44(3), 134\u2013141 (2006). https:\/\/doi.org\/10.1109\/MCOM.2006.1607877","journal-title":"IEEE Commun. Mag."},{"key":"9445_CR37","unstructured":"Hewlett Packard: IP firewall configuration guide (2005). ftp:\/\/ftp.hp.com\/pub\/networking\/software\/ProCurve-SR-IP-Firewall-Config-Guide.pdf"},{"key":"9445_CR38","unstructured":"IPTables Example Config. http:\/\/networking.ringofsaturn.com\/Unix\/iptables.php. Retrieved Sept 2014"},{"key":"9445_CR39","doi-asserted-by":"publisher","unstructured":"Jeffrey, A., Samak, T.: Model checking firewall policy configurations. In: Policies for Distributed Systems and Networks, pp. 60\u201367. IEEE (2009). https:\/\/doi.org\/10.1109\/POLICY.2009.32","DOI":"10.1109\/POLICY.2009.32"},{"key":"9445_CR40","doi-asserted-by":"crossref","unstructured":"Kawamura, S., Kawashima, M.: A recommendation for IPv6 address text representation. RFC 5952 (Proposed Standard) (2010)","DOI":"10.17487\/rfc5952"},{"key":"9445_CR41","unstructured":"Kazemian, P., Varghese, G., McKeown, N.: Header space analysis: static checking for networks. In: 9th USENIX Symposium on Networked Systems Design and Implementation (NSDI), NSDI\u201912, pp. 113\u2013126. USENIX Association, San Jose (2012)"},{"key":"9445_CR42","unstructured":"Kleene, S.C.: Introduction to Metamathematics. Bibliotheca Mathematica. North-Holland, Amsterdam (1952)"},{"key":"9445_CR43","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-39634-2_9","volume-title":"Automatic Data Refinement","author":"P Lammich","year":"2013","unstructured":"Lammich, P.: Automatic Data Refinement, pp. 84\u201399. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_9"},{"key":"9445_CR44","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-32347-8_12","volume-title":"Applying Data Refinement for Monadic Programs to Hopcroft\u2019s Algorithm","author":"P Lammich","year":"2012","unstructured":"Lammich, P., Tuerk, T.: Applying Data Refinement for Monadic Programs to Hopcroft\u2019s Algorithm, pp. 166\u2013182. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-32347-8_12"},{"key":"9445_CR45","unstructured":"Leblond, E.: Why you will love nftables (2014). https:\/\/home.regit.org\/2014\/01\/why-you-will-love-nftables\/"},{"key":"9445_CR46","unstructured":"Linux Kernel Sources: Linux\/include\/linux\/netfilter\/x_tables.h. Kernel 4.6. http:\/\/lxr.free-electrons.com\/source\/include\/linux\/netfilter\/x_tables.h?v=4.6#L343"},{"key":"9445_CR47","doi-asserted-by":"publisher","unstructured":"Mansmann, F., G\u00f6bel, T., Cheswick, W.: Visual analysis of complex firewall configurations. In: 9th International Symposium on Visualization for Cyber Security, VizSec \u201912, pp. 1\u20138. ACM (2012). https:\/\/doi.org\/10.1145\/2379690.2379691","DOI":"10.1145\/2379690.2379691"},{"key":"9445_CR48","unstructured":"Marmorstein, R.M., Kearns, P.: A tool for automated iptables firewall analysis. In: USENIX Annual Technical Conference, FREENIX Track, pp. 71\u201381. USENIX Association (2005)"},{"key":"9445_CR49","unstructured":"Marmorstein, R.M., Kearns, P., et\u00a0al.: Firewall analysis with policy-based host classification. In: 20th USENIX Large Installation System Administration Conference (LISA), vol.\u00a06. USENIX Association, Washington (2006)"},{"key":"9445_CR50","unstructured":"Michaelis, J., Diekmann, C.: LOFT\u2014verified migration of Linux firewalls to SDN. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/LOFT.shtml. Formal proof development"},{"key":"9445_CR51","unstructured":"Michaelis, J., Diekmann, C.: Routing. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/Routing.shtml. Formal proof development"},{"key":"9445_CR52","doi-asserted-by":"crossref","unstructured":"Monsanto, C., Foster, N., Harrison, R., Walker, D.: A compiler and run-time system for network programming languages. In: 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201912, pp. 217\u2013230. ACM (2012)","DOI":"10.1145\/2103656.2103685"},{"key":"9445_CR53","unstructured":"Moy, E., Gildea, S., Dickey, T.: XTerm control sequences (2016). http:\/\/invisible-island.net\/xterm\/ctlseqs\/ctlseqs.html"},{"key":"9445_CR54","unstructured":"Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: 24th USENIX Large Installation System Administration Conference (LISA). USENIX Association, San Jose (2010)"},{"key":"9445_CR55","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-319-19249-9_25","volume-title":"Static Differential Program Analysis for Software-Defined Networks","author":"T Nelson","year":"2015","unstructured":"Nelson, T., Ferguson, A.D., Krishnamurthi, S.: Static Differential Program Analysis for Software-Defined Networks, pp. 395\u2013413. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-19249-9_25"},{"key":"9445_CR56","unstructured":"Nelson, T., Ferguson, A.D., Scheer, M.J., Krishnamurthi, S.: Tierless programming and reasoning for software-defined networks. In: 11th USENIX Symposium on Networked Systems Design and Implementation (NSDI), NSDI\u201914, pp. 519\u2013531. USENIX Association, Seattle (2014)"},{"key":"9445_CR57","doi-asserted-by":"publisher","unstructured":"Nelson, T., Ferguson, A.D., Yu, D., Fonseca, R., Krishnamurthi, S.: Exodus: toward automatic migration of enterprise network configurations to SDNs. In: 1st ACM SIGCOMM Symposium on Software Defined Networking Research, no.\u00a013 in SOSR \u201915, pp. 13:1\u201313:7. ACM, Santa Clara (2015). https:\/\/doi.org\/10.1145\/2774993.2774997","DOI":"10.1145\/2774993.2774997"},{"key":"9445_CR58","doi-asserted-by":"publisher","unstructured":"Nelson, T., Guha, A., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: A balance of power: expressive, analyzable controller programming. In: Second ACM SIGCOMM Workshop on Hot Topics in Software Defined Networking, HotSDN \u201913, pp. 79\u201384. ACM, Hong Kong (2013). https:\/\/doi.org\/10.1145\/2491185.2491201","DOI":"10.1145\/2491185.2491201"},{"key":"9445_CR59","unstructured":"NetCitadel, Inc.: FirewallBuilder. http:\/\/www.fwbuilder.org. Ver. 5.1"},{"key":"9445_CR60","unstructured":"netfilter coreteam: libxtables\/xtables.c. https:\/\/git.netfilter.org\/iptables\/tree\/libxtables\/xtables.c?h=v1.6.0#n518"},{"key":"9445_CR61","unstructured":"Nicira, Inc.: Nicira extensions. openvswitch\/ovs repository (2016). https:\/\/github.com\/openvswitch\/ovs\/blob\/master\/include\/openflow\/nicira-ext.h. Revision fb8f22c186b89cd36059c37908f940a1aa5e1569"},{"key":"9445_CR62","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-319-10542-0"},{"key":"9445_CR63","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: a proof assistant for higher-order logic. In: LNCS, vol. 2283. Springer (2002, last updated 2016). http:\/\/isabelle.in.tum.de\/","DOI":"10.1007\/3-540-45949-9"},{"key":"9445_CR64","unstructured":"Nygren, A., Pfaff, B., Lantz, B., Heller, B., Barker, C., Beckmann, C., Cohn, D., Malek, D., Talayco, D., Erickson, D., McDysan, D., Ward, D., Crabbe, E., Schneider, F., Gibb, G., Appenzeller, G., Tourrilhes, J., Tonsing, J., Pettit, J., Yap, K., Poutievski, L., Dunbar, L., Vicisano, L., Casado, M., Takahashi, M., Kobayashi, M., Orr, M., Yadav, N., McKeown, N., dHeureuse, N., Balland, P., Madabushi, R., Ramanathan, R., Price, R., Sherwood, R., Das, S., Gandham, S., Curtis, S., Natarajan, S., Mizrahi, T., Yabe, T., Ding, W., Yiakoumis, Y., Moses, Y., Kis, Z.L.: OpenFlow switch specification v1.5.1 (2015). https:\/\/www.opennetworking.org\/images\/stories\/downloads\/sdn-resources\/onf-specifications\/openflow\/openflow-switch-v1.5.1.pdf.ONFTS-025"},{"key":"9445_CR65","unstructured":"Petrucci, L., Bonelli, N., Bonola, M., Procissi, G., Cascone, C., Sanvito, D., Pontarelli, S., Bianchi, G., Bifulco, R.: Towards a stateful forwarding abstraction to implement scalable network functions in software and hardware. ArXiv e-prints (2016)"},{"key":"9445_CR66","unstructured":"PF: the OpenBSD packet filter. http:\/\/www.openbsd.org\/faq\/pf\/"},{"key":"9445_CR67","unstructured":"Pfaff, B., Heller, B., Talayco, D., Erickson, D., Gibb, G., Appenzeller, G., Tourrilhes, J., Pettit, J., Yap, K., Casado, M., Kobayashi, M., McKeown, N., Balland, P., Price, R., Sherwood, R., Yiakoumis, Y.: OpenFlow switch specification v1.0.0 (2009). http:\/\/archive.openflow.org\/documents\/openflow-spec-v1.0.0.pdf"},{"key":"9445_CR68","doi-asserted-by":"crossref","unstructured":"Postel, J.: Internet protocol. RFC 791 (INTERNET STANDARD) (1981). Updated by RFCs 1349, 2474, 6864","DOI":"10.17487\/rfc0791"},{"key":"9445_CR69","doi-asserted-by":"publisher","unstructured":"Pozo, S., Ceballos, R., Gasca, R.M.: CSP-based firewall rule set diagnosis using security policies. In: 2nd International Conference on Availability, Reliability and Security (ARES), pp. 723\u2013729. IEEE, Los Alamitos (2007). https:\/\/doi.org\/10.1109\/ARES.2007.63","DOI":"10.1109\/ARES.2007.63"},{"issue":"5","key":"9445_CR70","doi-asserted-by":"crossref","first-page":"894","DOI":"10.1016\/j.infsof.2008.05.001","volume":"51","author":"S Pozo","year":"2009","unstructured":"Pozo, S., Ceballos, R., Gasca, R.M.: Model-based development of firewall rule sets: diagnosing model inconsistencies. Inf. Softw. Technol. 51(5), 894\u2013915 (2009)","journal-title":"Inf. Softw. Technol."},{"key":"9445_CR71","unstructured":"Renard, B.: cisco-acl-to-iptables (2013). http:\/\/git.zionetrix.net\/?a=summary&p=cisco-acl-to-iptables. Retrieved Sept 2014"},{"key":"9445_CR72","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Assigned numbers: RFC 1700 is replaced by an on-line database. RFC 3232 (Informational) (2002)","DOI":"10.17487\/rfc3232"},{"key":"9445_CR73","doi-asserted-by":"crossref","unstructured":"Reynolds, J., Postel, J.: Assigned numbers. RFC 1700 (Historic) (1994). Obsoleted by RFC 3232","DOI":"10.17487\/rfc1700"},{"issue":"4","key":"9445_CR74","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1145\/2377677.2377680","volume":"42","author":"J Sherry","year":"2012","unstructured":"Sherry, J., Hasan, S., Scott, C., Krishnamurthy, A., Ratnasamy, S., Sekar, V.: Making middleboxes someone elses problem: network processing as a cloud service. ACM SIGCOMM Comput. Commun. Rev. 42(4), 13\u201324 (2012)","journal-title":"ACM SIGCOMM Comput. Commun. Rev."},{"key":"9445_CR75","doi-asserted-by":"crossref","unstructured":"Sluizer, S., Postel, J.: Mail transfer protocol. RFC 780 (1981). Obsoleted by RFC 788","DOI":"10.17487\/rfc0780"},{"key":"9445_CR76","doi-asserted-by":"publisher","unstructured":"Smolka, S., Eliopoulos, S.A., Foster, N., Guha, A.: A fast compiler for NetKAT. In: International Conference on Functional Programming (ICFP), pp. 328\u2013341. ACM (2015). https:\/\/doi.org\/10.1145\/2784731.2784761","DOI":"10.1145\/2784731.2784761"},{"key":"9445_CR77","unstructured":"Tantau, T., Feuersaenger, C.: The TikZ and pgf packages (2016). Pgfversion 3.0.1a"},{"key":"9445_CR78","unstructured":"The netfilter.org project: netfilter\/iptables project. http:\/\/www.netfilter.org\/"},{"key":"9445_CR79","unstructured":"The netfilter.org project: netfilter\/nftables project. http:\/\/www.netfilter.org\/"},{"key":"9445_CR80","unstructured":"Tongaonkar, A., Inamdar, N., Sekar, R.: Inferring higher level policies from firewall rules. In: 21st USENIX Large Installation System Administration Conference (LISA), vol.\u00a07, pp. 1\u201310. USENIX Association, Dallas (2007)"},{"key":"9445_CR81","unstructured":"Verizon Business RISK Team, United States Secret Service: 2010 Data Breach Investigations Report (2010). http:\/\/www.verizonenterprise.com\/resources\/reports\/rp_2010-DBIR-combined-reports_en_xg.pdf"},{"issue":"6","key":"9445_CR82","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1109\/MC.2004.2","volume":"37","author":"A Wool","year":"2004","unstructured":"Wool, A.: A quantitative study of firewall configuration errors. IEEE Comput. 37(6), 62\u201367 (2004)","journal-title":"IEEE Comput."},{"issue":"6","key":"9445_CR83","doi-asserted-by":"crossref","first-page":"459","DOI":"10.1016\/j.cose.2004.02.003","volume":"23","author":"A Wool","year":"2004","unstructured":"Wool, A.: The use and usability of direction-based filtering in firewalls. Comput. Secur. 23(6), 459\u2013468 (2004)","journal-title":"Comput. Secur."},{"issue":"4","key":"9445_CR84","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1109\/MIC.2010.29","volume":"14","author":"A Wool","year":"2010","unstructured":"Wool, A.: Trends in firewall configuration errors: measuring the holes in swiss cheese. IEEE Internet Comput. 14(4), 58\u201365 (2010). https:\/\/doi.org\/10.1109\/MIC.2010.29","journal-title":"IEEE Internet Comput."},{"key":"9445_CR85","unstructured":"Yuan, L., Chen, H., Mai, J., Chuah, C.N., Su, Z., Mohapatra, P.: FIREMAN: a toolkit for firewall modeling and analysis. In: IEEE Symposium on Security and Privacy, pp. 199\u2013213 (2006)"},{"key":"9445_CR86","doi-asserted-by":"publisher","unstructured":"Zhang, B., Al-Shaer, E., Jagadeesan, R., Riely, J., Pitcher, C.: Specifications of a high-level conflict-free firewall policy language for multi-domain networks. In: 12th ACM Symposium on Access Control Models and Technologies, SACMAT\u201907, pp. 185\u2013194. ACM (2007). https:\/\/doi.org\/10.1145\/1266840.1266871","DOI":"10.1145\/1266840.1266871"},{"key":"9445_CR87","doi-asserted-by":"publisher","unstructured":"Zhang, S., Mahmoud, A., Malik, S., Narain, S.: Verification and synthesis of firewalls using SAT and QBF. In: Network Protocols (ICNP), pp. 1\u20136 (2012). https:\/\/doi.org\/10.1109\/ICNP.2012.6459944","DOI":"10.1109\/ICNP.2012.6459944"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9445-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9445-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9445-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T19:57:41Z","timestamp":1570564661000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9445-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,3]]},"references-count":87,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["9445"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9445-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,1,3]]}}}