[Odrl-version2] Reasoning about an Agreement

[Vicky Weissman]

Hello,

A few months ago, I told Renato that I would try to address the question "how
do we determine whether an action is permitted/forbidden by an agreement".
I'm sorry it has taken me so long to do this.

To start the discussion, consider an agreement A that does not include a
prohibition or duty.  We can rewrite the agreement as a set S of statements,
each of the form "if constraints c1, ..., cn hold then user u may do action a
to asset s" (e.g., if Alice has made less than 5 copies of file f and today's
date is before Aug, 31, 2005, then Alice may make a backup of f).  For
brevity, I'll write these statements as "c1 AND... AND cn => Perm(u, a, s)".
The Model Semantics doc (dated May 16, 2005) seems to say that two statements
in S can only differ on their action element.  In other words, every
statement in S includes the same constraints, user, and asset.  This doesn't
make sense to me, so I'm going to assume the statements can refer to
different constraints, users, and assets.  If I'm wrong, then I've simply
answered the question for a more general problem.  (As an aside, I think
different statements in S can have different constraints if you modify the
existing model so that constraints can be in "and" and "or" containers.)  

Suppose we want to determine if the statements in S imply that Alice is
permitted to copy a file f.  A naïve approach, call it ProcN, is to find the
set T of statements that are in S and have the form "c1 AND... AND cn =>
Perm(Alice, copy, f)".  For each t in T, check if the constraints hold.  (I'm
assuming constraint checking is fairly straightforward.  If the constraint
includes a status element, the check should be trivial; otherwise, I imagine
a database query of some sort would determine if the constraint held.)  If
all of the constraints in a t in T hold, then we say Alice is permitted to
copy file f; otherwise, we say the permission is not explicitly granted by A.

That's the obvious approach.  What could go wrong?  One problem is that we
need to be a bit careful about encoding S from A.  Suppose that A gives a
group g permission to do an action a to an asset s provided that the
forEachMember constraint holds.  This means that every member of g may do a
to s.  So we want S to include Perm(u, a, s) for every member u of g, rather
than "forEachMember => Perm(g, a, s)".  If g is a large group or its members
are not known, then we can use variables and modify ProcN accordingly.  

Another problem is that ProcN might not give the intuitively correct answer
if S contains two statements whose constraints, roughly speaking, cancel out.
For example, suppose S includes the statements "if Alice has made less than 5
copies of h, she is permitted to copy f" and "if Alice has made at least 5
copies of h, she is permitted to copy f".  Then we should conclude that Alice
may copy f, even if we don't know how many times she's copied h.  (This is
because we know she either copied h less than 5 times or at least 5 times
and, in either case, she's allowed to copy f.)  This is not the answer
produced by the naïve algorithm.  Joe Halpern and I have outlined an
alternative approach in "Using First-order Logic to Reason about Policies".
The conference version is online and the journal version, which is
significantly better, is almost done (please ping me if you want an
almost-finished copy).  If you want to consider the approach seriously, but
don't want to wade through a paper written for logicians, I can summarize the
paper by giving pseudocode for answering queries and a few restrictions that
guarantee the algorithm is relatively efficient.  (I need to think a bit
about how to do this for ODRL, but I'm fairly confident that I can.)
Alternatively, we could decide that the 2 statements alone do not imply that
Alice may copy f.  In general, we could define an agreement so that a
permission is granted only if it follows from a single statement.  If we do
this, then the naive strategy for answering queries will give the correct
answer according to the definition, but I don't think it gives the
intuitively correct answer.  A similar option is the one taken by XACML; each
statement is considered individually but the parties decide how to interpret
the results (e.g., a permission could be granted if it follows from a single
statement, if it follows from at least 3 statements,...)  

We can easily modify the above discussion for agreements that have
Prohibitions, rather than Permissions.  But what if an agreement has both?
Then we need to handle inconsistencies; that is, when a user is both
permitted and forbidden to do an action to an asset.  Probably the easiest
solution is to restrict agreements so this can't happen.  Alapan recommended
an approach in this category by suggesting that agreements are redefined so
that an agreement cannot have both a Permissions and a Prohibitions entity.
That will work, but it seems a bit drastic.  Alternatively, we could require
that the same action name does not appear in both the Permission and the
Prohibition.  Another option is to require that, if the same action name
appears in both, then the corresponding constraints cannot simultaneously
hold.  For example, an agreement A could say "Alice may copy f if she has
made less than 5 copies of f" and "Alice may not copy f if she has made at
least 5 copies of f", because Alice cannot satisfy both constraints
simultaneously.  It should be fairly easy to build an app that checks if an
agreement might be inconsistent and warns the parties accordingly.  

Best,
Vicky