Danish Mehmood
email: danish.mehmood@lums.edu.pk

Basit Shafiq

Jaideep Vaidya
email: jsvaidya@cimic.rutgers.edu

Yuan Hong
email: yhong@cimic.rutgers.edu

Nabil Adam
email: adam@cimic.rutgers.edu

Vijayalakshmi Atluri
email: atluri@cimic.rutgers.edu

Privacy-Preserving Subgraph Discovery

Graph structured data can be found in many domains and applications. Analysis of such data can give valuable insights. Frequent subgraph discovery, the problem of finding the set of subgraphs that is frequent among the underlying database of graphs, has attracted a lot of recent attention. Many algorithms have been proposed to solve this problem. However, all assume that the entire set of graphs is centralized at a single site, which is not true in a lot of cases. Furthermore, in a lot of interesting applications, the data is sensitive (for example, drug discovery, clique detection, etc). In this paper, we address the problem of privacy-preserving subgraph discovery. We propose a flexible approach that can utilize any underlying frequent subgraph discovery algorithm and uses cryptographic primitives to preserve privacy. The comprehensive experimental evaluation validates the feasibility of our approach.

Introduction

Today, graph structured data is ubiquitous. All types of relationships, including, spatial, topological, and other characteristics, can be modeled through the graph abstraction, thus capturing different data semantics. Graph-based analysis gives valuable insights into the data and has been successfully applied to various application domains including protein analysis [START_REF] Su | Application of knowledge discovery to molecular biology: Identifying structural regularities in proteins[END_REF],chemical compound analysis [START_REF] Chittimoori | Applying the subdue substructure discovery system to the chemical toxicity domain[END_REF], link analysis [START_REF] Mukherjee | Graph-based data mining for social network analysis[END_REF] and web searching [START_REF] Rakhshan | Structural web search engine[END_REF]. One of the most useful forms of analysis is to find frequent subgraphs from a large database of graphs. This has application in many different domains including cheminformatics (drug disovery), transportation networks, etc. Unlike standard frequent itemset discovery, used for association rule mining in transactional databases, frequent subgraph discovery is a much tougher problem due to underlying fundamental problems, such as canonical labeling of graphs and subgraph isomorphism.

In recent years, this has attracted a lot of attention with many efficient algorithms being developed to solve this problem. However, all of these algorithms assume that the set of graphs is either public or available at a single site. In reality, in many valuable cases, the set of graphs may be distributed between multiple parties, with each party owning a subset of the graphs. Chemical compound databases are one such example. Many pharmaceutical companies have local databases of pharmaceutical drugs which can be represented as graphs. Furthermore, in a lot of interesting applications, the data is sensitive (for example, drug discovery, clique detection, etc). Therefore, due to privacy and security concerns, the parties may not wish to reveal their individual graphs to each other or to a central site. In this case, a distributed privacy-preserving algorithm must be developed to enable mining in such cases. In this paper, we develop such an algorithm using cryptographic primitives to preserve privacy. Our algorithm uses any known subgraph discovery method as a subroutine, and therefore can be enhanced in the future as well. We have implemented our approach and the comprehensive experimental evaluation validates the feasibility of our approach.

Illustrative Example: Consider the case depicted in Figure 1, where 3 parties together own 5 graphs (Party 1 owns 2, Party 2 owns 2, and Party 3 owns 1). Figure 1 also depicts the common subgraph that is common to all of the five graphs. Therefore, even with a support threshold of 5, this graph will be detected when subgraph mining is done on the global set of graphs. Note that in this case, we assume that the graph is unlabeled (i.e., neither nodes nor edges are labeled). However, our approach is agnostic to the labeling -either the nodes, the edges, both, or neither could be labeled, based on the data semantics. As long as the underlying subgraph discovery algorithm can handle these cases, our approach will be able to take all of these requirements correctly into account.

Problem Statement

The basic problem is to discover frequent subgraphs in a privacy-preserving way from a set of graphs owned by different parties. This can be formalized as follows: Definition 1. Given k parties P 1 , . . . , P k , each of which own a set of graphs S i (let S = ∪ S i ), and a global threshold δ (0 ≤ δ ≤ 1), find the set of frequent subgraphs F S in a privacy-preserving fashion, wherein the global support of each subgraph in F S is over δ. Thus, for each subgraph f s j ∈ F S, ∑ i support(S i , f s j ) ≥ δ|S|, where support(S i , f s j ) = # graphs in S i that include f s j as a subgraph.

Note that in the definition above, we simply require that the set of frequent subgraphs is found in a privacy-preserving fashion. Under the framework of secure multiparty computation [START_REF] Yao | How to generate and exchange secrets[END_REF][START_REF] Goldreich | How to play any mental game -a completeness theorem for protocols with honest majority[END_REF], this equates to not leaking any additional information to any Fig. 2. Local candidate sets with respect to the example in Fig. 1 party beyond what can be inferred (in polynomial time) through the local input and output.

Instead of strictly following Definition 1, our protocol satisfies a relaxed form of this definition that allows efficient computation at the expense of leaking additional information. Below is the revised formulation with relaxed privacy requirement that the protocol satisfies. Definition 2. Given k parties P 1 , . . . , P k , each of which own a set of graphs S i (let S = ∪ S i ), and a global threshold δ (0 ≤ δ ≤ 1), find the set of frequent subgraphs F S (wherein the global support of each subgraph in F S is over δ) without leaking any additional information beyond the set of all local candidates, their support counts, and the number of parties owning them.

Proposed Approach

In this section, we present our proposed approach for privacy-preserving discovery of frequent subgraphs in the set of graphs distributed among multiple parties. The proposed approach essentially involves three key steps: The overall algorithm encompassing the above steps for subgraph discovery is given in Algorithm 1.This algorithm implements the distributed protocol involving k parties and a coordinator site. Each party owns a local set of graphs, and N is the total number of graphs, which is the sum of the number of graphs in the local set of all parties. The algorithms also uses a commutative cryptography system [START_REF] Pohlig | An improved algorithm for computing logarithms over GF(p) and its cryptographic significance[END_REF] for computing secure union and a homomorphic cryptography system [START_REF] Paillier | Public key cryptosystems based on composite degree residuosity classes[END_REF] for computing secure sum. Correspondingly, each party and coordinator site has a pair of commutative encryption and decryption keys; a public homomorphic encryption key which is shared among all the Algorithm 1 SubgraphDiscovery Require: k parties (P1, . . . , P k ) each owning a set of graphs and a coordinator site Coord Require: Pi owns the graph set, T . This threshold value is used to find a set of candidate frequent subgraphs from the set of local graphs GS (i) } 5: LocalCand (i) ← f ilter(gSpan(GS (i) , s

GS (i) = G (i) 1 , . . . , G (i) m Require: N = |GS (1) | + . . . + |GS (k) | Require: E (i) C , D (i) C Commutative
(i)
T , N odemin, Edgemin)) {run the gSpan algorithm locally to find the candidate frequent subgraphs from the local graph set. The f ilter function ensures that only those subgraphs that a party is comfortable with are included in the local candidate set.} 6: {STEP 2: Generation of Global Candidate Set} 7:

m (i) ← Encrypt(LocalCand (i) , E (i) C
). {The encryption method treats LocalCand (i) as a string so that the resulting cipher text m (i) does not reveal the structure of any of the local graphs.} 8: send m (i) (i) with length equal to the length of GlobalCand and initialize all the elements of Ecount (i) to random encryption of 0 using the homomorphic encryption key EH 18: for each subgraph sgj ∈ GlobalCand do 19:

for each local graph Gx ∈ GS (i) do 20:

if sgj is present in Gx then 21:

h 1 enc ← HomomorphicEncrypt(1, r, EH ) {Random encryption of 1 using homomorphic encryption key EH )} 22:

Ecount (i) [j] ← Ecount (i) [j] * h 1 enc 23: end if 24:
end for 25: end for 26: send Ecount (i) to Coord for secure sum 27: At Coord: 28: receive Ecount (i) from each party Pi 29: Count ← SecureSum(Ecount (1) q ← m (i) {m (i) is received from Pi} 7:

for j = 1 . . . k do 8:

if j ̸ = i then 9:

shuffle and send q to party Pj for commutative encryption with its key E (j) C

10: receive eq from Pj 11:

q ← eq 12:

end if for j = 1 . . . k do 5:

Ecnt[i] ← Ecnt[i] * Ecount (j) [i] 6:
end for 7: end for 8: Collaboratively decrypt Ecnt with T parties to get actual frequency count of each subgraph 9: return Decrypted Ecnt parties and coordinator; a private homomorphic decryption key derived from the public key. In addition, the algorithm requires the user to specify the support threshold (s T ), which is the percentage of total graphs in which the computed subgraphs are present. The user also specifies the minimum size of these subgraphs that need to be computed. This minimum size is specified in terms of the number of nodes (N ode min ) and number of edges (Edge min ).

Below we discuss each of the above three steps and how these steps are implemented in the Subgraph discovery algorithm.

Generation of Local Candidates

This step of generation of local candidates is implemented in lines 1 -4 of Algorithm 1. For generation of local candidates, each party runs the frequent subgraph mining algorithm. For frequent subgraph mining, we use the gSpan algorithm [START_REF] Yan | gspan: Graph-based substructure pattern mining[END_REF]. Our approach is agnostic to the underlying frequent subgraph mining algorithm. We chose gSpan since it was easily available and reasonably efficient. gSpan takes a collection of graphs and a minimum support threshold as input and computes all the subgraphs whose frequency is greater than or equal to the given threshold. In addition, we constrain the minimum size of subgraphs to avoid retrieving trivial subgraphs. For this, we use the (N ode min ) and (edge min ) parameters which are defined globally by the user.

Note that a f ilter function is applied to the output of gSpan to ensure that only those subgraphs that a party is comfortable with are included in its local candidate set. This improves the privacy protection. For computing the local candidate set, the support threshold needs to be closer to the global support threshold (s T ) or smaller to reduce the number of frequent sub-graphs that are missed from the final solution. Clearly, if a local support threshold corresponding to one graph only (i.e., a subgraph is present in only one of the local graph) is used, there will not be any miss. However, this significantly increases the computational overhead as there will be too many subgraphs in the local candidate set. We analyze this trade-off between performance and accuracy in our experiments discussed in Section 4.2.

Fig. 2 depicts the set of local candidates computed locally by each of the three parties P 1 , P 2 , and P 3 using their local set of graphs discussed in the Introduction and illustrated in Figure 1. In this Figure, the minimum size of the subgraphs are restricted to 4 nodes and 3 edges.

Generation of a Global Candidate Set

This step of generation of a global candidate set of frequent subgraphs is implemented in lines 5 -12 of Algorithm 1. Essentially, the global candidate set is the union of the local candidate sets computed by each party in Step 1. However, due to privacy requirements this union needs to be computed in a secure manner without revealing which candidate subgraph comes from which party. We employ a commutative encryptionbased approach for computing the secure union of the local candidate sets.

An encryption algorithm is commutative if plain text data item enciphered with multiple encryption keys in any arbitrary order will have the same enciphered text.Formally, an encryption algorithm is commutative if the following two equations hold for any given encryption keys K 1 , . . . , K n ∈ K, any data item to be encrypted m ∈ M , and any permutations of i, j :

∀m 1 , m 2 ∈ M such that m 1 ̸ = m 2 : E Ki 1 (...E Ki n (m)...) = E Kj 1 (...E Kj n (m)...) (1)
and for any given

k, ϵ < 1/2 k P r(E Ki 1 (...E Ki n (m 1 )...) = E Kj 1 (...E Kj n (m 2 )...)) < ϵ (2)
Pohlig-Hellman [START_REF] Pohlig | An improved algorithm for computing logarithms over GF(p) and its cryptographic significance[END_REF] is one example of a commutative encryption scheme (based on the discrete logarithm problem). This or any other commutative encryption scheme would work well for our purposes.

The basic idea of computing the secure union using the commutative encryption protocol is that each subgraph in every local candidate set is encrypted by all the parties using their commutative encryption keys. Then all these encrypted subgraphs are put into a global candidate set with their order shuffled. However, the elements in the encrypted global candidate set would have duplicates that need to be removed for the global candidate set to the union of all the local candidate sets. The encryption method used in the proposed approach treats each element in the local candidate set as a string so that the resulting cipher text mask the structural information of each local subgraph. Without knowing the structural information, duplicate subgraphs in the encrypted global candidate set cannot be removed. The following substeps elaborate on the proposed commutative encryption-based strategy for computing the secure union of local candidate set to form the global candidate set.

Substep 1. Each party P i represents its local candidate set into a string and applies its commutative encryption key E Substep 3. The encrypted global candidate set is sent by the coordinator to each party for decryption. Each party upon receiving the encrypted global candidate set shuffles its order and then applies its commutative decryption key. After all parties have applied their decryption keys, the structural information in the global candidate set is restored. After this the duplicate subgraphs in the global candidate set are removed (lines 17 -39 of Algorithm 2)). For duplicate removal, we perform a pairwise comparison between the subgraphs in the global candidate set using gSpan.

This strategy computes the global candidate set without revealing private information about the local subgraphs of any party to other parties -specifically, which subgraphs belong to which party. This is because during the commutative encryption substeps (substeps 1 and 2), the local candidate set of each party is encrypted by the encryption key of the party owning the graph. During the decryption phase all the local subgraphs are merged into one set with their order shuffled. Therefore, inferring which subgraph belongs to which party based on its position in the global candidate set is also not possible. The drawback of removing duplicates after decryption is that the coordinator would know how many parties have a given subgraph present in their graphs. We discuss this issue further in Section 3.

Removal of Non-frequent Subgraphs

The global candidate set is the union of the local candidate set. As discussed in Section 2.1 the support threshold for generation of subgraphs in the local candidate set may be smaller than the global support threshold. Therefore, all those subgraphs that do not satisfy the global threshold need to be removed from the global candidate set. This requires computing the frequency count (number of graphs in which a given subgraph is present) for each subgraph. This frequency count also needs to be computed in a secure and distributed manner as there is no global set of graphs and all the graphs are with their owner parties.

The step of removal of non-frequent subgraphs from the global candidate set is implemented in lines 13 -33 of Algorithm 1. intuitively in this step, each party P i computes the frequency count of each subgraph in the global set with respect to its local graph set GS (i) i (lines 17 -24 of Algorithm 1). This frequency count is stored in a vector which is sent to the coordinator. The coordinator after receiving the frequency count vector from all parties computes the sum for each subgraph in the global candidate set. If this sum is less than the given global support threshold, the corresponding subgraph is removed from the global candidate set (lines 22 -33 of Algorithm 1).

For secure computation and summation of the frequency counts, we employ an additive homomorphic cryptosystem such as the Paillier cryptosystem [START_REF] Paillier | Public key cryptosystems based on composite degree residuosity classes[END_REF]. An additive homomorphic encryption is semantically-secure public-key encryption which has the additional property that given any two encryptions E(A) and E(B), there exists an encryption E(A+B) such that E(A) * E(B) = E(A+B), where * denotes multiplication operator.

Following this homomorphic encryption property, each party initializes its frequency count vector by putting a random homomorphic encryption of '0' in each element of its frequency count vector (line 16 of Algorithm 1). When computing the frequency count of each subgraph in the nested for loop of lines 17 -24 of Algorithm 1, if a match is found the party increments the value of the corresponding element of the frequency count vector by '1'. This is done by multiplying the value of such element with a random homomorphic encryption of '1' (line 21 of Algorithm 1). Similarly, the coordinator employs a secure sum protocol to compute the sum of the frequency count vectors received from each party and employs threshold based decryption to decrypt the values of the global count for each subgraph. The reason for using threshold-based decryption strategy is to prevent a single party (coordinator) to decrypt the values in the frequency count vector received from each party. Threshold-based decryption with threshold of T requires T parties to collaboratively decrypt the encrypted values.

Complexity and Security Analysis

We now analyze the computation and communication complexity of our algorithms as well as the security provided through our approach.

Computation Cost

The computation cost of the distributed algorithm is actually comparable to the cost incurred in the centralized case. The main cost is incurred due to three steps, the local calls to the gSpan algorithm to find the local candidates, the commutative encryption based protocol to find the global candidate set, and the second round of local calls to the gSpan algorithm to find the frequency count of each candidate subgraph. Compared to these steps, the cost of the secure sum to find the global frequencies is negligible and can be ignored. Let us now consider the cost of each step.

Essentially, in the first step, even though each party invokes gSpan independently, it does so, only over the local set of graphs. Therefore the total computation cost is comparable to the cost of running gSpan over the entire set of graphs in a centralized case. In the second step, the secure union protocol is used to create a global candidate set. Essentially, each candidate subgraph is represented by a string, which is encrypted by all the parties, and then decrypted after merging into a combined set. Thus, assuming a total of l candidate graphs in the global set, the total cost is that of O(kl) encryptions and decryptions. In the third step, gSpan is run over each pair of candidate subgraph, and local graph. Thus, gSpan is invoked l|S| times, where |S| is the total number of graphs. Note that each invocation of gSpan in step 3 takes much less time than in step 1 as only two graphs are being compared.

Communication Cost

Communication between the parties only occurs when the local candidates are merged into a global set and sent to all of the parties, and in the final frequency determination phase. For the secure union, there are a total of O(kl) messages, for encryption and decryption. For the secure sum, it is the same with O(kl) messages being exchanged.

Security Analysis

Consider Algorithm 1. Step 1 is completely local, so no private information is disclosed. In step 2, the global candidate set is generated from the set of local candidates. Encryption is used to obscure the link between the candidates and the party generating them. The Secure Union protocol is used to securely combine the candidate sets. Assuming that this protocol is secure, nothing is leaked through the combination process, though all parties will learn the global candidate set (and can therefore identify candidates that do not belong to them, though they cannot identify which party the candidates come from). Note that, in reality, the secure union does leak some additional information. In the secure union (Algorithm 2), after merging local sub-graphs, duplicate sub-graphs are removed. However, the duplicates are removed after decryption. Therefore, the coordinator would know the number of parties that support each candidate sub-graph. In the extreme case where all parties support a particular subgraph, the coordinator would now know that the particular subgraph is frequent for all parties (though it still would not know which local subgraphs does it belong to for each party, as long as there are at least 3 parties).

In step 3, the non-frequent subgraphs are removed. For this, the support count of each of the candidate subgraphs is computed using the secure sum algorithm. Assuming this is secure, nothing is leaked, except for the support count (though, again, it is not clear which graphs contributed to this support count). In total, the overall process simply leaks the set of global candidates to all parties (along with the number of parties supporting each candidate, though only to the coordinator), as well as the frequency count (again, only to the coordinator).

Assuming that this additional information is given to the simulator, we can prove that the algorithm does not leak anything further. The question is whether this constitutes too much information. Let us consider each independently. Our algorithm leaks the set of global candidates, from which the final set of frequent subgraphs is picked. However, since each party locally mines its frequent subgraphs in step 1, it can easily refrain from including any of the subgraphs that it is uncomfortable with. This makes it difficult for any party to learn the entire graph or any unique / identifying subgraph of other parties. In the case of the frequency counts, if these are considered sensitive, it can be easily handled through the use of a simple add and compare [START_REF] Vaidya | Privacy-preserving k-means clustering over vertically partitioned data[END_REF] protocol that can check whether the global count of the candidate is above the threshold or not. Such a protocol can easily be implemented through the VIFF system1 .

Given a large set of graphs, this extra information can be considered to be acceptable and worth allowing, given the gain in efficiency that is obtained, as compared to generic secure multiparty computation techniques which would leak no information but be extremely slow. In this section we cover the details of our implementation of the privacy-preserving subgraph discovery algorithm on modern hardware and present experimental results demonstrating the usability of this algorithm. The general model of privacy preserving subgraph is as follows. The coordinator initiates a request for subgraph discovery. The coordinator could be a separate entity or one of the graph owner parties. There is one global coordinating class/interface that provides access to the subgraph discovery functionality. We call this the RmtMain interface. However, since this interface is present at a user site, the class implementing it should have access to no private information about the graphs of other parties. The class implementing this is the SiteCoordinator class which is initialized with the appropriate site information. There is another interface called, RmtSlave interfaces. All other parties that are involved in the sub-graph discovery process are treated as slave sites. The coordinator site coordinates with the slave sites to perform the required action.

Coordinator

Figure 3 demonstrates the basic interaction diagram. Java RMI is used to implement the distributed protocol between all of the sites.

We used Pohlig-Hellman encryption scheme [START_REF] Pohlig | An improved algorithm for computing logarithms over GF(p) and its cryptographic significance[END_REF] for implementing commutative encryption and Paillier Crypto system [START_REF] Paillier | Public key cryptosystems based on composite degree residuosity classes[END_REF] for implementing Homomorphic encryption.

Experimental Evaluation

We now present experimental results demonstrating the usability of the proposed algorithms. We ran our experiments on two real graph datasets [START_REF] Yan | gspan: Graph-based substructure pattern mining[END_REF] 4 shows the computation time and accuracy results of the SubgraphDiscovery algorithm for the Chemical 340 and Compound 422 datasets. The global threshold was set to 12% for both data sets. For the Chemical 340 dataset, the minimum size of the frequent subgraph was set to 5 nodes and 5 edges. The total number of frequent subgraphs in the Chemical 340 dataset satisfying the global threshold and minimum graph size requirements was 550. For the Compound 422 dataset, the minimum size of the frequent subgraph was also set to 5 nodes and 5 edges. In addition, we also constrain the maximum size to be 7 nodes and 7 edges. The total number of frequent subgraphs in the Compound 422 dataset satisfying the global threshold and minimum graph size requirements was 562. The graphs in both datasets were randomly distributed among three sites with each site having almost equal number of graphs.

Figure 4 shows the computation time and accuracy results against different local threshold values. Note that the running time depends much more on the local threshold level rather than the global threshold level, since the local threshold determines the As expected the accuracy is much higher for local threshold values that are closer to the global threshold or smaller. For example in both datasets, local threshold value of 9% yields 100% accuracy.

The appropriate local threshold is set by the parties in order to generate a reasonable set of candidates. From the security perspective, higher thresholds are better than lower. Therefore one possibility is to start from high threshold and progressively lower it to get an interesting set of results. This incremental computation does not incur any additional privacy loss since the results obtained at a higher threshold level are a subset of the results obtained at a lower threshold.

Figure 5 compares the computation time results for the Chemical 340 dataset distributed among 3, 4, and 5 sites. For this experiment both local and global threshold was set to 20%. The computation time increases with the number of sites. This is mainly due to the increase in number of messages for commutative encryption and decryption in step 2. Moreover, as the number of sites increases the coordinator has to interact with more sites for receiving the frequency count vector and summing them up for removal of non-frequent subgraphs (step 3).

Related Work

Privacy-preserving Data Mining (PPDM). The Work in PPDM has followed two major directions: i) randomization/perturbation; and ii) secure multiparty computation.

In the perturbation approach data is locally perturbed by adding "noise" before mining is done. For example, if we add a random number chosen from a Gaussian distribution to the real data value, the data miner no longer knows the exact value. However, important statistics on the collection (e.g., average) will be preserved. Agrawal and Srikant [START_REF] Agrawal | Privacy-preserving data mining[END_REF] introduced this notion as PPDM to the data mining community. Zhu and Lei [START_REF] Zhu | Optimal randomization for privacy preserving data mining[END_REF] study the problem of optimal randomization for privacy-preserving data mining and demonstrate the construction of optimal randomization schemes for density estimation.

The alternative approach of using cryptographic techniques to protect privacy was first utilized for the construction of decision trees by Lindell and Pinkas [START_REF] Lindell | Privacy preserving data mining[END_REF]. Later, these techniques were utilized in many subfields of data mining, e.g. association rule mining [START_REF] Vaidya | Secure set intersection cardinality with application to association rule mining[END_REF], clustering [START_REF] Jagannathan | Privacy-preserving distributed k-means clustering over arbitrarily partitioned data[END_REF], classification [START_REF] Du | Building decision tree classifier on private data[END_REF][START_REF] Vaidya | Privacy preserving naïve bayes classifier for vertically partitioned data[END_REF][START_REF] Vaidya | Privacy-preserving decision trees over vertically partitioned data[END_REF], outlier detection [START_REF] Vaidya | Privacy-preserving outlier detection[END_REF] and regression [START_REF] Karr | Secure regressions on distributed databases[END_REF][START_REF] Sanil | Privacy preserving regression modelling via distributed computation[END_REF]. Our work presents a secure method for frequent subgraph mining, which also follows the same line of research.

All of the cryptographic work falls under the theoretical framework of Secure Multiparty Computation [START_REF] Yao | How to generate and exchange secrets[END_REF][START_REF] Goldreich | How to play any mental game -a completeness theorem for protocols with honest majority[END_REF].

Frequent Subgraph Discovery. The graph mining techniques, in general, can be categorized into two categories:i) apriori-based approaches and pattern-growth based approaches.

In the first category, the apriori-based approaches follow the idea of apriori algorithm in frequent pattern mining for itemsets [START_REF] Agrawal | Fast algorithms for mining association rules[END_REF] -all the subgraphs of a discovered frequent subgraph are also frequent. AGM (apriori-based graph mining) [START_REF] Inokuchi | Complete mining of frequent patterns from graphs: Mining graph data[END_REF], FSG (frequent subgraph discovery) [START_REF] Kuramochi | Frequent subgraph discovery[END_REF] and PM (path mining) [START_REF] Gudes | Discovering frequent graph patterns using disjoint paths[END_REF] enumerate candidate subgraphs using vertices, edges and edge-disjoint paths respectively. Specifically, AGM [START_REF] Inokuchi | Complete mining of frequent patterns from graphs: Mining graph data[END_REF] discovers frequent subgraphs that occur above the percentage threshold of all graphs and uses a canonical representation of subgraphs for improving the efficiency of checking the subgraph isomorphism. FSG [START_REF] Kuramochi | Frequent subgraph discovery[END_REF] generates candidates with the edges which is shown in the adjacency matrix. The class of subgraphs discovered to connected subgraphs has been limited, and several heuristics have been proposed in [START_REF] Kuramochi | Frequent subgraph discovery[END_REF] to improve the efficiency of computing the subgraph support. Meanwhile, the efficiency of generating pattern candidates is also guaranteed. Similar to AGM and FSG, PM [START_REF] Gudes | Discovering frequent graph patterns using disjoint paths[END_REF] also generates candidate subgraph patterns using breadth-first enumeration. Nevertheless, this approach utilizes edge-disjoint paths to generate candidate patterns which reduces the number of iterations while still maintaining the completeness of the search space.

In the second category, the algorithm of gSpan (graph-based Substructure pattern mining) [START_REF] Yan | gspan: Graph-based substructure pattern mining[END_REF] discovers frequent subgraphs without candidate generation. It encodes the tree representation of graphs rather than the adjacency matrix using depth-first search code which provides a lexicographical order for searching the candidate patterns (subgraphs). gSpan algorithm performs efficiently not only on reducing the runtime cost but also saving memory space.

Conclusions and Future Work

In this paper, we have looked at the problem of finding frequent sub-graphs from a large distributed set of graphs in a privacy-preserving fashion. Our algorithm is flexi-ble and can use any underlying subgraph discovery approach as a subroutine. We have implemented our approach and the experimental evaluation shows that our approach is effective and allows a trade-off between utility and computation time. While we conducted the experimental evaluation with pharmaceutical data that have relatively small graph size, we plan to follow on with experiments on social network data. In the future, we also plan to consider the case of a single global graph, which is distributed between multiple parties (this happens in many cases such as transactions shared between financial organizations, call graphs, etc.) Here, you can find local frequent substructures as described in our paper, however, the inter-edges cause a problem. This could perhaps be solved using the graph duality restructuring approach (by building the dual of the graph, with nodes becoming edges, and vice versa). We plan to explore this in the future.

Fig. 1 .

 1 Fig. 1. Graphs owned by three parties (P1, P2, and P3) and the subgraph present in all the graphs of each party.

C 3 1 :

 31 ) to Coord {dq is decryption of q with the Commutative decryption key D SecureSUM(Ecount(1) , . . . , Ecount(k) )Require: Threshold-based homomorphic crypto system Require: EH A public Homomorphic encryption key Require: D (i) H Homomorphic decryption key of party Pi and D Coord H Homomorphic decryption key of Coord Require: T , Threshold for homomorphic decryption (No. of parties needed for decryption) At Coord: 2: Create an array Ecnt with length equal to the length of GlobalCand and initialize all the elements of Ecnt to random encryption of 0 using the homomorphic encryption key EH 3: for i = 1 . . . length(Ecnt) do 4:

C

  on the resulting string. This encrypted local candidate set is then sent to Coord for secure union. (Lines 5 and 6 of Algorithm 1) Substep 2. The Coord receives the encrypted local candidate set from each party and routes each candidate set to all other parties for commutative encryption. When all the local candidate sets are encrypted by all parties, the Coord combines them into one global encrypted set (Lines 7 -11 of Algorithm 1 and lines 1 -16 of Algorithm 2).

Fig. 3 .

 3 Fig. 3. Basic Interaction Diagram

1 .

 1 Generation of local candidates -each party computes a candidate set of frequent subgraphs from it local graph set. 2. Generation of a global candidate set of subgraphs -secure union of local candidates to form a global candidate set -the global candidate set is generated by performing secure union of the local candidate sets. 3. Removal of non-frequent subgraphs from the global candidate set -the frequency count of each subgraph in the global candidate set is compared against a global threshold to check if this candidate is a real result.

{STEP 3: Removal of Non-frequent Subgraphs} 15: send GlobalCand to each party Pi 16: At each party Pi: 17: create an array Ecount

	to Coord for secure union
	9: At Coord:
	10: F SG ← {}
	11: receive m (i) from each party Pi 12: M ← ∪ k i=1 m (i)
	13: GlobalCand ← SecureU nion(M )
	14:

  : i) Chemical 340; ii) Compound 422. The Chemical 340 dataset 340 chemical compounds, 24 different atoms, 66 atom types, and 4 types of bonds. The average graph size in this dataset is 27 nodes and 28 edges. The largest graph in this dataset has 214 nodes and 214 edges.

				Chemical 340
	Dataset		Total graphs = 340; Average graph size = (27 nodes, 28 edges); Largest
			graph size = (214 nodes, 214 edges)
	Frequent		Size(Node min =5, Edge min =5); Global Threshold = 12%; Number of
	Subgraphs	frequent subgraphs = 550
	Sites		Randomly distributed among 3 sites with each site having equal number
			of graphs
	No.	Local	Average	Step 1	Step 2	Step 3	Total	Accuracy
	Threshold	subgraphs per	Time	Time	Time	Time
	(%age)	site	(sec)	(sec)	(sec)	(sec)	(%age)
	1	9	1308	23	8,871	1,537 10,423	100
	2	13	513	14	2,761	458	3,233	99.82
	3	15	393	12	2,087	359	2,458	95.82
	4	18	264	11	1336	249	1,596	71.09
	5	19	203	10	1008	205	1,223	58.55
	6	22	120	11	578	151	740	33.82
				Compound 422
	Dataset		Total graphs = 422; Average graph size = (40 nodes, 42 edges); Largest
			graph size = (189 nodes, 196 edges)
	Frequent		Size (Node min =5, Edge min edges=5; Node max =7, Edge max edges=7); Global
	Subgraphs	Threshold = 12%; Number of frequent subgraphs = 562
	Sites		Randomly distributed among 3 sites with each site having equal number
			of graphs
	No.	Local	Average	Step 1	Step 2	Step 3	Total	Accuracy
	Threshold	subgraphs per	Time	Time	Time	Time
	(%age)	site	(sec)	(sec)	(sec)	(sec)	(%age)
	1	9	728	14	3768	661	4433	100
	2	12	571	13	2739	513	3265	100
	3	15	442	12	2094	437	2543	95.20
	4	18	351	14	1631	341	1986	78.29
	Fig. 4. Computation time and accuracy vs. local threshold for Chemical 340 and Compound 422
	datasets
	The Compound 422 dataset has 422 graphs with average graph size of 40 nodes and 42
	edges. The largest graph in this dataset has 189 nodes and 196 edges.
	Figure

  Computation time and accuracy vs. number of sites number of candidates which in turn determines the time taken by steps 2 and 3. For both datasets, the computation time decreases as the local threshold value increases. This is because increasing the local threshold results in smaller number of local candidate subgraphs and consequently the size of the global candidate set decreases. Also, it is obvious from the results that the computation overhead of step 2 (Generation of global candidate set) dominates all other steps. This step involves encryption of the local candidate set, computing secure union, and removing duplicates.

			Chemical 340 -multiple sites
	Dataset		Total graphs = 340; Average graph size = (27 nodes, 28
			edges); Largest graph size = (214 nodes, 214 edges);
			Randomly distributed among sites.
	Frequent	Size(Node min =5, Edge min =5); Global Threshold = 20%;
	Subgraphs	Local Threshold = 20%; Number of frequent subgraphs =
			134
	Sites	Average	Step 1	Step 2	Step 3	Total	Accuracy
		subgraphs	Time	Time	Time	Time
		per site	(sec)	(sec)	(sec)	(sec)	(%age)
	3	171	10	830	188	1028	100
	4	263	13	2455	336	2804	100
	5	284	16	4188	605	4809	100
		Fig. 5.

http://viff.dk/

Acknowledgements

The work of Mehmood and Shafiq is supported in part by the LUMS Departmental Research Grant. The work of Vaidya is supported in part by the National Science Foundation under Grant No. CNS-0746943. The work of Atluri is supported through the IR/D by the National Science Foundation.


Alessandro Armando

Silvio Ranise

Automated and Efficient Analysis of Role-Based Access Control with Attributes

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Role Based Access Control (RBAC) [START_REF] Sandhu | Role-Based Access Control Models[END_REF] is one of the most widely adopted model for information security. It regulates access by assigning users to roles which, in turn, are granted permissions to perform certain operations. Despite several advantages (e.g., reduction of the complexity of security administration), it has been observed that RBAC suffers some inflexibility in adapting to rapidly evolving domains in particular when there is a need to take into account dynamic attributes to determine the permissions of a user. The problem is the explosion in the number of roles that should be considered in order to specify the various sets of permissions that a user may acquire depending on the values of the dynamic attributes.

To overcome this problem, [START_REF] Kuhn | Adding Attributes to Role Based Access Control[END_REF] proposes to add attributes to RBAC and overviews several approaches to do this. Among these, the one called Dynamic Roles (DRs) determines the user's role depending on his/her attributes. The interest of DRs is that they retain the structure of the RBAC model while providing additional flexibility to cope with attributes. A similar approach have already been investigated in [START_REF] Al-Kahtani | A Model for Attribute-Based User-Role Assignment[END_REF][START_REF] Al-Kahtani | Induced Role Hierarchies with Attribute-Based RBAC[END_REF] and problems concerning redundancies in the rules that assign users to roles and possible inconsistencies with the standard RBAC role hierarchy are studied. Furthermore, in [START_REF] Al-Kahtani | Rule-based RBAC with negative authorization[END_REF], negative roles are introduced to widen the scope of applicability of the RBAC model to those situations in which an open (allow-by-default) policy approach is adopted (i.e. access is denied if there exists a corresponding negative authorization and is permitted otherwise [START_REF] Samarati | Access control: Policies, Models, and Mechanisms[END_REF]). In this context, conflicts may arise among rules that assign users to a role and, at the same time, to the negated role.

Clearly, simply authoring a set of rules that assign users to roles is not sufficient: an organization must also be able to analyse it in order to avoid the kind of problems sketched above. Testing, while useful, is not exhaustive and, as organizations grow, their rule set can become very large, which places particular burden on the quality of testing. Designers of RBAC policies with DRs would thus benefit from complementing testing with more exhaustive and automatic, formal analysis techniques. In this respect, the paper makes three contributions.

First, we give an abstract definition for policies with DRs that naturally extends the RBAC model (Section 2). Negative authorization (via negated roles) can be easily accommodated in the proposed framework (Section 2.3).

Second, we provide a rule-based characterization of the association between users' attributes and roles (Section 2) that allows us to formally state two crucial problems for the design of RBAC policies with DRs: detection of redundancies (Section 2.1) and detection of conflicts (Section 2.3).

Third (Section 4.1), we show how conditions on the users' attributes of authorization rules can be expressed by theories, whose satisfiability problems can be efficiently decided by Satisfiability Modulo Theories (SMT) solvers (Section 3) and characterize the decidability and the complexity of the problems of detecting redundancies and conflicts under natural assumptions on the theories of the attributes (Sections 4.2 and 4. 3). An experimental evaluation with a prototype implementation of the algorithm (Figure 1) used for the decidability results on a synthetic benchmark confirms the viability of the approach (Section 4.4).

Related work and conclusions are also discussed (Section 5). Proofs can be found in the extended version of this paper available at http://st.fbk.eu/ SilvioRanise#Papers.

RBAC with Dynamic Roles

Preliminarily, we recall some basic notions concerning the RBAC model [START_REF] Sandhu | Role-Based Access Control Models[END_REF]. RBAC regulates access through roles. Roles in a set R associate permissions in a set P to users in a set U by using the following two relations: U A ⊆ U × R and P A ⊆ R × P . Roles are structured hierarchically so as to permit permission inheritance. Formally, a role hierarchy is a partial order RH on R, where (r 1 , r 2 ) ∈ RH means that r 1 is more senior than r 2 for r 1 , r 2 ∈ R. A user u is an explicit member of role r when (u, r) ∈ U A, u is an implicit member of r if there exists r ∈ R such that (r , r) ∈ RH and (u, r ) ∈ U A, and u is a member of role r if he/she is either an implicit or explicit member of r. Given U A and P A, a user u has permission p if there exists a role r ∈ R such that (p, r) ∈ P A and u is a member of r. A RBAC policy is a tuple (U, R, P, U A, P A, RH).

When extending RBAC with dynamic roles, the relation U A is not given explicitly but it is defined in terms of pairs (attribute name, attribute value). A RBAC policy with Dynamic Roles (RBAC-DR) is a tuple (U, R, P, a, D a , s a , AR, P A, RH) where U , R, P , P A, and RH are as in the RBAC model above, a is a (finite) sequence of attributes, D a is a (finite) sequence of domains associated to a, s a is a sequence of user-attribute mappings associated to a (the sequences a, D a , and s a have equal length) such that for each a in a (written a ∈ a) s a is a function from U to 2 Da , and AR is the attribute-role relation that contains tuples of the form (C, r) where C is a set of pairs (a, e a ) with e a ∈ D a for a ∈ a and r ∈ R. (In the following, the sub-script of D a and s a will be dropped to simplify the notation.) Given a RBAC-DR policy (U, R, P, a, D, s, AR, P A, RH), a user u ∈ U is an explicit member of role r ∈ R under the user-attribute mapping s iff there exist a pair (C, r) ∈ AR and a set S u ⊆ C such that e a ∈ s a (u) for every (a, e a ) ∈ S u . The notions of "being an implicit member of a role" and "having a permission" are defined as those of RBAC policies above.

Rule-based Authorization Rules

The most difficult part in the design of a RBAC-DR policy is the definition of the attribute-role relation. To do this, following [START_REF] Al-Kahtani | A Model for Attribute-Based User-Role Assignment[END_REF], we use authorization rules that associate a role to a user provided that his/her attribute values satisfy certain conditions. Let a = a 1 , ..., a n be a sequence of attributes, a pair (b, C) r) ∈ AU and (e 1 , ..., e m ) ∈ C}. By abuse of notation, a tuple (U, R, P, a, D, s, AU, P A, RH), where AU is a finite set of authorization rules and all the other components are as in a RBAC-DR policy, will also be called a RBAC-DR policy. Given a RBAC-DR policy (U, R, P, a, D, s, AU, P A, RH), a user u satisfies the condition C(b 1 , ..., b m ) of an authorization rule in AU under the user-attribute mapping s, in symbols u, s C(b 1 , ..., b m ), iff (e 1 , ...e m ) ∈ C and e j ∈ s bj (u) for j = 1, ..., m. The implicit user-role relation IUA ⊆ U × R is defined as IUA := {(u, r) | there exists (C r) ∈ AU such that u, s C}. A user u ∈ U is a member of role r ∈ R under the user-attribute mapping s (via the notion of attribute-role relation associated to the set AU of authorization rules) iff (u, r) ∈ IUA.

For effectiveness, we assume the computability of (a) the user-attribute assignments and of (b) the membership to the conditions of the authorization rules as well as to (c) the relations RH and PA. Requirement (a) is reasonable as the notion of user-attribute assignment is an abstraction of the mechanism that associates users with attributes (e.g., an LDAP). Requirement (b) is necessary for the effectiveness of the satisfaction relation . Concerning (c), we observe that since the sets R and P are finite in several applications, then membership to RH and PA is obviously computable.

Example 1. We consider a refined version of the example in [START_REF] Al-Kahtani | A Model for Attribute-Based User-Role Assignment[END_REF] for an on-line entertainment store streaming movies to users. The store needs to enforce an access control policy that is based on the user's age and the country where the user lives that may have different regulations for considering someone as an adult, a teen, or a child. E.g., for the legislation of Italy and France, one is considered adult when he/she is 18 or older while in Japan the adult age is 20.

For simplicity, we assume there are only three users Alice, Bob, and Charlie. Alice is 12 years old and lives in Italy, Bob is 39 and lives in Japan, and Charlie is 17 and lives in France. We leave unspecified the permissions, the role hierarchy, and the role-permission assignment as we want to focus on the user-role assignment based on the age and country attributes. In the corresponding RBAC-DR policy (U, R, P, a, D, s, AU, P A, RH), we have that U := {Alice, Bob, Charlie}, R := {Adult, Teen, Child }, a = age, country, D = N, WC where WC is an enumerated set containing all the countries in the world, s = s age , s country where s age = {Alice → 12, Bob → 39, Charlie → 17}, s country = {Alice → Italy, Bob → Japan, Charlie → France}, and AU contains, among others, the following authorization rules: that correspond to the policy informally described above (a and c abbreviate age and country, respectively). It is not difficult to see that Bob, s ρ 1 but Bob, s ρ 2 , that Charlie, s ρ 3 but Charlie, s ρ i for i = 1, 2, 4, and that Alice, s ρ 4 but Alice, s ρ i for i = 1, 2, 3. As a consequence, we have that, e.g., (Alice, Child ) ∈ IUA, (Bob, Adult) ∈ IUA, and (Charlie, Teen) ∈ IUA.

ρ1 : {(a, c) ∈ N × WC |a ≥ 20 and c ∈ {Japan, Indonesia}} Adult, ρ2 : {(a, c) ∈ N × WC |a ≥ 18 and c ∈ {Italy, France, ...}} Adult, ρ3 : {(a, c) ∈ N × WC |13 ≤ a ≤

Redundancies in RBAC-DR policies

As observed in [START_REF] Al-Kahtani | Induced Role Hierarchies with Attribute-Based RBAC[END_REF], for RBAC-DR policies, besides the usual role hierarchy RH, it is possible to define another hierarchy IRH induced by the authorization rules in AU . We follow [START_REF] Al-Kahtani | Induced Role Hierarchies with Attribute-Based RBAC[END_REF] and since IRH is defined for every possible userattribute mapping, we introduce the notion of RBAC-DR family of policies as a tuple (R, P, a, D, AU, P A, RH) where its components are the same as those of a RBAC-DR policy; in other words, a RBAC-DR family of policies is a RBAC-DR policy where the users and the user-attribute assignment are omitted. For every pair (ρ 1 , ρ 2 ) of authorization rules in AU , ρ 1 is more senior than ρ 2 (in symbols, ρ 1 ρ 2 ) iff for every user u and every user-attribute assignment s if u, s C 1 then also u, s C 2 , where C i is the condition of ρ i for i = 1, 2, i.e. when the set of users satisfying C 1 is a subset of that satisfying C 2 under every possible user-attribute mapping s. Then, we define (r 1 , r 2 ) ∈ IRH , i.e. the pair (r 1 , r 2 ) is in the induced role hierarchy IRH , iff for each rule (C 1 r 1 ) ∈ AU there exists a rule (C 2 r 2 ) ∈ AU such that (C 1 r 1 ) (C 2 r 2 ). The key difference between RH and IRH is that the former is designed so that seniority among roles reflects inheritance of permissions associated to them whereas the latter characterizes seniority according to the sets of users associated to them by the set AU of authorization rules. It may happen that the induced role hierarchy IRH is such that both (r, r ) ∈ IRH and (r , r) ∈ IRH for two distinct roles r, r ∈ R, i.e. the set of users associated to r and that associated to r are identical. This is so because IRH is a quasi-order (i.e. it is reflexive and transitive) and not a partial order as RH (that is also anti-symmetric). This implies a redundancy in the definition of IRH since the two roles r 1 and r 2 can be considered equivalent as both (r 1 , r 2 ) ∈ IRH and (r 2 , r 1 ) ∈ IRH . This does not necessarily imply a problem in the authorization rules but it is desirable that designers become aware of all the redundancies in IRH (see [START_REF] Al-Kahtani | Induced Role Hierarchies with Attribute-Based RBAC[END_REF] for more on this issue). Notice that once the "more senior than" relation among the authorization rules in AU is known, detecting redundancies in IRH becomes obvious. As a consequence, we define the problem of computing the "more senior than relation" over a set AU of authorization rules (MS-AU problem, for short) as follows: given a RBAC-DR family (R, P, a, D, AU, P A, RH) of policies, the MS-AU problem amounts to checking whether ρ 1 ρ 2 for every pair ρ 1 and ρ 2 of authorization rules in AU . Notice that this problem is stated for a RBAC-DR family of policies and thus must be solved regardless of the set of users and the user-attribute mapping.

Solving the MS-AU problem allows one to eliminate the redundancies in IRH . Formally, this amounts to first turning into a partial order in such a way that also IRH is so. This is a crucial pre-requisite to apply the techniques in [START_REF] Al-Kahtani | Induced Role Hierarchies with Attribute-Based RBAC[END_REF] to detect (and eliminate) any "disagreement" between RH and IRH , i.e. to identify those situations in which the security policies encoded by the authorization rules and the business practices captured by RH do not match. Although we do not explore this problem further, we observe that the automated technique to solve MS-AU problems in Section 4.2 facilitates the application of the techniques in [START_REF] Al-Kahtani | Induced Role Hierarchies with Attribute-Based RBAC[END_REF].

RBAC-DR with negative authorization

In [START_REF] Al-Kahtani | Rule-based RBAC with negative authorization[END_REF], negative authorizations are added to the RBAC-DR model by allowing negated roles in authorization rules. The intuition is that an authorization rule with a negative role r denies access to the permissions associated to r via the permission-assignment relation. This characterization of negative roles allows for the adoption of the so-called open (allow-by-default) policy semantics [START_REF] Jajodia | Flexible support for multiple access control policies[END_REF][START_REF] Samarati | Access control: Policies, Models, and Mechanisms[END_REF] in an extension of the RBAC model, that is based on positive permissions conferring the ability to do something on the holders of the permissions [START_REF] Sandhu | Role-Based Access Control Models[END_REF]. This is crucial to widen the scope of applicability of the RBAC model extended with dynamic roles to applications where the set of users is not known a priori, e.g., web-services. Unfortunately, as pointed out in [START_REF] Al-Kahtani | Rule-based RBAC with negative authorization[END_REF], the addition of negative authorizations introduces conflicts that need to be detected and then resolved.

Formally, we define the set SR = {+, -} × R of signed roles and write the pairs (+, r) and (-, r) as +r and -r, respectively, for a role r ∈ R. We extend the definition of authorization rule as follows: a pair C sr is a signed authorization rule where C is a condition and sr ∈ SR. Intuitively, a user u satisfying the condition C of a signed authorization rule of the form C -r under a certain user-attribute mapping is forbidden to be assigned the role r. A RBAC-DR policy with negative roles (RBAC-NDR) is a tuple (U, R, P, a, D, s, AU, P A, RH) where U, R, P, a, D, s, P A and RH are as in a RBAC-DR policy and AU is a set of signed authorization rules. A RBAC-NDR family of policies is the tuple (R, P, a, D, AU, P A, RH)

To understand the kind of conflicts that may arise from the use of signed authorization rules, consider ρ 1 := (C 1 +r) and ρ 2 := (C 2 -r) such that a user u satisfies both C 1 and C 2 under a certain user-attribute mapping. At this point, we are faced with the problem of deciding whether the user u should be assigned or not the role r. As discussed in [START_REF] Al-Kahtani | Rule-based RBAC with negative authorization[END_REF], there are several strategies to resolve the problem, e.g., by adopting a "deny-override" strategy where a user u can be assigned a role r provided that u satisfies the condition C of a rule of the form C +r in AU and there is no rule in AU of the form C -r such that u satisfies the condition C that forbids the assignment of r to u. However, this or alternative conflict elimination strategies may be unsatisfactory for certain applications; see again [START_REF] Al-Kahtani | Rule-based RBAC with negative authorization[END_REF] for details. Furthermore, certain conflicts may arise from errors in the design of the authorization rules and must be identified in order to correct them. As a consequence, we define the problem of detecting conflicts in the set AU of signed authorization rules (CD-SAU problem, for short) as follows: given a RBAC-NDR family (R, P, a, D, AU, P A, RH) of policies, the CD-SAU problem amounts to checking whether for each pair (C +r, C -r) in AU , there is no user u satisfying both C and C under a user-attribute mapping s. As for the MS-AU problem, also the CD-SAU problem is stated for a family of policies and thus must be solved for any set of users and any user-attribute mapping.

Satisfiability Modulo Theories Solving

We assume the usual syntactic (e.g., signature, variable, term, atom, literal) and semantic (e.g., structure, truth) notions of many-sorted first-order logic with equality (see, e.g., [START_REF] Enderton | A Mathematical Introduction to Logic[END_REF]). A constraint (clause, resp.) is a conjunction (disjunction, resp.) of literals (i.e. atoms or their negations) and a quantifier-free formula is an arbitrary Boolean combination of atoms.

According to [START_REF] Ranise | The SMT-LIB Standard: Version 1[END_REF], a theory T is a pair (Σ, C), where Σ is a signature and C is a class of Σ-structures; the structures in C are the models of T . Given a theory T = (Σ, C), a quantifier-free Σ-formula φ(v)-i.e. a quantifier-free formula built out of the symbols in Σ and the variables in the sequence v-is T -satisfiable if there exists a Σ-structure M in C and a valuation µ mapping the variables in v to values of the domain of

M such that φ(v) is true in M (in symbols, M, µ |= φ); it is T -valid (in symbols, T |= ϕ) if M, µ |= ϕ(v) for every M ∈ C
and every valuation µ. The quantifier-free formula ϕ(v) is T -valid iff its negation ¬ϕ(v) is T -unsatisfiable. For example, if ϕ is the implication ϕ 1 → ϕ 2 , then its T -validity is equivalent to the T -unsatisfiability of the conjunction of ϕ 1 with the negation of ϕ 2 (ϕ 1 ∧ ¬ϕ 2 ).

The satisfiability modulo the theory T (SM T (T )) problem amounts to establishing the T -satisfiability of quantifier-free Σ-formulae. Many state-of-the-art SMT solvers, in their simplest form, tackle the SMT(T ) as follows. Initially, each atom occurring in the input quantifier-free formula ϕ is considered simply as a propositional letter (in other words, the theory T is forgotten). Then, the "propositional abstraction" of ϕ is sent to a SAT solver. If this reports propositional unsatisfiability, then ϕ is also T -unsatisfiable. Otherwise, an assignment of truth values to the atoms in ϕ is returned that makes its propositional abstraction true. Such an assignment can be seen as a conjunction of literals and checked by a specialized theory solver for T that can only deal with constraints (i.e. conjunctions of literals). If the theory solver establishes the T -satisfiability of the constraint then ϕ is also T -satisfiable. Otherwise, the theory solver computes a clause that, once added to the SAT solver, precludes the assignment of truth values that has been considered. The SAT solver is then started again. This process is repeated until the theory solver reports the T -satisfiability of one assignment or all the assignments returned by the SAT solver are found Tunsatisfiable so that also ϕ is reported to be T -unsatisfiable. Various refinements of this basic schema have been proposed for efficiency, the interested reader is pointed to, e.g., [START_REF] Sebastiani | Lazy Satisfiability Modulo Theories[END_REF][START_REF] Moura | Satisfiability modulo theories: introduction and applications[END_REF].

The SMT(T ) problem is NP-hard as it subsumes the SAT problem. To evaluate the additional complexity due to the theory T , we focus on theory solvers and consider the complexity of checking the T -satisfiability of constraints, called the constraint T -satisfiability problem for some theories that have been found useful for the declarative specifications of authorization policies (see, e.g., [START_REF] Li | Datalog with constraints: a foundation for trust management langauges[END_REF]). The theory EU F of equality with uninterpreted function symbols is the theory interpreting the symbol = as an equivalence relation that is also a congruence. The constraint EU F-satisfiability problem is decidable and polynomial. The theory ED({v 1 , ..., v n }, S) of the enumerated data-type S with values {v 1 , ..., v n } (for n ≥ 1) is the theory whose signature consists of the sort S, the constant symbols v 1 , ..., v n of sort S, and its class of models contains all the structures whose domain contains exactly n distinct elements. The constraint ED-satisfiability problem is decidable and NP-complete. Linear Arithmetic on the Rationals (Integers, resp.) LAR (LAI, resp.) is the theory whose class of models is the singleton containing the usual structure R of the Reals (Z of the integers, resp.) and whose atoms are equalities, disequalities, and inequalities of linear polynomials whose coefficients are integers and the variables take values over the Reals (integers, resp.). The constraint satisfiability problems for LAR and LAI are decidable, the former is polynomial and the latter is NP-complete. The theory RDL of real difference logic is the sub-theory of LAR whose atoms are written as x -y c where is an arithmetic operator, x and y are variables, and c ∈ R. The theory IDL of integer difference logic is defined as RDL but it is a sub-theory of LAI. Both the constraint RDL-and IDL-satisfiability problems are decidable and polynomial. For more details about these and other theories, see, e.g., [START_REF] Sebastiani | Lazy Satisfiability Modulo Theories[END_REF][START_REF] Moura | Satisfiability modulo theories: introduction and applications[END_REF]. Many applications require to reason about conjunctions of constraints coming from several theories T 1 , ..., T n . In this situation, it is easy to build a theory solver by reusing those available for the theories T 1 , ..., T n as follows. Let α = α 1 (v 1 )∧• • •∧α n (v n ) be a composite constraint, i.e. α i is a literal over the signature of T i for i = 1, ..., n whose variables v i are disjoint with those of the other constraints. Then, α is satisfiable iff each α i is T i -satisfiable and it is unsatisfiable otherwise, i.e. there exists i ∈ {1, ..., n} such that α i is T i -unsatisfiable. Thus, if the constraint T i -satisfiability problem is decidable and polynomial for each i = 1, ..., n, then it is also decidable and polynomial to check the satisfiability of composite constraints.

Solving the MS-AU and CD-SAU problems

We explain how RBAC-DR and RBAC-NDR policies can be specified by using theories and how this allows us to prove the decidability of the MS-AU and CD-SAU problems. The proof is constructive and reduces both problems to a sequence of SMT problems that can be efficiently solved by invoking state-ofthe-art SMT solvers.

Specifying RBAC-DR and RBAC-NDR policies with theories

The idea is to use quantifier-free formulae of a suitable theory to specify the conditions of (signed) authorization rules. Formally, we assume the availability of a theory T A = (Σ A , C A ) of attributes and define a RBAC-DR policy with background theory T A of attributes as a tuple (U, R, P, a, s, AU QF , P A, RH) where U, R, P, P A, and RH are as specified above, and the following conditions hold: (C1) each a ∈ a is a first-order variable of sort S a in Σ A and each s a ∈ s is a mapping s a : U → 2 S M A a for some M A ∈ C A (where σ M A is the interpretation in M A of the symbol σ ∈ Σ; e.g., S M A a is a subset of the domain of M A ), (C2) for every e ∈ S M A there exists a constant c of sort S a in Σ A such that c M A = e for some M A ∈ C A ,3 and (C3) the set AU QF contains finitely many pairs of the form ϕ(b) r, called syntactic authorization rules, where ϕ is a quantifier-free formula built out of the symbols of Σ A and the variables in b, that is a sub-sequence of a.

The crucial observation is that each quantifier-free formula ϕ(b) in a syntactic authorization rule ϕ(b) r in AU QF defines a condition C(b), in the sense of Section 2.2, as follows: (e 1 , ..., e m ) ∈ C(b) iff there exists M A ∈ C A and a valuation µ such that µ(b j ) = e j ∈ S M A bj for j = 1, ..., m and M A , µ |= ϕ(b). In the following, the condition C(b) associated to the quantifier-free formula ϕ(b) is written as [[ϕ(b)]]. Thus, a RBAC-DR policy (U, R, P, a, s, AU QF , P A, RH) with background theory T A = (Σ A , C A ) of the attributes defines the following RBAC-DR policy: (U, R, P, a, D, s, AU, P A, RH) where

D a = S M A a for each a ∈ a and AU = {[[ϕ(b)]] r | (ϕ(b) r) ∈ AU QF } for some M A ∈ C A .
Similar definitions can be given for RBAC-NDR policies and RBAC-DR (RBAC-NDR) family of policies with background theory T A of attributes.

Example 2. For Example 1, we consider composite constraints from the enumerated data-type theory ED({Italy, France, Japan, Indonesia, ...}, C) for the set W C of world countries and the theory IDL for the constraints on the age (see Section 3). The attribute country is also seen as a variable of sort C and the attribute age as a variable of sort Z. As a consequence, the syntactic authorization rules corresponding to the authorization rules in Example 1 are:

ρ1 : -age ≤ -20 ∧ (country = Japan ∨ country = Indonesia) Adult, ρ2 : -age ≤ -18 ∧ (country = Italy ∨ country = France ∨ • • • ) Adult, ρ3 : -age ≤ -13 ∧ age ≤ 17 ∧ (country = Italy ∨ country = France ∨ • • • ) Teen, ρ4 : age ≤ 12 ∧ (country = Italy ∨ country = France ∨ • • • ) Child
Notice that country ∈ {c 1 , ..., c n } has been translated as n i=1 country = c i . By generalizing the observations in the example, it is not difficult to see that the language to express authorization rules introduced in [START_REF] Al-Kahtani | A Model for Attribute-Based User-Role Assignment[END_REF] can be translated to syntactic authorization rules provided that a suitable background theory of attributes is used.

Proposition 1. Given a RBAC-DR policy (U, R, P, a, s, AU QF , P A, RH) with background theory

T A = (Σ A , C A ) of the attributes. If the SMT(T A ) problem is decidable, then it is decidable to check if a user u ∈ U is a member of a role r ∈ R.
An obvious corollary of this proposition and the fact that the membership to RH and P A is computable is that checking whether a user is an implicit member of a role or he/she has a permission are also decidable.

In the following, without loss of generality, we assume that (A1) any condition of an authorization rule is T A -satisfiable but not T A -valid (i.e. its negation is also T A -satisfiable) and (A2) the conditions of the syntactic authorization rules in AU QF are constraints and not arbitrary Boolean combinations of atoms. The two situations ruled out by assumption (A1) can be automatically identified under the assumption that the SMT(T A ) problem is decidable and can be safely discarded as uninteresting: those that are T A -satisfiable never assigns a user to a role while those that are T A -valid assigns any user to a role (this kind of problems have been considered in the context of a similar rulebased specification framework for access control policies [START_REF] Ribeiro | Security Policy Consistency[END_REF]). To see why assumption (A2) is without loss of generality, consider a rule ϕ r in AU QF where ϕ is a quantifier-free formula (and r ∈ R). Since it is possible to transform ϕ into disjunctive normal form, i.e. into a formula of the form d j=1 α j where α j is a constraint (for j = 1, ..., d and d ≥ 1), we can consider the set AU QF := AU QF \ {ϕ r} ∪ {α j r | j = 1, ..., d}. Clearly, the user-role assignment relations induced by AU QF and by AU QF are the same. By iterating the process, we derive a set of syntactic authorization rules whose conditions are constraints only.

The MS-AU problem

We consider the MS-AU problem (recall its definition at the end of Section 2.2) for RBAC-DR policies with a background theory of the attributes, i.e. given a IF (i2j=unsat AND j2i=unsat) THEN union(i,j) 12:

ELSE S := S∪{(i,j,f1,f2),(j,i,f1,f2)}; 13: ELSE S := S∪{(i,j,f1,f2)} Fig. 1. Solving the MS-AU and CD-SAU problems RBAC-DR family of policies (U, R, P, a, AU QF , P A, RH) with background theory T A of the attribute, the MS-AU problem amounts to checking whether ρ 1 ρ 2 for every pair ρ 1 and ρ 2 of syntactic authorization rules in AU QF .

The key observation is that we can reduce the problem of establishing whether ρ 1 ρ 2 to an SMT(T A ) problem involving the conditions of the rules ρ 1 and ρ 2 . Before being able to formally state this, we need to introduce the following notion. Two rules (α 1 (b 1 ) r 1 ) and (α 2 (b 2 ) r 2 ) are syntactically related if b 1 ∩ b 2 = ∅ (by abuse of notation, we consider the sequence b i as a set, i = 1, 2); otherwise, they are syntactically unrelated. Proposition 2. Let (R, P, a, AU QF , P A, RH) be a RBAC-RD family of policies with background theory T A of the attributes and ρ i = (α i (b i ) r i ) be an authorization rule in AU QF for i = 1, 2. Then, the following facts hold:

(a) if ρ 1 and ρ 2 are syntactically unrelated, then ρ 1 ρ 2 and ρ 2 ρ 1 and (b) if ρ 1 and ρ 2 are syntactically related, then ρ 1

ρ 2 iff α 1 (b 1 ) → α 2 (b 2 ) is T A -valid (or, equivalently, α 1 (b 1 ) ∧ ¬α 2 (b 2 ) is T A -unsatisfiable).
Assuming that the SMT(T A ) problem is decidable, it is possible to automatically check whether a rule is more senior than the other by Proposition 2. This is the idea underlying the algorithm in Figure 1 r[j] are syntactically related. The Boolean function opposite is the constant function false so that the third component of the tuples in S is always set to false (this will be important only when solving CD-SAU problems, see Section 4.3 below). The function find and the procedure union form the interface to a union-find data structure (see, e.g., [START_REF] Tarjan | Efficiency of a Good But Not Linear Set Union Algorithm[END_REF]) to maintain a set of equivalence classes: find(i) returns the representant of the equivalence class to which the rule c[i] r[i] belongs to and union(i, j) merges the equivalence classes to which the rules c[i] r[i] and c[j] r[j] belong to. The function check T A (ϕ) returns sat (unsat, resp.) iff the quantifier-free Σ A -formula ϕ is T A -satisfiable (T A -unsatisfiable, resp.) and it is implemented by invoking an available solver supporting the solution of SMT(T A ) problems.

The algorithm works by enumerating pairs of rules (the two nested loops at lines 2 and 3) to establish whether they are syntactically related (flag f2 line 4). In case they are not, the tuple (i, j, false, false) is added to S (line 13) meaning that the pair (i, j) of rules cannot be compared with respect to . Otherwise, the union-find data structure is queried (line 6) in order to establish if the rules identified by i and j are already in the same equivalence class. If this is the case, the tuples (i, j, false, true) and (j, i, false, true) are added to S (line 12) meaning that both i j and j i. Otherwise, it is checked if i j (line 7, by testing if c[i] implies c[j] modulo T A or, equivalently, the conjunction of c[i] with the negation of c[j] is T A -unsatisfiable) and the tuple (i, j, false, true) is added to S (line 8). The same is done to establish if j i (lines 9 and 10). If both previous tests (lines 8 and 10) have been successful, then the two equivalence classes to which i and j belong to are merged (line 11). The cost of invoking the function opposite is constant (recall that this is a constant function returning false when solving the MS-AU problem) while that of related is linear in a by using bit-strings to represent sequences of variables occurring in the conditions of the rules. The union-find algorithm in [START_REF] Tarjan | Efficiency of a Good But Not Linear Set Union Algorithm[END_REF] takes almost constant (amortized) time for invoking both the find and union operations (more precisely, it takes O(A -1 (N )) where A -1 is the inverse of the Ackermann function; since for any practical values of N , A -1 (N ) is bounded by 5, each invocation to find and union can be considered as constant). Thus, the complexity of the algorithm is clearly dominated by the number of invocations to check T A . Notice that the function is invoked on quantifier-free formulae obtained by conjoining a constraint α i with the negation of a constraint ¬α j (i.e. a clause). This allows us to characterize the complexity of the MS-AU problem. Formally, we introduce the following notion. A theory T is convex (see, e.g., [START_REF] Nelson | Simplification by Cooperating Decision Procedures[END_REF]) iff whenever a constraint implies a clause, it also implies one of the literals in the clause. Examples of convex theories are EU F, ED, LAR, and RDL whose we call) CD-SAU problems by using description logic and tableaux reasoners, respectively, are described. Neither a complexity characterization nor an extensive experimental evaluation are proposed and the techniques do not support rich background theories of the attributes as we do here. The policy specification languages in [START_REF] Yuan | Attributed Based Access Control (ABAC) for Web Services[END_REF][START_REF] Li | RT: A Role-based Trust-management Framework[END_REF] can express authorization policies with attributes. They support policies that go beyond those considered in this paper but do not propose automated techniques for detecting inconsistencies and redundancies as we do here. Furthermore, they adopt a closed (deny-by-default) policy model (where access is allowed if there exists a corresponding (positive) authorization and is denied otherwise [START_REF] Jajodia | Flexible support for multiple access control policies[END_REF][START_REF] Samarati | Access control: Policies, Models, and Mechanisms[END_REF]) rather than an open (allow-by-default) policy as we do in this paper. We leave it to future work the study of the impact of using a closed policy model on the decidability and complexity of the MS-AU and CD-SAU problems. We notice that our framework (including Theorems 1 and 2) can be easily extended to cope with conditions about the environment (e.g., time of the day) as done in [START_REF] Yuan | Attributed Based Access Control (ABAC) for Web Services[END_REF].

Several works [START_REF] Shaikh | Inconsistency Detection Method for Access Control Policies[END_REF][START_REF] Adi | Typing for Conflict Detection in Access Control Policies[END_REF][START_REF] Mankai | Access Control Policies: Modeling and Validation[END_REF][START_REF] Hughes | Automated Verification of Access Control Policies Using a SAT Solver[END_REF][START_REF] Fisler | Verification and change-impact analysis of access control policies[END_REF][START_REF] Autrel | MotOrBAC 2: a security policy tool[END_REF][START_REF] Lin | EXAM: a comprehensive environment for the analysis of access control policies[END_REF] have proposed techniques to detect inconsistencies and redundancies in XACML or extensions of RBAC policies by leveraging a variety of verification engines. None of these works provides decidability and complexity results of the analysis techniques as we do in this paper.

  is a condition C on a subsequence b = b 1 , ..., b m of a (i.e. for each b j there exists a k such that b j = a k for j = 1, ..., m, k = 1, ..., n, and m ≤ n), also written as C(b), where C is a sub-set of D b1 ו • •×D bm . A (rule-based) authorization rule is a pair (C(b), r), also written as C(b) r, such that C(b) is a condition and r is a role in R. The attribute-role relation AR associated to the set AU of authorization rules is {({(b 1 , e 1 ), ..., (b m , e m )}, r) | (C(b 1 , ..., b m )

  17 and c ∈ {Italy, France, ...}} Teen, and ρ4 : {(a, c) ∈ N × WC |a ≤ 12 and c ∈ {Italy, France, ...}} Child

  Input: c: array[0..N-1] of constraints r: array[0..N-1] of (signed) roles 1: S := ∅; 2: FOR i=0 TO N-2 DO 3: FOR j=i+1 TO N-1 DO 4: f1 := opposite(r[i],r[j]); f2 := related(c[i],c[j]) 5: IF f2 THEN 6:IF find(i) =find(j) THEN 7:i2j := checkT A (c[i] ∧ ¬ c[j]) 8:IF i2j=unsat THEN S := S∪{(i,j,f1,f2)}; 9:j2i:= checkT A (c[j] ∧ ¬ c[i]) 10:IF j2i=unsat THEN S := S∪{(j,i,f1,f2)}; 11:

  for automatically solving the MS-AU problem. Let (R, P, a, AU QF , P A, RH) be a RBAC-RD family of policies with background theory T A where |AU QF | = N. The input to the algorithm are two arrays c and r such that for each rule α r in AU QF there exists i in the range [0..N-1] such that c[i] = α and r[i] = r (the latter will contain signed roles only when solving CD-SAU problems, see Section 4.3 below). The variable S ⊆ [0, N -1] × [0, N -1] × {true, false} × {true, false} stores increasingly precise approximations of the relation in a sense to be made precise below. The Boolean function related(c[i], c[j]) returns true iff the rules c[i] r[i] and c[j]

Lemma 1 .

 1 Let (R, P, a, AU QF , P A, RH) be a family of RBAC-RD policies with background theory T A of the attributes whose SMT(T A ) problem is decidable and |AU QF | = N. Then, the following facts hold after the execution of the algorithm in Figure1: (a) (i, j, false, true) ∈ S iff c[i] r[i] c[j] r[j], (b) find(i) = find(j) iff c[i] r[i] c[j] r[j] and c[j] r[j] c[i] r[i],i.e. the union-find data structure stores the equivalence classes of the "more senior than" relation over AU QF , and (c) the number of invocations to check T A is at most N(N -1).

This condition is not restrictive as it is always possible to add a constant ce for each element e in the domain whose interpretation is e itself. The addition of these constants does not change the set of satisfiable quantifier-free formulae (see, e.g.,[START_REF] Enderton | A Mathematical Introduction to Logic[END_REF]).

The sources of the program used to perform the experiments are available at http: //st.fbk.eu/SilvioRanise#Papers.

Acknowledgements. This work was partially supported by the "Automated Security Analysis of Identity and Access Management Systems (SIAM)" project funded by Provincia Autonoma di Trento in the context of the "team 2009 -Incoming" COFUND action of the European Commission (FP7).

constraint satisfiability problem is polynomial (convexity of LAR derives from the convexity of linear algebra). Instead, both LAI and its sub-theory IDL are not convex (e.g., x ≥ 0 ∧ x ≤ 1 ∧ ¬(x = 0 ∧ x = 1) is LAI-unsatisfiable but neither x ≥ 0 ∧ x ≤ 1 ∧ x = 0 nor x ≥ 0 ∧ x ≤ 1 ∧ x = 1 is LAI-unsatisfiable).

Theorem 1. If the SMT problem of the background theory T A of the attributes is decidable, then the MS-AU problem is decidable. If furthermore T A is convex and the constraint T A -satisfiability problem is polynomial, then the MS-AU problem is also polynomial.

When the background theory of the attributes is EQ, LAR, RDL, or we consider composite constraints of these theories, the MS-AU problem is decidable and polynomial since all these theories are decidable and polynomial (see Section 3). When the background theory of the attributes is ED, LAI, or IDL, the MS-AU problem is decidable and NP-complete. While this is obvious for ED and LAI (whose constraint satisfiability problem is already NP-complete), it is less so for IDL since its constraint satisfiability problem is polynomial. Since IDL is not convex, the problem of checking the satisfiability of a constraint with a clause becomes NP-complete [START_REF] Lahiri | An Efficient Decision Procedure for UTVPI Constraints[END_REF]. Thus, besides polynomial constraint satisfiability, convexity is crucial to have a polynomial MS-AU problem.

The CD-SAU problem

We consider the CD-SAU problem (recall its definition at the end of Section 2.3) for RBAC-NDR policies with a background theory of the attributes, i.e. given a RBAC-NDR family of policies (R, P, a, AU QF , P A, RH) with background theory T A of the attributes, the CD-SAU problem amounts to checking whether for each signed authorization rule α 1 (b 1 ) +r in AU QF , there is no rule α 2 (b 2 ) -r in AU QF such that a user u satisfies both α 1 (b 1 ) and α 2 (b 2 ) under some userattribute mapping s. We say that there is a conflict between rule α 1 (b 1 ) +r and α 2 (b 2 ) -r if there exists a user u satisfying both α 1 (b 1 ) and α 2 (b 2 ) under some user-attribute mapping s. Interestingly, it is possible to distinguish two types of conflicts depending on the fact that the rules can or cannot be compared by the "more senior than" relation. Formally, the rules ρ 1 and ρ 2 are relevant iff ρ 1 ρ 2 or ρ 1 ρ 2 , and are irrelevant otherwise. If two rules are syntactically unrelated, they are also irrelevant by Proposition 2 (a).

We solve the CD-SAU problem by using again the algorithm in Figure 1 where the array r stores signed roles, the auxiliary function opposite(r[i], r[j]) returns true iff r[i] = +r and r[j] = -r or r[i] = -r and r[j] = +r, and all the other data structures and functions are as described in Section 4.2. As anticipated in Section 4.2, the third component of the relation S is important and distinguishes between relevant and irrelevant pairs of rules.

As before, the algorithm enumerates pairs of rules and establishes whether they have signed roles +r and -r and they are syntactically related (flags f1 and f2 at line 4, respectively). In case the two rules are not syntactically related, the tuple (i, j, f 1 , false) is added to S (line 13) meaning that the rules identified by i and j are irrelevant and there is a conflict between them when f 1 is true.

Otherwise, the union-find data structure is queried (line 6) in order to establish if the rules identified by i and j are already in the same equivalence class. If this is the case, the tuples (i, j, f 1 , true) and (j, i, f 1 , true) are added to S (line 12) meaning than the rules identified by i and j are relevant and there is a conflict between them when f 1 is true.

r[j] (line 7) and the tuple (i, j, f 1 , true) is added to S (line 8), the same is done to establish if c[j] r[j] c[i] r[i] (lines 9 and 10): the rules are relevant and there is a conflict between them when f 1 is true. If both previous tests (lines 8 and 10) have been successful, then the two equivalence classes to which i and j belong to are merged (line 11).

Lemma 2. Let (R, P, a, AU QF , P A, RH) be a family of RBAC-NDR policies with background theory T A of the attributes whose SMT(T A ) problem is decidable and |AU QF | = N. Then, after the execution of the algorithm in Figure 1 the following holds: if (i, j, τ, true) ∈ S, then there is a conflict between rules i and j and the two rules are relevant (irrelevant, resp.) when τ is true (false, resp.) and the number of invocations to check T A is at most N(N -1).

We state the second main result of the paper.

Theorem 2. If the SMT problem of the background theory T A of the attributes is decidable, then the CD-SAU problem is decidable. If furthermore T A is convex and the constraint T A -satisfiability problem is polynomial, then the CD-SAU problem is also polynomial.

Experiments

To test the practical viability of our techniques, we have implemented the algorithm of Figure 1 in C. To implement check T A , we have chosen Yices [31] for its easy-to-use API, although many other state-of-the-art SMT solvers (e.g., Z3 [34]) can be used. We have also implemented a generator of synthetic MS-AU problems; we expect similar performances on CD-SAU problems since the algorithm of Figure 1 can solve also these problems with minimal variations. The starting point is the policy of Example 1. The idea is to randomly generate composite constraints for the conditions of the rules taken from an enumerated data-type theory ED({v 1 , ..., v V }, E) and IDL: the former corresponds to the set of countries in the world and the latter to the age of users. We randomly generate composite constraints whose literals are e = v i , e = v i (for i ∈ {1, ..., V }), a = k, a > k, and a < k (for k ∈ Z) where e and a are variables of sort E and Z, respectively. According to Theorem 1, the resulting MS-AU problem is NP-complete as the constraint ED-satisfiability problem is NP-complete and that of IDL is polynomial but IDL is not convex. Thus the invocations to check T A can be computationally expensive. The random generation of literals in the composite constraints is inspired to Gorrilla [START_REF] Korovin | GoRRiLA and Hard Reality[END_REF] that is known to generate difficult problems for many state-of-the-art SMT solvers. The method of [START_REF] Korovin | GoRRiLA and Hard Reality[END_REF] has been adapted to satisfy assumption (A1) of Section 4.1 and to generate constraints that can be considered as "realistic" conditions of authorization rules, i.e. roughly similar to those in Example 2.

There are three inputs to the benchmark generator: the number V of values of ED, a positive integer M bounding the constant k occurring in the arithmetic literals, and the number N of conditions to be considered. The first two parameters V and M have negligible influence on the performance of our implementation of the algorithm in Figure 1. As a consequence, Figure 2 shows the plot of the time taken to solve an MS-AU problem for the last parameter, i.e. an increasing number N of rules (ranging from 100 to 1,000). 4 The behaviour of the algorithm is clearly quadratic. This is possible because we invoke the SMT solver only (around) 1/4 of the potential N 2 calls, thanks to the notion of two rules being syntactically unrelated (see before Proposition 2 for the definition) and the use of the union-find data structure that provides us with a computationally cheap method to deduce the transitive chains of the "more senior than relation." We believe that this gives a first important evidence of the practical viability of our technique.

Related work and Discussion

The problem of combining RBAC with more flexible methods of assigning users to roles has been considered several times (see, e.g., [START_REF] Lupu | Reconciling Role Based Management and Role Based Access Control[END_REF][START_REF] Ardagna | Expressive and Deployable Access Control in Open Web Service Applications[END_REF]). In this line of work, to the best of our knowledge, no automated analysis technique has been proposed to assist designers to detect redundancies and inconsistencies of policies as we do here. We have presented an abstract rule-based framework for the integration of attributes in RBAC inspired to [START_REF] Al-Kahtani | A Model for Attribute-Based User-Role Assignment[END_REF]. The MS-AU and the CD-SAU problems are inspired to problems informally characterized in [START_REF] Al-Kahtani | Induced Role Hierarchies with Attribute-Based RBAC[END_REF] and [START_REF] Al-Kahtani | Rule-based RBAC with negative authorization[END_REF]. The idea of using SMT solvers for their efficient solution together with their decidability and complexity results are new; except for [START_REF] Armando | Automated Symbolic Analysis of ARBAC Policies[END_REF][START_REF] Alberti | Efficient Symbolic Automated Analysis of Administrative Role Based Access Control Policies[END_REF] that exploit SMT solvers to solve administrative RBAC problems. In [START_REF] Yu | Research on Description Logic Based Conflict Detection Methods for RB-RBAC Model[END_REF][START_REF] Kamoda | Access Control Policy Analysis Using Free Variable Tableaux[END_REF], techniques to solve (what