Index: doc/design
===================================================================
--- doc/design	(revision 530866097ef90b6467f0129fb8b74d4d69b160c8)
+++ doc/design	(revision 3529e2da4cef27a733e0bc598417b0a1cbff8479)
@@ -89,4 +89,275 @@
     - query whether a principal has a given role
 
+RT2
+
+RT2 is an more expressive logic than the original RT0 logic that ABAC
+supported.
+
+The RT2 specification extends the existing RT0 notation in 5 ways:
+
+	* More general principal specification to allow room for other
+	  identity providers
+	* Explicit syntax for specifying RT2 objects
+	* Explicit type information to differentiate roles and o-sets.
+	* Explicit type information for RT1 and RT2 parameters
+	* Syntax for constraints
+
+These additions make the syntax both much less terse and much less
+ambiguous. 
+
+A few words about RT1 and RT2 before we describe syntax.  RT1 parameterizes
+roles, that is, it attaches ordered, typed data to roles.  It also adds
+matching requirements to role derivations, including constraints.  The
+RT1 rule
+
+A.r(?x, ?y) <- A.s(1, ?y:[1..3]) & A.t(?y, ?x)
+
+requires that all instances of ?x and ?y on the right side have the same
+type and that the constraints on ?y in the first term are valid for that
+type.  There's no explicit typing in the rule notation of the papers,
+which this specification addresses.
+
+The data types in the papers inlcude integers, floats, dates, closed
+enumerations, and open enumerations.  Closed enumerations are things
+like C or C++ enums, with boolean being a specific example.  Open
+enumerations include things like principals.  For tractability we're
+going to want to define a specific set of data types, which we do
+below.
+
+RT2 allows principals to label data in the same way that they label
+principals.  The ABAC authors helpfully use the exact same syntax for
+assigining a label to a data object as they do for assigning a role to a
+principal, but the semantics are slightly different.  We add syntax
+that clarfies when data is being labelled and when principals are being
+labelled.  These "data roles" are called o-sets.
+
+On with the specification, from the basic chunks up to rules.
+
+Principal Names
+
+We've been using self-signed X.509 identity certificates as identities,
+and that's been a useful way to get started, but it would be nice to be
+able to use other identities in the future.  Now a principal name is not
+marked in the representation at all.  New principal IDs will be of the
+form: [idtype:A].  The idtype will define what valid characters in A
+will be, but in any event "]" must be escaped with a backslash. 
+
+The current id's will be of idtype 'keyid', so only applying the
+principal extensions, the role A.r would be written [keyid:A].r, where A
+is the sha1 hash of the public key.  keyid principal names can include
+[0-9a-fA-F] (hex digits).
+
+I'm going to continue to use [keyid:A] here so not everything runs off
+the page.
+
+Data Objects
+
+The RT1 and RT2 parameters are loosely data objects.  RT1 allows one to
+reason about them, RT2 adds the ability to have principals make
+statements about these data objects.  Just as we need to represent
+principals including their type, we need to represent objects with their
+type.  We support following types:
+
+	int: 32-bit signed integers
+	float: floats in the range of an IEEE float.
+	time: a time expressed as yyyymmddThhmmss where the lower case
+		letters are digits and the T is a T.  Zulu time,
+		everything after the T is optional
+	boolean: true or false
+	urn: a resource named by a URN
+	string: a UTF-8 string.  This is a free space for people to
+		define local free-form attributes
+
+A particular object is specified by:
+
+[ type: name] 
+
+Objects are always specified this way, because rules and assignments may
+come from many places and the typing information must mesh.  The {}
+indicates this is data constant, as opposed to the variables below.
+
+Examples:
+
+	[boolean: true]
+	[int: 3454] 
+	[float: -323.0] also [ float: 1]
+	[time: 20111109T122300] also [ time: 20101010]
+	[urn:"file:///usr/local/bin/ls"]
+	[urn:"uuid://106c0cdd-0afb-11e1-90d8-14feb5e4012d"]
+	[string:"a string"]
+
+Roles anfd O-Sets
+
+In the ABAC papers, roles and o-sets look exactly alike, and one may
+have trouble understanding that they are different.  This spec
+explicitly types them for clarity.  Roles are prefixed by "role:" and
+o-sets by "o-set:".
+
+The rule that places principal P in role A.r is written in the paper as
+
+A.r <- P
+
+In our notation:
+
+[keyid:A].role:r <- [keyid:P]
+
+The rule that places file P in o-set A.r is written in the paper as
+
+A.r <- P
+
+In our notation:
+
+[keyid:A].oset:r <- ["urn:file://P"]
+
+Similarly derivation rules like:
+
+A.r <- B.r
+
+become 
+
+[keyid:A].role:r <- [keyid:B].role:r
+
+or
+
+[keyid:A].oset:r <- [keyid:B].oset:r
+
+depening on their intent.  It is an error to try (or probably to think):
+
+[keyid:A].oset:r <- [keyid:B].role:r
+
+Note also that
+
+[A.keyid].oset:os <- [keyid:B].role:r.oset:os
+
+Is the only valid linking credential for assigning o-sets.
+[keyid:B].role:r is a set of principals that may have defined an o-set
+(oset:os), but the members of an o-set could not have done so.
+
+Variables
+
+Both RT1 and RT2 allow rules defining roles or osets to match
+parameters using variable bindings.  We illustrate with roles here,
+though all of this holds for osets.  The variables may be named to
+specify connections between the role to be defined and the roles used to
+define it.
+
+For example the rule (in paper notation):
+
+A.evaluatorOf(?x) <- A.managerOf(?x)
+
+means that if 
+
+A.managerOf(mikeryan) <- faber
+
+then 
+
+A.evaluatorOf(mikeryan) <- faber 
+
+is also true.  The two ?x es bind to the same thing.  For more complex
+rules, we have to make sure that the types are also consistent:
+
+A.example(?x) <- A.isInteger(?x) & A.isFloat(?x)
+
+?x is not allowed to match an integer-typed data object in the first
+clause and a float-typed one in the second.  The papers say this is an
+invalid rule, but without knowing the types of the parameters it cannot
+be checked.
+
+We adopt the same variable naming convention, but require them to be
+prefixed with the types above.  Variable names start with a ? and can
+contain [_a-zA-Z0-9] that is, alphanumerics and the underscore.  ? is a
+valid anonymous variable name.  Multiple instances of ? in the same rule
+can bind to different types.  This is OK:
+
+[keyid:A]role:weird([urn:?x]) <- 
+	[keyid:B].role:a([urn:?x], [int:?]) & [keyid:C].role:b([urn:?x], 
+		[boolean:?])
+
+Other examples:
+
+[keyid:A].role:example([int:?x]) <- [keyid:A].role:isInteger([int:?x]) &
+	[keyid:A].role:isFloat([int:?x])
+
+is valid
+
+[keyid:A].role:example([int:?x]) <- [keyid:A].role:isInteger([int:?x]) &
+	[keyid:A].role:isFloat([float:?x])
+
+is not because the types of ?x are different.
+
+
+In addition to the data object types, the "principal" type is allowed as
+well, indicating that the variable must match an ABAC principal.  The
+first example in this section is written:
+
+[keyid:A].role:evaluatorOf([principal:?x]) <- 
+	[keyid:A].role:managerOf([principal:?x])
+
+Constraints
+
+A constraint is a static (RT1) or dynamic (RT2) set of valid choices for
+a parameter.  There are two kinds of constraint sets, static and
+dynamic.  A dynamic constraint set is an oset or role.  Static
+constraint sets are a list of valid values.  Constraints are separated
+from a variable name by a colon (:).
+
+We specify a static set by enclosing the values in [] separated by
+commas.  Because the set is bound to a typed variable the values in the
+set omit the [type:], so we write:
+
+[keyid:A].role:r([int:?x:[1,3,5]) 
+
+not
+
+[keyid:A].role:r([int:?x:[[int:1],[int:3],[int:5]]) 
+
+For ordered sets like integers and dates, the .. sequence specifies a
+range (floats may not be given ranges):
+
+[keyid:A].role:r(int:?x:[1..5])
+
+in static constraint sets, commas, elipses (..), and the bracket
+characters [, ] must be escaped using a backslash (\) prefix.
+
+The constraint can also be an oset (for objects) or a role (for a principal).
+
+[keyid:A].role:r([principal:?x:[[A].role:r1]) 
+[keyid:A].role:r([urn:?x:[[A].oset:o1]) 
+
+A Complex Example
+
+The example on p. 10 of "Design of a Role-Based Trust Management
+Framework" starts with the rule
+
+Alpha.fileAc(read, ?F:Alpha.documents(?proj)) <- Alpha.team(?proj)
+
+and says that given 
+
+Alpha.documents(proj1) <- fileA
+Alpha.team(proj1) <- Bob
+
+one can conclude 
+
+Alpha.fileAc(read, fileA) <- Bob
+
+In our notation the initial rule is encoded (note the mingling of o-sets
+and roles)
+
+[keyid:Alpha].role:fileAc([string:"read"], 
+	[string:?F:[keyid:Alpha].o-set:documents([string:?proj])]) 
+		<- [keyid:Alpha].role:team([string:?proj])
+
+and given 
+
+[keyid:Alpha].o-set:documents([string:"proj1"]) <- [string:"fileA"]
+[keyid:Alpha].role:team([string:"proj1"]) <- [keyid:Bob]
+
+one can conclude 
+
+[keyid:Alpha].role:fileAc([string:"read"], [string:"fileA"]) <- [keyid:Bob]
+
+It is more verbose, but draws out the different roles and o-sets in
+play.  
+
 REFERENCES
 
