In a collaborative distributed environment, users own a set of private resources that they possibly share with each other to achieve mutual advantages. The access to resources is regulated by a policy de ned by each user in isolation, and independently of the others. However, typical access control languages allow de ning policies that only check the roles or the attributes of the requesters and resources. But they do not impose a fair exchange of access grants by taking into account what requesters o er to others. Here, we present MuAC, a logic-based access control language designed for expressing mutuality. In particular, MuAC allows specifying conditions on what requesters must o er in exchange for using a particular resource.
Here, we start to address the mutuality issue and propose MuAC, a logic-based access control language. This language not only allows specifying conditions on the resource and users, but also constraints on what requesters must o er in exchange. We claim that MuAC naturally expresses situations in which mutuality has involved forms.
Even though policies are exclusive of each user, they impact on each other. For example, consider the case of picture sharing mentioned above: Alice needs to be aware of Bob's policy for granting him access to her pictures. In general, deciding an access request may require a complete knowledge of the policies of every user. Here, we assume a centralized evaluation model where each user separately de nes his local policies and sends them to the policy enforcement point (PEP), responsible for the evaluation of the requests and the interactions among users.
Mutuality may however induce circularity while evaluating access requests. Consider again picture sharing and assume that the PEP receives from Bob a request to watch Alice's pictures. If Bob unconditionally allows Alice to watch his, then there is no circularity and Bob's request is accepted. A circularity instead occurs if Bob allows Alice to watch his picture only if she shares her pictures with him. Nevertheless, the PEP should grant Bob access to Alice`s pictures, and viceversa.
Unfortunately, classical logic is not fully adequate to express this situations, which are
typical of common contracts. To overcome this limitation, an e ective predicative contractual
logic (PCL) was introduced in [
We therefore exploit PCL to resolve circularity arising in mutual access policies. More in
detail, the PEP translates the policies of the users into a conjunction of PCL formulas, and relies
on teh deductive machinery of [
Plan of the paper Section 2 gently introduces MuAC and its features through a running example. Section 3 brie y reviews the logic PCL. Section 4 presents the syntax and the semantics of MuAC ; discusses its expressive power through a bunch of examples; and describes the algorithm implementing a centralized PEP for request evaluation. Section 5 compares our proposal with the literature, and draws some conclusions and future work. 2
Consider a computer science department with several research group on di erent areas. Each group has a nite amount of resources, some of which may be shared to enhance cooperation and to optimize their usage. Sharing however is not always for free, and each research group wants something in return for allowing a fair access to its resources, while avoiding free raiders and guaranteeing mutuality of the bene ts. In other words, each researcher should be enabled to decide which resources to share and with whom, and which guarantees to require, so giving rise to an access policy. We here o er a formal language for specifying individual policies, independently of each other. The task of the automatic access control system we propose is to combine these policies together and enforce them on all the involved entities.
We now informally describe the department; then we intuitively present possible individual policies and their formalization in a simpli ed form; and nally we discuss how the individual policies are combined to control accesses.
There are three research group inside the department: machine learning, consisting of Mark, Michelle and Morty; networks, including Nick, Nancy and Neil; and security, with Selene and Sam. Resources are of di erent kinds, e.g. computational power, data, software, picture.
Table 1 describes what researchers require (line wants), what they o er (line shares) and under which conditions (line with). For example, Morty (i) looks for picture and o ers in exchange computational power, provided that who requires it shares something with him, in this case pictures; moreover, he (ii) o ers for free his software. Nick o ers pictures and post, under the condition that the requester is in his group of shares something with its member, and wants computational power. Selene instead requires both network software and source code and o ers network logs to the members of her group who share something with her, or also to a member who shares something with someone sharing with her (a sort of transitive sharing).
More formally, the case (i) of Morty's policy is rendered by the following rule computational-power(Resource); Allows(Me; r; Subject) (1) where the rst predicate is true when the resource requested is of kind computational power. The predicate Allow is typical of our policy language and is the key one. It has three arguments: the rst is the individual who decided the policy, here Me is Morty; the second argument is the resource requested by Morty; and the last one says that r is owned by Subject (note that the check that the type of r is picture is completely demanded to the access control manager). Intuitively, Allow evaluates true when Subject permits Me to access r. But this cannot be established without inspecting the individual policy of Subject.
The case (ii) of Morty's policy, i.e. he shares his software with everyone, is easier: software(Resource)
As expected, Morty and Nick can share some of their resources. Indeed, the relevant portion of Nick's policy is rendered the following formula: pictures(Resource); Allows(s; r; Subject); Networks(s) (2) Note that the third predicate constrains Morty to share something with a member of the Networks group, here Nick himself. The sharing between Morty and Nick can only take place if both (1) and (2) hold. This happens when in the rules (1) Me stands for Morty; Subject is bound to Nick; and r to a picture P o ered by Nick. (2) s is bound to Nick; Subject stands for Morty; and r is bound to computational power
CP o ered by Morty.
As mentioned above, the predicate Allows plays a key role and deserves a non standard
treatment. Indeed, in order to prove that Allows(Morty, P, Nick) holds, we need to show that
Allows(Nick, CP, Morty) holds, and viceversa so leading to a circularity. To break it safely, we
exploit the contractual implication of Propositional Contract Logic [
Bartoletti e Zunino introduced in [
The main aspect of contract logic is its ability of dealing with the circularity arising when p is veri ed if q is as well and vice versa, formally (p q) ^ (q p). In contrast with common implication, here the result is that both the formulas are veri ed. This handshake property is formally stated as
` (p q) ^ (q p) ! p ^ q Of course, circularity may involve many steps, rather than the two considered above.
Contractual implication satis es transitivity ` (p q) ^ (q r) ! (p r)
A further natural property is that promises in contracts can be arbitrarily weakened, while the precondition can be arbitrarily strengthened. Intuitively: if I am willing to grant you something in change of something else, then I am also willing to give you less for getting more: (p q) ^ (q ! q0) ! (p q0) (p0 ! p) ^ (p q) ! (p0 q)
Finally, a contract should be satis ed also when the premise is unconditionally satis ed, and if a promise q is already true, then it is also true any contract which promises q ` p ^ (p q) ! q ` q ! (p q)
The propositional intuitionistic logic has been proved decidable. The theorem prover of [
The MuAC
Our model considers a system hosting a nite set U of users (ranged over by u; u0; ui) that protect and use a nite set R of resources (ranged over by r; r0; ri) of various kinds. Each user chooses how to regulate accesses to his resources by specifying a set of rules, describing the conditions under which access is granted to another user, called Subject. Although the speci cation of access rights is fully demanded to each users, their enforcement results from the combination of these individual policies and a centralized entity grants or denies access, upon receiving a request.
Policy speci cation A rule 2 contains atomic propositions on users and resources, and possibly the special predicate Allows. We assume a set of user variables u; u0 : : : ; a set of resource variables r; r0 : : : ; three special variables Me; Subject; Resource that take value when used (Me indicates the owner of the rule, Subject the requester and Resource has the obvious meaning); and a set of atomic predicates p; q; p0; q0 : : : Let U range over Me, Subject and user variables; and let R range over Resource and resource variables. Rules are de ned as follows ::= p(U ) j p(R) j Allows(U; R; U ) j ; The intended meaning of a rule is that Me grants Subject access to Resource if all the predicates occurring in are proved true, possibly involving circularity.
Atomic predicates express properties of users and resources that are meaningful in the overall system. E.g., software(Resource) in Morty's policy holds true if the requested resource is a piece of software. The predicate Allows(U; R; U 0) states the condition that the user U is allowed by user U 0 to access resource R. An example is the formula Allows(Me; r; Subject), occurring in the rule (1) of Morty's policy. The comma is the standard logical conjunction. We assume that all the variables are existentially quanti ed, except for the special ones. See for instance the discussion at the end of Section 2, where the rule (2) of Nick's policy pictures(Resource); Allows(s; r; Subject); Networks(s) was shown to hold for speci c values of the variables s and r.
Finally, the centralized granting authority collects all the rules in a con guration, i.e. a mapping from users to sets of rules : U ! 2 .
Expressivity Despite the simplicity of the examples considered, MuAC allows a user to de ne involved policies, some of which we discuss below.
In the simplest kind of rule, its owner, i.e. Me, o ers a resource to the requester, i.e. Subject provided that in exchange it shares some (other) resource. This is the case (of a portion) of Sam's policy (3) as intuitively de ned in Table 1 speaking both of code, and of Morty's (4) where the exchanged resources are of di erent nature: source-code(Resource); Allows(Me; r; Subject); source-code(r) source-code(Resource); Allows(Me; r; Subject); picture(r) Of course, more than one resource can be requested. For example Me o ers network logs to those who are willing to share both network software and computational power: network-log(Resource); Allows(Me; r; Subject); Allows(Me; r0; Subject); network-software(r); computational-power(r') (3) (4) Note that to o er k sorts of resources, one has to write k distinct rules.
A second kind of rules considers groups of users rather than a single one: Me o ers a resource to a member of a group, provided that (another) member gives something in exchange. The following example says that Me o ers computational power to the security group members if any of them shares some source code with him computational-power(Resource); Allows(Me; r; u); source-code(r); security(Subject); security(u) Also the converse is possible, when the shared resource is for a member of the group of Me (see also the rule 2): computational-power(Resource); Allows(u; r; Subject); networks(u); networks(Me); computational-power(r)
So far a single Allow occurred in the rules. When there are more, we obtain a sort of transitivity of o ers and requests. A simple example follows where all the resources are code, r belongs to Subject and r0 to the user u. Intuitively, the rule says that Me grants Subject access to Resource if Subject o ers r to u, who in turn o ers r0 to Me: source-code(Resource); Allows(u; r; Subject); Allows(Me; r0; u); source-code(r); source-code(r0) Of course this form of transitivity may involve arbitrary chains of Allow, as in the rule below, where the second Allow is only applied to variables: source-code(Resource); Allows(u; r; Subject); Allows(u0; r0; u); Allows(Me; r00; u0); source-code(r); source-code(r0); source-code(r00) (5)
A special form of (multi-user) cooperation is also expressible, illustrated by the following rule. Subject is granted access to the picture Resource by Me, if both Me and Subject o er to u some source code (r0 and r, resp.):
picture(Resource); Allows(u; r; Subject); Allows(u; r0; Me); source-code(r); source-code(r0)
Policy meaning The semantics of our language is de ned by giving meaning to con
gurations. This is done by rst translating a con guration to a nite set of contract logic
propositions [
We assume that PEP knows which are the resources each user handles, R"u, and those he wants, R#u. Also, we assume that this authority can evaluate the atomic predicates appearing in the rules.
We associate with a given con guration the PCL theory with propositions de ned through the inference rule below, for all s; u 2 U ; r 2 R; 2 (u); : (U ! U ) [ (R ! R) Allow[ ]
Allows(s; r; u) 2 if and only if constraints[ ] ^ (Me) = u ^ (Subject) = s ^ (Resource) = r 2 R"u \ R#s ^ 8 predicate Allows(s0; r0; u0) occurring in Allow[ ]; it is r0 2 R"u0 \ R#s0 where Allow and constraints are the conjunctions of all the instances of the predicate Allows and of the instances of atomic predicates in , resp., and [ ] extends homomorphically .
A few comments are in order. The ground substitution binds in all possible ways the resource and user variables, so to evaluate the atomic predicates in , except then the special one Allow. The predicate constraints[ ] holds true whenever maps the variables to users and resources that satisfy the relevant predicates in . Furthermore is required to bind in the contractual implication the special variables Me to the actual owner u of the access rule , and Subject, Resource to the user s and the resource r, belonging to u and requested by s. In addition, all the resources r0 occurring in a predicate Allows(s0; r0; u0) should belong to u0 and be wanted by s0, as well. If all the above holds, Allow[ ] Allows(s; r; u) is a formula of . Policy and request evaluation The Algorithm 1 implements the declarative construction of a PCL theory of the previous paragraph. It presents the function TRANSLATE-INTO-PCL that given a con guration processes each rule therein by computing the legal substitutions such that the instantiated atomic predicates evaluate to true. Finally, it collects the obtained formulae into the theory .
The PEP executes Algorithm 2 that receives the policies from the users and builds a
conguration . Then it translates into a PCL theory , using Algorithm 1, and starts serving
requests from the users. When the user s tries to access a resource r, his query asks(s,r) is
transformed into the formula Allows(s; r; u), where u is the owner of r. Finally, the enforcement
and decision point checks if the theory entails this formula, i.e. ` Allows(s; r; u), and replies
accordingly. The proof of the entailment is demanded to the deduction system of PCL [
It is worth noting that the order in which the access rules are speci ed is immaterial, because the semantics transforms them in the logical theory . Also, there are neither rules explicitly denying accesses, nor constraining requests to be denied. Consequently, there are no con icts, in logical terms contradictions, and a permission is granted only when entails the query. 5
We have de ned MuAC, a control access language for a distributed collaborative environment.
Its main feature concerns expressivity, as it permits to de ne and handle access requests that
demand mutual agreement between several users. To resolve the circularities that may arise
with this form of mutuality we resorted to the propositional contract logic PCL [
For the time being, MuAC has the grant accept only. We plan to extend the language with deny rules, which also require to address the resolution of potential con icts. A further extension is allowing rules in which a user speci es resources that must not be shared. For example, Alice permits Bob to access her pictures, provided that Bob does not share anything with Charlie. This kind of negative requirement is the rst step towards the de nition of policies regulating con icts of interest. Finally, we plan to study the relationship between MuAC and languages for trust negotiation and the security properties that our language can o er when some users misbehave.
Related work Access control is a wide sudied eld, surveyed by many papers, e.g. [
Input: Con guration : U ! 2 Output: PCL theory function Translate-into-PCL( )
; for all users u 2 U and rules 2 (u) do for all user variable ui appearing in do
Ui set of users that verify every atomic predicates p(ui) in for all resource variable ri appearing in not appearing in any Allows do
Ri set of resources that verify every atomic predicates p(ri) in for all users s 2 U that verify all the predicates over Subject in and resources r 2 R"u \ R#s that verify all the predicates over Resource in 0Allow AllowfMe 7! u; Subject 7! s; Resource 7! rg for all u1 2 U1 : : : un 2 Un and r1 2 R1 : : : rm 2 Rm do 0Allow 0Allowfu1 7! u1 : : : un 7! ung 0Allow 0Allowfr1 7! r1 : : : rm 7! rmg for all resource variables r0i such that
Allows(us; r0i; uo) occurs in for some us and uo do
Ri0 subset of R"uo \ R#us that verify the predicates p(r0i) in return for all r10 2 R10 : : : rk0 2 Rk0 do 0Allow 0Allowfr01 7! r10 : : : r0k 7! rk0g [ ( 0Allow Allow(s; r; u)) do
for all users u 2 U do (u) receive-from(u)
Translate-into-PCL( )
while true do
asks(s; r) receive-from-any(s 2 U )
u owner(r)
check PCLprover( , Allows(s; r; u))
if check then send-to(s, Grant)
else send-to(s, Deny)
. through Algorithm 1
. checks if
` Allows(s; r; u)
they own. In this environment, a main issue is the combination of individual policies. To
the best of our knowledge, no proposals address mutuality, but only focus on the resolution
of con icts [
Mutuality plays a main role also in trust negotiation, a process that permits a safe interaction
between two parties that do not trust each other [