{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T11:55:46Z","timestamp":1772106946029,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2007,11,2]],"date-time":"2007-11-02T00:00:00Z","timestamp":1193961600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2007,11,2]]},"DOI":"10.1145\/1314436.1314440","type":"proceedings-article","created":{"date-parts":[[2007,11,15]],"date-time":"2007-11-15T14:30:20Z","timestamp":1195137020000},"page":"22-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":35,"title":["Formal correctness of conflict detection for firewalls"],"prefix":"10.1145","author":[{"given":"Venanzio","family":"Capretta","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernard","family":"Stepien","sequence":"additional","affiliation":[{"name":"University of Ottawa, Ottawa, ON, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amy","family":"Felty","sequence":"additional","affiliation":[{"name":"University of Ottawa, Ottawa, ON, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stan","family":"Matwin","sequence":"additional","affiliation":[{"name":"University of Ottawa, Ottawa, ON, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2007,11,2]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2005.854119"},{"key":"e_1_3_2_1_2_1","first-page":"17","volume-title":"IFIP\/IEEE Eighth International Symposium on Integrated Network Management","author":"Ehab","year":"2003","unstructured":"Ehab S. Al-Shaer and Hazem H. Hamed. Firewall policy advisor for anomaly discovery and rule editing . In IFIP\/IEEE Eighth International Symposium on Integrated Network Management , pages 17 -- 30 , 2003 . Ehab S. Al-Shaer and Hazem H. Hamed. Firewall policy advisor for anomaly discovery and rule editing. In IFIP\/IEEE Eighth International Symposium on Integrated Network Management, pages 17--30, 2003."},{"key":"e_1_3_2_1_3_1","first-page":"2605","volume-title":"Discovery of policy anomalies in distributed firewalls","author":"Al-Shaer Ehab S.","year":"2004","unstructured":"Ehab S. Al-Shaer and Hazem H. Hamed . Discovery of policy anomalies in distributed firewalls . In Proceedings of IEEE Infocom , volume 4 , pages 2605 - 2626 , 2004 . Ehab S. Al-Shaer and Hazem H. Hamed. Discovery of policy anomalies in distributed firewalls. In Proceedings of IEEE Infocom, volume 4, pages 2605- 2626, 2004."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/645532.656180"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1035582.1035583"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions","author":"Bertot Yves","year":"2004","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions . Springer , 2004 . Yves Bertot and Pierre Cast\u00e9ran. Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Springer, 2004."},{"key":"e_1_3_2_1_7_1","volume-title":"CISCO IOS in a Nutshell. O'Reilly","author":"Boney James","year":"2001","unstructured":"James Boney . CISCO IOS in a Nutshell. O'Reilly , first edition, 2001 . James Boney. CISCO IOS in a Nutshell. O'Reilly, first edition, 2001."},{"key":"e_1_3_2_1_8_1","volume-title":"IASTED International Conference on Communication, Network, and Information Security","author":"Cuppens F.","year":"2005","unstructured":"F. Cuppens , N. Cuppens-Boulahia , and J. Garc\u00eda-Alfaro . Detection and removal of firewall misconfiguration . In IASTED International Conference on Communication, Network, and Information Security , 2005 . F. Cuppens, N. Cuppens-Boulahia, and J. Garc\u00eda-Alfaro. Detection and removal of firewall misconfiguration. In IASTED International Conference on Communication, Network, and Information Security, 2005."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90058-L"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/365411.365791"},{"key":"e_1_3_2_1_11_1","first-page":"100","volume-title":"6th Nordic Workshop on Secure IT Systems","author":"Eronen Pasi","year":"2001","unstructured":"Pasi Eronen and Jukka Zitting . An expert system for analyzing firewall rules . In 6th Nordic Workshop on Secure IT Systems , pages 100 -- 107 , 2001 . Pasi Eronen and Jukka Zitting. An expert system for analyzing firewall rules. In 6th Nordic Workshop on Secure IT Systems, pages 100--107, 2001."},{"key":"e_1_3_2_1_12_1","series-title":"Lecture Notes in Computer Science","first-page":"166","volume-title":"Mathematical Models for the Semantics of Parallelism","author":"Girard J.-Y.","year":"1986","unstructured":"J.-Y. Girard . Linear logic and parallelism . In Mathematical Models for the Semantics of Parallelism , volume 280 of Lecture Notes in Computer Science , pages 166 -- 182 . Springer-Verlag , 1986 . J.-Y. Girard. Linear logic and parallelism. In Mathematical Models for the Semantics of Parallelism, volume 280 of Lecture Notes in Computer Science, pages 166--182. Springer-Verlag, 1986."},{"key":"e_1_3_2_1_13_1","first-page":"120","volume-title":"IEEE Symposium on Security and Privacy","author":"Guttman Joshua D.","year":"1997","unstructured":"Joshua D. Guttman . Filtering postures : Local enforcement for global policies . In IEEE Symposium on Security and Privacy , pages 120 -- 129 , 1997 . Joshua D. Guttman. Filtering postures: Local enforcement for global policies. In IEEE Symposium on Security and Privacy, pages 120--129, 1997."},{"key":"e_1_3_2_1_14_1","volume-title":"International Journal of Information Security","author":"Joshua","year":"2003","unstructured":"Joshua D. Guttman and Amy L. Herzog. Rigorous automated network security management . International Journal of Information Security , 2003 . To appear. Joshua D. Guttman and Amy L. Herzog. Rigorous automated network security management. International Journal of Information Security, 2003. To appear."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/MCOM.2006.1607877"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/INFCOM.2000.832496"},{"key":"e_1_3_2_1_17_1","first-page":"479","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Howard W. A.","year":"1980","unstructured":"W. A. Howard . The formulae-as-types notion of construction . In J. P. Selding and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism , pages 479 -- 490 . Academic Press , 1980 . W. A. Howard. The formulae-as-types notion of construction. In J. P. Selding and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479--490. Academic Press, 1980."},{"key":"e_1_3_2_1_18_1","volume-title":"Second International Workshop","volume":"2646","author":"Letouzey Pierre","year":"2003","unstructured":"Pierre Letouzey . A new extraction for Coq. In Types for Proofs and Programs , Second International Workshop , volume 2646 of Lecture Notes in Computer Science, pages 200--219. Springer-Verlag , 2003 . Pierre Letouzey. A new extraction for Coq. In Types for Proofs and Programs, Second International Workshop, volume 2646 of Lecture Notes in Computer Science, pages 200--219. Springer-Verlag, 2003."},{"key":"e_1_3_2_1_19_1","series-title":"Lecture Notes in Computer Science","first-page":"196","volume-title":"Data and Applications Security","author":"Liu Alex X.","year":"2005","unstructured":"Alex X. Liu and Mohamed G. Gouda . Complete redundancy detection in firewalls . In Data and Applications Security , volume 3654 of Lecture Notes in Computer Science , pages 196 -- 209 . Springer-Verlag , 2005 . Alex X. Liu and Mohamed G. Gouda. Complete redundancy detection in firewalls. In Data and Applications Security, volume 3654 of Lecture Notes in Computer Science, pages 196--209. Springer-Verlag, 2005."},{"key":"e_1_3_2_1_20_1","volume-title":"Universit\u00e9 du Qu\u00e9bec en Outaouais","author":"Mankai Mahdi","year":"2005","unstructured":"Mahdi Mankai . V\u00e9rification et analyse des politiques de contr\u00f4le d'acc\u00e8s: Application au langage XACML. Master's thesis , Universit\u00e9 du Qu\u00e9bec en Outaouais , January 2005 . Mahdi Mankai. V\u00e9rification et analyse des politiques de contr\u00f4le d'acc\u00e8s: Application au langage XACML. Master's thesis, Universit\u00e9 du Qu\u00e9bec en Outaouais, January 2005."},{"key":"e_1_3_2_1_21_1","first-page":"85","volume-title":"Access control policies: Modeling and validation","author":"Mankai Mahdi","year":"2005","unstructured":"Mahdi Mankai and Luigi Logrippo . Access control policies: Modeling and validation . In K. Adi, D. Amyot, and L. Logrippo, editors, 5th NOTERE Conferenc (Nouvelles Technologies de la R\u00e9partition), pages 85 -- 91 , Gatineau, Canada , 2005 . Mahdi Mankai and Luigi Logrippo. Access control policies: Modeling and validation. In K. Adi, D. Amyot, and L. Logrippo, editors, 5th NOTERE Conferenc (Nouvelles Technologies de la R\u00e9partition), pages 85--91, Gatineau, Canada, 2005."},{"key":"e_1_3_2_1_22_1","volume-title":"Bibliopolis, 1984","author":"Martin-L\u00f6f Per","year":"1980","unstructured":"Per Martin-L\u00f6f . Intuitionistic Type Theory . Bibliopolis, 1984 . Notes by Giovanni Sambin of a series of lectures given in Padua , June 1980 . Per Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/882494.884424"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75285"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/647801.737001"},{"key":"e_1_3_2_1_26_1","volume-title":"June","author":"Sedayao Jeff","year":"2001","unstructured":"Jeff Sedayao . Cisco IOS Access Lists. O'Reilly , June 2001 . Jeff Sedayao. Cisco IOS Access Lists. O'Reilly, June 2001."},{"key":"e_1_3_2_1_27_1","volume-title":"Lectures on the Curry-Howard Isomorphism","author":"S\u00f8rensen Morten Heine B.","year":"2006","unstructured":"Morten Heine B. S\u00f8rensen and P. Urzyczyn . Lectures on the Curry-Howard Isomorphism . Elsevier Science , 2006 . Morten Heine B. S\u00f8rensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier Science, 2006."},{"key":"e_1_3_2_1_28_1","unstructured":"Sun Microsystems. A brief introduction to XACML. http:\/\/-www.-oasis-open-.org\/-committees\/-download.php\/-2713\/-Brief_Introduction_to_XACML.html 2003.  Sun Microsystems. A brief introduction to XACML. http:\/\/-www.-oasis-open-.org\/-committees\/-download.php\/-2713\/-Brief_Introduction_to_XACML.html 2003."},{"key":"e_1_3_2_1_29_1","volume-title":"INRIA","author":"Development Team The Coq","year":"2004","unstructured":"The Coq Development Team . LogiCal Project . The Coq Proof Assistant. Reference Manual. Version 8 . INRIA , 2004 . Available at the web page http:\/\/pauillac.inria.fr\/coq\/coq-eng.html+. The Coq Development Team. LogiCal Project. The Coq Proof Assistant. Reference Manual. Version 8. INRIA, 2004. Available at the web page http:\/\/pauillac.inria.fr\/coq\/coq-eng.html+."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1029133.1029143"},{"key":"e_1_3_2_1_31_1","volume-title":"10th USENIX Security Symposium","author":"Wool Avishai","year":"2001","unstructured":"Avishai Wool . Architecting the Lumeta firewall analyzer . In 10th USENIX Security Symposium , 2001 . Avishai Wool. Architecting the Lumeta firewall analyzer. In 10th USENIX Security Symposium, 2001."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.16"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2007.32"}],"event":{"name":"CCS07: 14th ACM Conference on Computer and Communications Security 2007","location":"Fairfax Virginia USA","acronym":"CCS07","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control","ACM Association for Computing Machinery"]},"container-title":["Proceedings of the 2007 ACM workshop on Formal methods in security engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1314436.1314440","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1314436.1314440","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:56:04Z","timestamp":1750254964000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1314436.1314440"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,11,2]]},"references-count":33,"alternative-id":["10.1145\/1314436.1314440","10.1145\/1314436"],"URL":"https:\/\/doi.org\/10.1145\/1314436.1314440","relation":{},"subject":[],"published":{"date-parts":[[2007,11,2]]},"assertion":[{"value":"2007-11-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}