Using access control policy rules with deny effects (i.e., negative authorization) can be preferred to using complemented conditions in the rules as they are often easier to comprehend in the context of large policies. However, the two constructs have different impacts on the expressiveness of a rule-based access control model. We investigate whether policies expressible using complemented conditions can be expressed using deny rules instead. The answer to this question is not always affirmative. In this paper, we propose a practical approach to address this problem for a given policy. In particular, we develop theoretical results that allow us to pose the problem as a set of queries to an SAT solver. Our experimental results using an off-the-shelf SAT solver demonstrate the feasibility of our approach and offer insights into its performance based on access control policies from multiple domains.

Recent access control models such as attribute-based access control and relationship-based access control allow flexible expression of authorization policies using the concepts of rules and conditional expressions. The independent nature of policy rules from each other and the amount of flexibility that they enjoy (e.g., the type of conditional expressions they support and whether they can permit or deny matching requests) make those policies quite expressive. But how expressive are they? Do we need to enable all possible flexibilities in a rule-based model to achieve the maximum possible expressiveness? Answering such questions is essential in making informed decisions when designing new models or choosing existing models for implementation. In this paper, we propose an approach towards answering those questions by developing a novel theory for capturing the semantics of rule-based policies depending on their support of different constructs such as flexibility of conditional expressions, rule modalities, and conflict resolution. Our formal policy semantics model enjoys an intuitive design that can capture the semantics of various rule-based policies. We show the well-formedness properties of such semantics and how they can be used to analyze the expressive power of a number of rule-based models.

Recent advances in the automated analysis of cryptographic protocols have aroused new interest in the practical application of unification modulo theories, especially theories that describe the algebraic properties of cryptosystems. However, this application requires unification algorithms that can be easily implemented and easily extended to combinations of different theories of interest. In practice this has meant that most tools use a version of a technique known as variant unification. This requires, among other things, that the theory be decomposable into a set of axioms B and a set of rewrite rules R such that R has the finite variant property with respect to B. Most theories that arise in cryptographic protocols have decompositions suitable for variant unification, but there is one major exception: the theory that describes encryption that is homomorphic over an Abelian group.

A number of new cryptographic protocols are being designed to secure applications such as video-conferencing and electronic voting. Many of them rely upon cryptographic functions with complex algebraic properties that must be accounted for in order to be correctly analyzed by automated tools. Maude-NPA is a cryptographic protocol analysis tool based on narrowing and typed equational unification which takes into account these algebraic properties. It has already been used to analyze protocols involving bounded associativity, modular exponentiation, and exclusive-or. All of the above can be handled by the same general variant-based equational unification technique. However, there are important properties, in particular homomorphic encryption, that cannot be handled by variant-based unification in the same way. In these cases the best available approach is to implement specialized unification algorithms and combine them within a modular framework. In this paper we describe how we apply this approach within Maude-NPA, with respect to encryption homomorphic over a free operator. We also describe the use of Maude-NPA to analyze several protocols using such an encryption operation. To the best of our knowledge, this is the first implementation of homomorphic encryption of any sort in a tool for verifying the security of a protocol in the presence of active attackers.

We address the insecurity problem for cryptographic protocols, for an active intruder and a bounded number of sessions. The protocol steps are modeled as rigid Horn clauses, and the intruder abilities as an equational theory. The problem of active intrusion -- such as whether a secret term can be derived, possibly via interaction with the honest participants of the protocol -- is then formulated as a Cap Unification problem. Cap Unification is an extension of Equational Unification: look for a cap to be placed on a given set of terms, so as to unify it with a given term modulo the equational theory. We give a decision procedure for Cap Unification, when the intruder capabilities are modeled as homomorphic encryption theory. Our procedure can be employed in a simple manner to detect attacks exploiting some properties of block ciphers.

replace me

A term rewrite system (TRS) terminates if its rules are contained in a reduction ordering >. In order to deal with any set of equations, including inherently non-terminating ones (like commutativity), TRS have been generalised to ordered TRS (E, >), where equations of E are applied in whatever direction agrees with >. The confluence of terminating TRS is well-known to be decidable, but for ordered TRS the decidability of confluence has been open. Here we show that the confluence of ordered TRS is decidable if ordering constraints for > can be solved in an adequate way, which holds in particular for the class of LPO orderings. For sets E of constrained equations, confluence is shown to be undecidable. Finally, ground reducibility is proved undecidable for ordered TRS.

Abstract Cartesian closed categories (CCCs) have played and continue to play an important role in the study of the semantics of programming languages. An axiomatization of the isomorphisms which hold in all Cartesian closed categories discovered independently by Soloviev and Bruce, Di Cosmo and Longo leads to seven equalities. We show that the unification problem for this theory is undecidable, thus settling an open question. We also show that an important subcase, namely unification modulo thelinear isomorphisms, is NP-complete. Furthermore, the problem of matching in CCCs is NP-complete when the subject term is irreducible. CCC-matching and unification form the basis for an elegant and practical solution to the problem of retrieving functions from a library indexed by types investigated by Rittri. It also has potential applications to the problem of polymorphic type inference and polymorphic higher-order unification, which in turn is relevant to theorem proving and logic programming.

We consider the problem of solving linear equations over various semirings. In particular, solving of linear equations over polynomial rings with the additional restriction that the solutions must have only non-negative coefficients is shown to be undecidable. Applications to undecidability proofs of several unification problems are illustrated, one of which, unification modulo one associative-commutative function and one endomorphism, has been a long-standing open problem. The problem of solving multiset constraints is also shown to be undecidable.

We show that elementary ACI10 unification is in P, even with constant restrictions. As a corollary, we prove that validity of quantified Horn formulae can be tested in O(n 2 ) time. Solvability of elementary disunification problems modulo ACI10 is shown to be NP-hard.

The matrix tree theorem for directed graphs is generalized to cover all minors of nodal formulations of all linear circuits with voltage controlled current sources. The term signs are readily evaluated from linking-cycle-arborescence: configurations in a common generalization of Maxwell's and Coates' rules. All minors are treated with the same formalism. The formulation introduces half-resistors which are transposed unistors. Their use for intuitive description of circuit operation based on approximation, nodal impedance conditions and backward error analysis is described for BJT amplifiers and the switch model for digital MOS circuits.

An axiomatization of the isomorphisms that hold in all Cartesian closed categories (CCCs), discovered independently by S.V. Soloviev (1983) and by K.B. Bruce and G. Longo (1985), leads to seven equalities. It is shown that the unification problem for this theory is undecidable, thus setting an open question. It is also shown that an important subcase, namely unification modulo the linear isomorphisms, is NP-complete. Furthermore, the problem of matching in CCCs is NP-complete when the subject term is irreducible. CCC-matching and unification form the basis for an elegant and practical solution to the problem of retrieving functions from a library indexed by types investigated by M. Rittri (1990, 1991). It also has potential applications to the problem of polymorphic higher-order unification, which in turn is relevant to theorem proving, logic programming, and type reconstruction in higher-order languages.>

It is shown that unifiability is decidable in theories presented by a set of ground equations with several associative-communicative symbols (ground AC theories). This result applies, for instance, to finitely presented commutative semigroups, and it extends the authors' previous work (P. Narendran and M. Rusinwithch, 1991) where they gave an algorithm for solving the uniform word problem in ground AC theories.>

In this paper, it is shown that there is an algorithm that, given by finite set E of ground equations, produces a reduced canonical rewriting system R equivalent to E in polynomial time. This algorithm based on congruence closure performs simplification steps guided by a total simplification ordering on ground terms, and it runs in time O(n 3 ) .

An algorithm for computing a complete set of unifiers for two terms involving associative-commutative function symbols is presented. It is based on a nondeterministic algorithm given by the authors in 1986 to show the NP-completeness of associative-commutative unifiability. The algorithm is easy to understand, and its termination can be easily established. Its complexity is easily analyzed and shown to be doubly exponential in the size of the input terms. The analysis also shows that there is a double-exponential upper bound on the size of a complete set of unifiers of two input terms. Since there is a family of simple associative-commutative unification problems which have complete sets of unifiers whose size is doubly exponential, the algorithm is optimal in its order of complexity in this sense.>

In this paper, it is shown that the method of matings due to Andrews and Bibel can be extended to (first-order) languages with equality. A decidable version of E -unification called rigid E-unification is introduced, and it is shown that the method of equational matings remains complete when used in conjunction with rigid E -unification. Checking that a family of mated sets is an equational mating is equivalent to the following restricted kind of E -unification. Problem Given E → ={E i | 1≤i≤n} a family of n finite sets of equations and S={〈u i ,v i 〉 |1≤i≤n} a set of n pairs of terms, is there a substitution θ such that, treating each set θ(E i ) as a set of ground equations (i.e., holding the variables in θ(E i ) “rigid”), θ(u i ), and θ(v i ) are provably equal from θ(E i ) for i=1,...,n? Equivalently, is there a substitution θ such that θ(u i ) and θ(v i ) can be shown congruent from θ(E i ) by the congruence closure method for i=1,...,n? A substitution θ solving the above problem is called a rigid E → -unifier of S , and a pair 〈E → ,S〉 such that S has some rigid E → -unifier is called an equational premating. It is shown that deciding whether a pair 〈 E → ,S〉is an equational premating is an NP-complete problem.

Rigid E-unification is a restricted kind of unification modulo equational theories, or E-unification, that arises naturally in extending Andrew's theorem proving method of matings to first-order languages with equality. This extension was first presented by J. H. Gallier, S. Raatz, and W. Snyder, who conjectured that rigid E-unification is decidable. In this paper, it is shown that rigid E-unification is NP-complete and that finite complete sets of rigid E-unifiers always exist. As a consequence, deciding whether a family of mated sets is an equational mating is an NP-complete problem. Some implications of this result regarding the complexity of theorem proving in first-order logic with equality are also discussed.

Rigid E-unification is a restricted kind of unification modulo equational theories, or E-unification, that arises naturally in extending P. Andrews' (1981) theorem-proving method of mating to first-order languages with equality. It is shown that rigid E-unification is NP-complete and that finite complete sets of rigid E-unifiers always exist. As a consequence, deciding whether a family of mated sets is an equational mating is an NP-complete problem. Some implications of this result regarding the complexity of theorem proving in first-order logic with equality are discussed.>

Since about 1971, much research has been done on Thue systems that have properties that ensure viable and efficient computation. The strongest of these is the Church-Rosser property, which states that two equivalent strings can each be brought to a unique canonical form by a sequence of length-reducing rules. In this paper three ways in which formal languages can be defined by Thue systems with this property are studied, and some general results about the three families of languages so determined are studied.

The use of formal geometric reasoning is proposed to analyze algorithms for machine vision and robotics. This paper develops the basis for this approach and illustrates the method with several examples taken from perspective scene analysis. The application of recent developments in algebraic deduction methods is described.

The Knuth-Bendix completion procedure for term rewriting systems in many cases provides a decision procedure for equational theories and has been found to have many applications in various areas. We discuss the application of the Knuth-Bendix procedure to Thue systems. We use the notion of a reduced Thue system and show that for every Church-Rosser Thue system, there is a unique reduced Church-Rosser Thue system equivalent to it. Furthermore, the Knuth-Bendix completion procedure, when applied to a Thue system T, always produces the finite reduced Church-Rosser Thue system equivalent to T whenever such a system exists. Similar results can also be proved for almost-confluent Thue systems. Using properties of reduced Church-Rosser systems, we develop conditions under which a class of special Thue systems have equivalent finite Church-Rosser systems. In addition, we show that the completion procedure always terminates on finite parenthesized Thue systems, from which the termination of the completion procedure over ground-term-rewriting systems can be shown immediately. From the results discussed in this paper, we also obtain the termination of the Knuth-Bendix completion procedure for commutative Thue systems (commutative monoids) as a simple corollary.