docs: I finally understand why a formal policy language is helpful

1 files changed, 50 insertions, 2 deletions

diff --git a/doc/share/authz/ReBAC.md b/doc/share/authz/ReBAC.md
index b62bd7f..ee82ba2 100644
--- a/doc/share/authz/ReBAC.md
+++ b/doc/share/authz/ReBAC.md
@@ -28,7 +28,7 @@ essentially formulating the following policy: `grant p to user u if R(u)`.
 
 PriMA is another recently proposed privacy protection mechanism for SNSs.
 
-Policy
+## Access Control Policies
 
 Let `U` be the set of all users in the system.
 Accesses are directed against resources. A resource may represent one or more
@@ -47,7 +47,9 @@ relationship with the owner in order be granted. Huh?
 Associated with every resource is an `access control policy`.
 Policy is modeled as a ternary predicate: `U x U x G(U, I) => {0, 1}`.
 
-A protection system N is a 7-tuple (I, U, R, C, C0, policy, owner) where:
+## Protection System
+
+A protection system `N` is a 7-tuple `(I, U, R, C, C0, policy, owner)` where:
 
 * `I` is the set of relation identifiers (See my question in the README about resource identifiers in our system)
 * `U` is a finite set of users in the system
@@ -57,6 +59,52 @@ A protection system N is a 7-tuple (I, U, R, C, C0, policy, owner) where:
 * `R => PP(U, I)` assigns a policy predicate to every resource in the system. (This means that every resource is addressable through a universal identifier, right? Goodbye `bigint`? Yay!)
 * `owner: R -> U` is a function that assigns an owner to every resource in the system.
 
+Where the access control policy of a resource comes from doesn't matter. The
+possibilities are:
+
+1. Mandatory: Some policies are mandated by the system administrator
+1. Discretionary: The resource owners are responsible for specifying their
+   access control policies
+1. Policy Vocabulary: A set of policy predicates from which users take their
+   picks. (friends, friends-of-friends)
+
+## Protection State
+
+Given a protection system `N = {I,U,R,C,C0,policy,owner}`, a protection state is
+a triple `{C,sn,extends}` composed of the following elements:
+
+* `C`: is the set of active contexts in the state. This set is infinite and
+  non-empty.
+* function `sn : C -> G(U,I)` that maps each context of the state to a social
+  network `sn(s)` records the relationships that have been articulated in
+  context `c`.
+* `extends ~= C x C` is a binary relation defined over `C`, such that:
+  * a: the directed graph is a tree
+  * b: `c0` is the root of the tree
+  * c: if `(c1,c2) ~= extends` then `c1` is the child of `c2` in the tree. The
+    extends relationship defines a **context hierarchy**.
+
+## Authorization
+
+Authz is achieved by consulting relationships in a social network. Authorization
+decisions are made primarily by consulting the relationship between accessor and
+the owner. In a real implementations, it is possible for the system to have a
+hybrid authorization scheme that is both relationship based and role based.
+
+Relationship inheritance allows relationships articulated in ancestor contexts
+to be inherited by the effictive social network of descendant contexts. The
+social network of a child context contains no less relationships than that of a
+parent context.
+
+## Policy Language
+
+It is desirable to have a policy language for specifying ReBAC policies.
+
+A policy language facilitates:
+
+1. the specification of composite policies, which in turn forms the basis of trust delegation.
+1. **the static analysis of policies and system configuration.**
+
 ## See also
 
 * [Relationship-Based Access Control: Protection Model and Policy Language by Philip W. L. Fong](https://cspages.ucalgary.ca/~pwlfong/Pub/codaspy2011.pdf)