.. Spécification-formelle-de-firewalls, 111 5.2.1 Vocabulaire et définition

A. Près-la-seconde-guerre-mondiale, informatique restait l'apanage de grandes entreprises qui pouvaient se permettre l'acquisition de quelques ordinateurs. La communication de station à station s'effectuait alors au moyen de supports amovibles. La taille et la complexité des organisations ayant crû significativement Access control based on execution history, Proceedings of the 10th Annual Network and Distributed System Security Symposium, pp.107-121, 2003.

. Abbes, An inference system for detecting firewall filtering rules anomalies, Proceedings of the 2008 ACM symposium on Applied computing , SAC '08, pp.2122-2128, 2008.
DOI : 10.1145/1363686.1364197

URL : https://hal.archives-ouvertes.fr/inria-00329730

. Abdulla, Regular Tree Model Checking, Computer Aided Verification, pp.452-466, 2002.
DOI : 10.1007/3-540-45657-0_47

URL : http://user.it.uu.se/~parosh/publications/trees.ps

. Abiteboul, Foundations of databases, 1995.

. Abrams, Sécurité des systèmes d'information, 1995.

. Adiseshu, Detecting and resolving packet filter conflicts, INFOCOM 2000 -9th annual joint Conference of the IEEE Computer and Communication Societies, pp.1203-1212, 2000.

E. Al-shaer and H. Hamed, Firewall policy advisor for anomaly detection and rule editing, IFIP/IEEE 8th International Symposium on Integrated Network Management IFIP Conference Proceedings, pp.17-30, 2003.
DOI : 10.1109/inm.2003.1194157

E. Al-shaer and H. Hamed, Discovery of policy anomalies in distributed firewalls, IEEE INFOCOM 2004, pp.2605-2616, 2004.
DOI : 10.1109/INFCOM.2004.1354680

. Al-shaer, Conflict classification and analysis of distributed firewall policies, IEEE Journal on Selected Areas in Communications, vol.23, issue.10, pp.2069-2084, 2005.
DOI : 10.1109/JSAC.2005.854119

F. Avolio, Firewalls and Internet security, the second hundred (Internet) years, The Internet Protocol Journal, vol.2, issue.2, pp.24-32, 1999.

N. Baader, F. Baader, and T. Nipkow, Term rewriting and all that, 1998.

. Bachmair, . Dershowitz, L. Bachmair, and N. Dershowitz, Completion for rewriting modulo a congruence, Theoretical Computer Science, vol.67, issue.2-3, pp.173-201, 1989.
DOI : 10.1016/0304-3975(89)90003-0

. Balland, Tom: Piggybacking Rewriting on Java, 18th International Conference on Term Rewriting and Applications -RTA 2007, pp.36-47, 2007.
DOI : 10.1007/978-3-540-73449-9_5

URL : https://hal.archives-ouvertes.fr/inria-00142045

. Bandara, Using Argumentation Logic for Firewall Policy Specification and Analysis, International Workshop on Distributed Systems : Operations and Management Large Scale Management, pp.185-196, 2006.
DOI : 10.1007/s10207-005-0074-z

S. Barker, The next 700 access control models or a unifying meta-model?, Proceedings of the 14th ACM symposium on Access control models and technologies, SACMAT '09, pp.187-196, 2009.
DOI : 10.1145/1542207.1542238

. Barker, Action Control by Term Rewriting, Proceedings of the Third International Workshop on Security and Rewriting Techniques, pp.19-36, 2009.
DOI : 10.1016/j.entcs.2009.02.070

F. Barker, S. Barker, and M. Fernández, Term Rewriting for Access Control, Data and applications security XX, pp.179-193, 2006.
DOI : 10.1145/344287.344301

F. Barker, S. Barker, and M. Fernàndez, Action-status access control as term rewriting, Proceedings of the International Workshop on Security and Rewriting Techniques, pp.3-16, 2007.
DOI : 10.1145/1266840.1266873

S. Barker and P. Stuckey, Flexible access control policy specification with constraint logic programming, ACM Transactions on Information and System Security, vol.6, issue.4, pp.501-546, 2003.
DOI : 10.1145/950191.950194

M. Becker and S. Nanz, A logic for state-modifying authorization policies, ACM Transactions on Information and System Security, vol.13, issue.3, pp.1-28, 2010.
DOI : 10.1145/1805974.1805976

S. Becker and P. Sewell, Cassandra: flexible trust management, applied to electronic health records, Proceedings. 17th IEEE Computer Security Foundations Workshop, 2004., pp.139-154, 2004.
DOI : 10.1109/CSFW.2004.1310738

. Bell, . Lapadula, D. Bell, and L. Lapadula, Secure computer systems : Mathematical foundations and model, 1973.

. Benelbahri, . Bouhoula, A. Benelbahri, and A. Bouhoula, Tuple Based Approach for Anomalies Detection within Firewall Filtering Rules, 2007 IEEE Symposium on Computers and Communications, pp.63-70, 2007.
DOI : 10.1109/ISCC.2007.4381486

. Bertino, An access control model supporting periodicity constraints and temporal reasoning, ACM Transactions on Database Systems, vol.23, issue.3, pp.231-285, 1998.
DOI : 10.1145/293910.293151

URL : http://mercurio.sm.dsi.unimi.it/~samarati/Papers/tods-temporal.ps

. Bertino, A logical framework for reasoning about access control models, ACM Transactions on Information and System Security, vol.6, issue.1, pp.71-127, 2003.
DOI : 10.1145/605434.605437

. Bertolissi, . Fernández, C. Bertolissi, and M. Fernández, A rewriting framework for the composition of access control policies, Proceedings of the 10th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '08, pp.217-225, 2008.
DOI : 10.1145/1389449.1389476

. Bertolissi, . Fernandez, C. Bertolissi, and M. Fernandez, An algebraic-functional framework for distributed access control, 2008 Third International Conference on Risks and Security of Internet and Systems, pp.1-8, 2009.
DOI : 10.1109/CRISIS.2008.4757458

. Bertolissi, . Fernandez, C. Bertolissi, and M. Fernandez, Distributed event-based access control, International Journal of Information and Computer Security, vol.3, issue.3/4, pp.306-320, 2009.
DOI : 10.1504/IJICS.2009.031042

. Bertolissi, Dynamic Event-Based Access Control as Term Rewriting, Data and Applications Security, pp.195-210, 2007.
DOI : 10.1109/2.485845

URL : http://www.dcs.kcl.ac.uk/staff/clara/papers/dbsec07-final.pdf

. Bouajjani, Abstract Regular Tree Model Checking, 7th International Workshop on Verification of Infinite-State Systems, pp.37-48, 1995.
DOI : 10.1016/j.entcs.2005.11.015

URL : https://hal.archives-ouvertes.fr/hal-00156828

A. Bouhoula, Using induction and rewriting to verify and complete parameterized specifications, Theoretical Computer Science, vol.170, issue.1-2, pp.245-276, 1996.
DOI : 10.1016/S0304-3975(96)80708-0

A. Bouhoula, Mécanisation du raisonnement par récurrence . Habilitation à diriger des recherches, 1998.

A. Bouhoula, Simultaneous checking of completeness and ground confluence for algebraic specifications, ACM Transactions on Computational Logic, vol.10, issue.3, p.20, 2009.
DOI : 10.1145/1507244.1507250

. Bourdier and T. Bourdier, Specification, analysis and transformation of security policies via rewriting techniques, Journal of Information Assurance and Security, vol.6, issue.5, pp.357-368, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00525761

. Bourdier and T. Bourdier, Tree Automata Based Semantics of Firewalls, 2011 Conference on Network and Information Systems Security, pp.171-178, 2011.
DOI : 10.1109/SAR-SSI.2011.5931363

URL : https://hal.archives-ouvertes.fr/inria-00460462

T. Bourdier and H. Cirstea, Constrained rewriting in regular theories, INRIA Research Report, 2010.

. Bourdier, . Cirstea, T. Bourdier, and H. Cirstea, Symbolic analysis of network security policies using rewrite systems, Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming, PPDP '11, 2011.
DOI : 10.1145/2003476.2003489

URL : https://hal.archives-ouvertes.fr/inria-00567858

. Bourdier, Extensional and Intensional Strategies, 9th International Workshop on Reduction Strategies in Rewriting and Programming of Electronic Proceedings in Theoretical Computer Science, pp.1-19, 2010.
DOI : 10.1007/978-1-4612-4190-4

URL : https://hal.archives-ouvertes.fr/inria-00494636

. Bourdier, On formal specification and analysis of security policies. Available as an, Grande Region Security and Reliability Day, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00429240

. Bourdier, Rule-based specification and analysis of security policies. Available as 156 BIBLIOGRAPHIE an, 5th International Workshop on Security and Rewriting Techniques, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00552221

. Bourdier, Formal Specification and Validation of Security Policies, Foundations & Practice of Security, 2011.
DOI : 10.3233/JCS-2007-15202

URL : https://hal.archives-ouvertes.fr/inria-00507300

. Bourdier, Analysis of lattice-based access control policies using rewriting systems and tom, Proceedings of the 1st Luxembourg Day on Security and Reliability, pp.33-40, 2009.

. Carrasco, An Implementation of Deterministic Tree Automata Minimization, 12th International Conference on Implementation and Application of Automata, pp.122-129, 2007.
DOI : 10.1007/978-3-540-76336-9_13

. Cirstea, Rule-based Programming in Java For Protocol Verification, 5th International Workshop on Rewriting Logic and Its Applications, pp.209-227, 2005.
DOI : 10.1016/j.entcs.2004.06.022

URL : https://hal.archives-ouvertes.fr/inria-00100025

E. F. Codd, Rewrite based specification of access control policies, 3rd International Workshop on Security and Rewriting Techniques Relational Completeness of Data Base Sublanguages, pp.37-54, 1972.

P. M. Cohn, Universal algebra, volume 6 of Mathematics and its applications, 1965.

H. Comon, Résolution de contraintes dans les algèbres de termes. Habilitation à diriger des recherches, 1992.

H. Comon, Completion of Rewrite Systems with Membership Constraints Part I: Deduction Rules, Journal of Symbolic Computation, vol.25, issue.4, pp.397-419, 1998.
DOI : 10.1006/jsco.1997.0185

H. Comon, Completion of Rewrite Systems with Membership Constraints Part II: Constraint Solving, Journal of Symbolic Computation, vol.25, issue.4, pp.421-453, 1998.
DOI : 10.1006/jsco.1997.0186

H. Comon, Inductionless Induction, Handbook of Automated Reasoning, pp.913-962, 2001.
DOI : 10.1016/B978-044450813-3/50016-3

D. Comon, H. Comon, and C. Delor, Equational Formulas with Membership Constraints, Information and Computation, vol.112, issue.2, pp.167-216, 1994.
DOI : 10.1006/inco.1994.1056

H. Comon and J. Jouannaud, Les termes en logique et en programmation Available at : www.lix.polytechnique.fr/ ~jouannaud/articles/cours-tlpo, 2003.

L. Comon, H. Comon, and P. Lescanne, Equational problems anddisunification, Journal of Symbolic Computation, vol.7, issue.3-4, pp.371-425, 1989.
DOI : 10.1016/S0747-7171(89)80017-3

URL : https://doi.org/10.1016/s0747-7171(89)80017-3

F. Conoboy, B. Conoboy, and E. Fictner, IP Filter Based Firewalls HOWTO, 2002.

. Contejean, A3PAT, an approach for certified automated termination proofs, Proceedings of the ACM SIGPLAN 2010 workshop on Partial evaluation and program manipulation, PEPM '10, pp.63-72, 2010.
DOI : 10.1145/1706356.1706370

URL : https://hal.archives-ouvertes.fr/inria-00535655

B. Courcelle, Resolution of Equations in Algebraic Structures , chapter On recognizable Sets and Tree Automata, 1989.

F. Cuppens, Modélisation formelle de la sécurité des systèmes d'informations. Habilitation à diriger des recherches, 2000.

. Cuppens, Detection and removal of firewall misconfiguration, International Conference on Communication, Network and Information Security, pp.154-162, 2005.

. Cuppens, Detection of network security component misconfiguration by rewriting and correlation, Proceedings of the 5th Conference on Security and Network Architectures joint with the 3rd Conference on Security in Information Systems, 2006.

. Cuppens, A Formal Approach to Specify and Deploy a Network Security Policy, 2nd IFIP TC1 WG1.7 Workshop on Formal Aspects in Security and Trust IFIP Advances in Information and Communication Technology, pp.203-218, 2004.
DOI : 10.1007/0-387-24098-5_15

. Damianou, A survey of policy specification approaches Comparaison de divers formalismes pour la modélisation et le test de politiques de sécurité, Imperial College of Science Technology and MedicinePapers/PolicySurvey.pdf. Projet POTESTAT, 2002.

T. Dauchet, M. Dauchet, S. Tison, and N. Dausque, The theory of ground rewrite systems is decidable, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.242-2481, 1990.
DOI : 10.1109/LICS.1990.113750

. Dershowitz, Decidable matching for convergent systems, 11th International Conference on Automated Deduction, pp.589-602, 1992.
DOI : 10.1007/3-540-55602-8_194

Y. Deswarte and L. Mé, Sécurité des réseaux et systèmes répartis, Hermès Science, 2002.

. Dougherty, Modular Access Control Via Strategic Rewriting, 12th European Symposium On Research In Computer Security, pp.578-593, 2007.
DOI : 10.1007/978-3-540-74835-9_38

URL : https://hal.archives-ouvertes.fr/inria-00185697

. Dougherty, Specifying and Reasoning About Dynamic Access-Control Policies, 3rd International Joint Conference on Automated Reasoning, pp.632-646, 2006.
DOI : 10.1007/11814771_51

URL : http://www.cs.wpi.edu/~kfisler/Pubs/ijcar06.pdf

. Durán, MTT: The Maude Termination Tool (System Description), 4th International Joint Conference on Automated Reasoning, number 5195 in Lecture Notes in Computer Science, pp.313-319, 2008.
DOI : 10.1007/978-3-540-71070-7_27

I. Durand, Autowrite: A Tool for Term Rewrite Systems and Tree Automata, 5th International Workshop on Rule-Based Programming, pp.29-49, 2005.
DOI : 10.1016/j.entcs.2004.11.019

URL : https://hal.archives-ouvertes.fr/hal-00338572

P. Echahed, R. Echahed, and F. Prost, Security policy in a declarative style, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming , PPDP '05, pp.153-163, 2005.
DOI : 10.1145/1069774.1069789

. Edjlali, History-Based Access Control for Mobile Code, Secure Internet Programming, pp.413-431, 1999.
DOI : 10.1007/3-540-48749-2_19

Z. Eronen, P. Eronen, and J. Zitting, An expert system for analyzing firewall rules, Proc. 6th Nordic Worksh. Secure IT Systems, number IMM-TR-2001-14 in Technical report, pp.100-107, 2001.

. Escobar, Narrowing and Rewriting Logic: from Foundations to Applications, 15th Workshop on Func- BIBLIOGRAPHIE tional and (Constraint) Logic Programming, pp.5-33, 2007.
DOI : 10.1016/j.entcs.2007.01.004

K. Falke, S. Falke, and D. Kapur, Inductive Decidability Using Implicit Induction, Logic for Programming, pp.45-59, 2006.
DOI : 10.1007/11916277_4

T. Fernandes, Les politiques de sécurité, 2001.

M. Fernandez, Narrowing based procedures for equational disunification, Applicable Algebra in Engineering, Communication and Computing, vol.65, issue.4, pp.1-26, 1992.
DOI : 10.1016/B978-0-12-115350-2.50017-8

. Feuillade, Reachability Analysis over Term Rewriting Systems, Journal of Automated Reasoning, vol.37, issue.1?2, pp.3-4341, 2004.
DOI : 10.1016/B978-0-08-012975-4.50028-X

URL : https://hal.archives-ouvertes.fr/inria-00071609

. Fruhwirth, Logic programs as types for logic programs, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.300-309, 1991.
DOI : 10.1109/LICS.1991.151654

. Fuller, . Li, V. Fuller, and T. Li, Classless Inter-Domain Routing (CIDR) : The Internet Address Assignment and Aggregation Plan. The Internet Society, 2006.
DOI : 10.17487/rfc4632

. Gécseg, . Steinby, F. Gécseg, and M. Steinby, Handbook of formal languages, 1997.

. Gelfond, M. Lifschitz-]-gelfond, and V. Lifschitz, Action languages, Electronic Transactions on Artificial Intelligence, vol.2, pp.193-210, 1998.

K. Genet, T. Genet, and F. Klay, Rewriting for Cryptographic Protocol Verification, 17th International Conference on Automated Deduction, pp.271-290, 2000.
DOI : 10.1007/10721959_21

URL : https://hal.archives-ouvertes.fr/inria-00072731

V. Gligor, Characteristics of role-based access control, Proceedings of the first ACM Workshop on Role-based access control , RBAC '95, 1995.
DOI : 10.1145/270152.270169

J. Goubault-larrecq-]-goubault-larrecq, Deciding by resolution, Information Processing Letters, vol.95, issue.3, pp.401-408, 2005.
DOI : 10.1016/j.ipl.2005.04.007

L. Gouda and A. Liu, Firewall design: consistency, completeness, and compactness, 24th International Conference on Distributed Computing Systems, 2004. Proceedings., pp.320-327, 2004.
DOI : 10.1109/ICDCS.2004.1281597

D. Graham, G. Graham, and P. Denning, Protection, Proceedings of the November 16-18, 1971, fall joint computer conference on, AFIPS '71 (Fall), pp.417-429, 1972.
DOI : 10.1145/1478873.1478928

. Greco, COMPLEX: an object-oriented logic programming system, IEEE Transactions on Knowledge and Data Engineering, vol.4, issue.4, pp.344-359, 1992.
DOI : 10.1109/69.149930

. Habib, Formal definition and comparison of access control models, Journal of Information Assurance and Security, vol.4, issue.4, pp.372-381, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01195856

W. Halpern, J. Halpern, and V. Weissman, Using First-Order Logic to Reason about Policies, ACM Transactions on Information and System Security, vol.11, issue.4, pp.1-41, 2008.
DOI : 10.1145/1380564.1380569

. Hamdi, A Domain Specific Language for Securing Distributed Systems, 2007 Second International Conference on Systems and Networks Communications (ICSNC 2007), 2007.
DOI : 10.1109/ICSNC.2007.2

URL : https://hal.archives-ouvertes.fr/hal-00306235

A. Hamed, H. Shaer, and E. , Taxonomy of conflicts in network security policies, IEEE Communications Magazine, vol.44, issue.3, pp.134-141, 2006.
DOI : 10.1109/MCOM.2006.1607877

. Hamed, Modeling and Verification of IPSec and VPN Security Policies, 13TH IEEE International Conference on Network Protocols (ICNP'05), pp.259-278, 2005.
DOI : 10.1109/ICNP.2005.25

. Hardin, Access control and rewrite systems, Proceedings of the 1st International Workshop on Security and Rewriting Techniques, 2006.
URL : https://hal.archives-ouvertes.fr/hal-01352004

S. Hazelhurst, Algorithms for analysing firewall and router access lists, 2000.

R. Heintze, N. Heintze, and J. Riecke, The SLam calculus, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '98, pp.365-377, 1998.
DOI : 10.1145/268946.268976

M. Hirokawa, N. Hirokawa, and A. Middeldorp, Tyrolean termination tool: Techniques and features, Information and Computation, vol.205, issue.4, pp.474-511, 2005.
DOI : 10.1016/j.ic.2006.08.010

H. Huet, G. Huet, and J. Hullot, Proofs by induction in equational theories with constructors, Journal of Computer and System Sciences, vol.25, issue.2, pp.239-266, 1982.
DOI : 10.1016/0022-0000(82)90006-X

URL : https://hal.archives-ouvertes.fr/inria-00076533

F. Jacquemard and F. Jacquemard, Automates d'arbres et réécriture de termes Decidable approximations of term rewriting systems, 7th International Conference on Rewriting Techniques and BIBLIOGRAPHIE Applications, volume 1103 of Lecture Notes in Computer Science, pp.362-376, 1996.

. Jajodia, Flexible support for multiple access control policies, ACM Transactions on Database Systems, vol.26, issue.2, pp.214-260, 2001.
DOI : 10.1145/383891.383894

. Jajodia, A logical language for expressing authorizations, Proceedings. 1997 IEEE Symposium on Security and Privacy (Cat. No.97CB36097), pp.31-42, 1997.
DOI : 10.1109/SECPRI.1997.601312

. Jouannaud, . Kirchner, J. Jouannaud, and C. Kirchner, Solving equations in abstract algebras : a rule-based survey of unification, Computational Logic : Essays in Honor of Alan Robinson, pp.257-321, 1991.

. Jouannaud, . Kirchner, J. Jouannaud, and H. Kirchner, Completion of a Set of Rules Modulo a Set of Equations, SIAM Journal on Computing, vol.15, issue.4, pp.1155-1194, 1986.
DOI : 10.1137/0215084

. Kalam, Organization based access control, Proceedings POLICY 2003. IEEE 4th International Workshop on Policies for Distributed Systems and Networks, pp.120-131, 2003.
DOI : 10.1109/POLICY.2003.1206966

URL : https://hal.archives-ouvertes.fr/hal-01483818

. Kamara, Analysis of vulnerabilities in Internet firewalls, Computers & Security, vol.22, issue.3, pp.214-232, 2003.
DOI : 10.1016/S0167-4048(03)00310-9

. Kirchner, Strategic computations and deductions, Reasoning in Simple Type Theory ? Festschrift in Honor of Peter B. Andrews on his 70th Birthday, pp.339-364, 2008.

. Kirchner, . Kirchner, C. Kirchner, and H. Kirchner, Constrained equational reasoning, Proceedings of the ACM-SIGSAM 1989 international symposium on Symbolic and algebraic computation , ISSAC '89, pp.382-389, 1989.
DOI : 10.1145/74540.74585

. Kirchner, . Kirchner, C. Kirchner, and H. Kirchner, Rewriting Solving Proving. Preliminary version of a book Available at, 2006.

. Kirchner, Deduction with symbolic contraints. Revue d'intelligence artificielle, Hermès Science, vol.4, issue.3, pp.9-52, 1990.

. Kirchner, Analysis of Rewrite-Based Access Control Policies, 3rd International Workshop on Security and Rewriting Techniques 5th Princeton Conf. on Information Sciences and Systems, pp.55-75, 1971.
DOI : 10.1016/j.entcs.2009.02.072

URL : https://hal.archives-ouvertes.fr/inria-00335088

O. Lengál, An efficient tree automata library, 2010.

R. Limet, S. Limet, and P. Réty, Solving disequations modulo some class of rewrite systems, 9th International Conference on Rewriting Techniques and Applications, pp.121-135, 1998.
DOI : 10.1007/BFb0052365

URL : https://hal.archives-ouvertes.fr/hal-00809565

A. Liu, Formal Verification of Firewall Policies, 2008 IEEE International Conference on Communications, pp.1494-1498, 2008.
DOI : 10.1109/ICC.2008.289

G. Liu, A. Liu, and M. Gouda, Complete Redundancy Detection in Firewalls, Data and Applications Security XIX, pp.193-206, 2005.
DOI : 10.1006/jagm.1996.0063

. Liu, Firewall Queries, 8th International Conference on Principles of Distributed Systems, pp.197-212, 2005.
DOI : 10.1007/11516798_15

G. Liu, A. X. Liu, and M. G. Gouda, Firewall Policy Queries, IEEE Transactions on Parallel and Distributed Systems, vol.20, issue.6, pp.766-777, 2009.
DOI : 10.1109/TPDS.2008.263

URL : http://www.cse.msu.edu/~alexliu/publications/FirewallQueries/FirewallQueryTPDS.pdf

P. Marchand, Mathématiques Discrètes -Automates, langages , logique et décidabilité, 2003.

K. Marmorstein, R. Marmorstein, and P. Kearns, An open source solution for testing NAT'd and nested iptables firewalls, 19th Conference on Systems Administration, pp.103-112, 2005.

. Masson, An access control model based testing approach for smart card applications : Results of the POSE project PDDL ? the Planning Domain Definition Language, Journal of Information Assurance and Security, vol.5, issue.1, pp.335-351, 1998.

J. Mclean, The algebra of security, Proceedings. 1988 IEEE Symposium on Security and Privacy, pp.2-7, 1988.
DOI : 10.1109/SECPRI.1988.8092

D. Mé, L. Mé, and Y. Deswarte, Sécurité des systèmes d'information. Hermès Science, 2006.

J. Monin, Introduction aux méthodes formelles, Hermès Science, 2000.

C. Morisset, Sémantique des systèmes de contrôle d'accès ? Définition d'un cadre sémantique pour la spécification, l'implantation et la comparaison de modèles de contrôle d'accès, 2007.

. Nelson, The margrave tool for firewall analysis, International Conference on Large Installation System Administration, pp.1-8, 2010.

. Nieslon, Normalizable horn clauses, strongly recognizable relations and spi, Static Analysis Symposium, pp.20-35, 2002.

N. Peltier, Constructing infinite models represented by tree automata, Annals of Mathematics and Artificial Intelligence, vol.2, issue.4, pp.65-85, 2009.
DOI : 10.1007/3-540-61511-3_96

URL : https://hal.archives-ouvertes.fr/hal-00940621

C. Rocha, The maude invariant analyzer tool, 2011.

M. Rocha, C. Rocha, and J. Meseguer, Proving Safety Properties of Rewrite Theories, 4th Conference on Algebra and Coalgebra in Computer Science, pp.314-328, 2011.
DOI : 10.1007/978-3-642-22944-2_22

R. Russell, Linux 2.4 packet filtering howto Available at, 2002.

S. Russo, L'information, source de pouvoir, ??conomie rurale, vol.69, issue.1, pp.3-10, 1966.
DOI : 10.3406/ecoru.1966.1943

URL : http://www.persee.fr/docAsPDF/ecoru_0013-0559_1966_num_69_1_1943.pdf

V. Rusu, Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications, Tests and Proofs, pp.135-150, 2010.
DOI : 10.1007/978-3-642-13977-2_12

URL : https://hal.archives-ouvertes.fr/inria-00527864

D. Samarati, . Vimercati, P. Samarati, and S. De-vimercati, Access Control: Policies, Models, and Mechanisms, Foundations of Security Analysis and Design, pp.137-196, 2001.
DOI : 10.1007/3-540-45608-2_3

R. Sandhu, Lattice-based access control models, Computer, vol.26, issue.11, pp.9-19, 1993.
DOI : 10.1109/2.241422

URL : http://www.list.gmu.edu/journals/computer/pdf_ver/i93lbacm.pdf

S. Sandhu, R. Sandhu, and P. Samarati, Access control: principle and practice, IEEE Communications Magazine, vol.32, issue.9, pp.40-48, 1994.
DOI : 10.1109/35.312842

O. Santana-de and A. Santana-de-oliveira, Rewriting-based access control policies, Proceedings of the 1st International Workshop on Security and Rewriting Techniques, pp.59-72, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00112340

O. Santana-de and A. Santana-de-oliveira, Réécriture et modularité pour les politiques de sécurité, 2008.

O. Santana-de, Weaving rewrite-based access control policies, ACM Workshop on Formal methods in security engineering, pp.71-80, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00185710

. Sasturkar, Policy analysis for administrative role based access control, Proceedings of the 19th IEEE workshop on Computer Security Foundations, pp.124-138, 2006.

F. Schneider, Enforceable security policies, ACM Transactions on Information and System Security, vol.3, issue.1, pp.30-50, 2000.
DOI : 10.1145/353323.353382

URL : http://www.cs.cornell.edu/fbs/publications/99-1759.pdf

. Souayeh, Automatic Validation of Firewall Configurations using SMT Solvers, Journal of Information Assurance and Security, vol.5, issue.1, pp.561-568, 2010.

A. Sperschneider, V. Sperschneider, and G. Antoniou, Logic : A Fundation for Computer Science. International Computer Science Series, 1991.

H. Srisuresh, P. Srisuresh, and M. Holdrege, IP Network Address Translator (NAT) Terminology and Considerations. The Internet Society, 1999.
DOI : 10.17487/rfc2663

URL : https://www.rfc-editor.org/rfc/pdfrfc/rfc2663.txt.pdf

S. Sterling, L. Sterling, and E. Shapiro, The Art of Prolog, IEEE Expert, vol.2, issue.2, 1994.
DOI : 10.1109/MEX.1987.4307074

D. Sterne, On the buzzword 'security policy', Proceedings. 1991 IEEE Computer Society Symposium on Research in Security and Privacy, pp.219-231, 1991.
DOI : 10.1109/RISP.1991.130789

S. Stratulat, Automatic ???Descente Infinie??? Induction Reasoning, TABLEAUX, pp.262-276, 2005.
DOI : 10.1007/11554554_20

W. Thatcher, J. W. Thatcher, and J. B. Wright, Generalized finite automata theory with an application to a decision problem of second-order logic, Theory of Computing Systems, pp.57-81, 1968.
DOI : 10.1145/320924.320931

S. Tison, Tree Automata and Term Rewrite Systems, 11th International Conference on Rewriting Techniques and Applications, pp.27-30, 2000.
DOI : 10.1007/10721975_2

URL : http://www.inf.u-szeged.hu/tanszekek/szamitastudomanyalapjai/RRVagvolgy2003.ps

J. Ullman, Principles of database and knowledge-base systems, 1988.

C. Uribe, T. Uribe, and S. Cheung, Automatic analysis of firewall and network intrusion detection system configurations, Journal of Computer Security, vol.15, issue.6, pp.691-715, 2007.
DOI : 10.3233/JCS-2007-15605

J. Wijesekera, D. Wijesekera, and S. Jajodia, Policy algebras for access control -the predicate case Authorization in distributed systems : A new approach, 9th ACM Conference on Computer and Communications Security, pp.171-180107, 1993.

. Yuan, Fireman : A toolkit for firewall modeling and analysis, IEEE Symposium on Security and Privacy (S&P), 2006.