This page introduces a trust management system Soutei. The system is essentially based on Binder. However we have
specified many aspects left undefined in the original DeTreville's
paper [Binder], and added several extensions. The most
notable extension is the disequality predicate and a type system to
guarantee its static safety and the preservation of monotonicity. Many
of the extensions -- such as the interaction between an application
and Soutei, communicating the context of the request to the decision
engine -- are notably influenced by the KeyNote system. We have
specified the protocol for sending Soutei assertions in HTTP requests
and in various certificates. We have also clarified the logical
meaning of the distinguished Binder/Soutei relation
says.
In the following, we first describe Soutei's syntax, which differs
from that of Binder. We added numeric and IP address literals. We
changed the syntax of variables and constants to inhibit user errors
that may have serious security consequences. We added a disequality
predicate, and a type system that statically ensures that disequality
and other restricted-mode predicates are safe and do not
destroy the overall monotonicity. A Soutei assertion that is found
unsafe is rejected by the compiler. We specify semantics of
Soutei. In particular, we concentrate on the application context and on the logical and operational interpretations of
says. We describe the use of Soutei for role-based or
capability-based access control, and the revocation of privileges.
Finally, we introduce a number of use cases. The cases are meant to illustrate notable aspects of the system -- in particular, several levels of trust delegation. We test both granting and rejecting user requests. The test cases are meant to be executable, and so to constitute an acceptance test of an early prototype and the regression test of the finished system.
A separate page [Transport] discusses various ways of making Soutei assertions available to the decision engine: by querying trusted databases, LDAP servers, or by delivering the assertions in HTTP headers and in Public-key and Attribute X.509 certificates.
| [1] | <Assertion> |
::= |
<Statement>* ; also called clause |
| [2] | <Statement> |
::= |
<Rule> | <Fact> |
| [3] | <Rule> |
::= |
<Head> ":-" <Body> "." |
| [4] | <Head> |
::= |
<pAtom> |
| [5] | <Fact> |
::= |
<Head> "." |
| [6] | <Body> |
::= |
<Atom> ( "," <Atom> )* |
| [7] | <Atom> |
::= |
<cAtom> | <pAtom> |
| [8] | <pAtom> |
::= |
<Predicate> "(" <Args> ")" |
| [9] | <cAtom> |
::= |
<Context> "says" <pAtom> |
| [10] | <Predicate> |
::= |
<symbol-constant> |
| [11] | <Args> |
::= |
<Term> ( "," <Term> )* |
| [12] | <Term> |
::= |
<constant> | <variable> |
| [13] | <Context> |
::= |
<Term> |
| [14] | <variable> |
::= |
"?" | "?"<id-symbol>+ |
| [15] | <constant> |
::= |
<string-constant> | <numeric-constant> | <symbol-constant> | <ip-constant> | <ipnetwork-constant> |
Clauses with the same predicate must be consecutive.
Lexical entities:
| [L1] | <string-constant> |
::= |
A quoted Scheme string |
| [L2] | <numeric-constant> |
::= |
A real Scheme number |
| [L3] | <symbol-constant> |
::= |
A Scheme symbol |
| [L4] | <ip-constant> |
::= |
"#p"<IP4-quad or IP6-address> |
| [L5] | <ipnetwork-constant> |
::= |
"#n"<IP4-quad or IP6-address>"/"<number of significant bits> |
| [L5] | <id-symbol> |
::= |
A lower- or upper-case character or digit that can appear in a
Scheme symbol |
As usual, non-terminals of the grammar are separated by whitespace. Whitespace between two non-terminals may be elided if the non-terminals can still be parsed separately. A semi-colon introduces a comment that spans through the closest line terminator: a line-feed character, a carriage-return character, or a combination of line-feed followed by carriage-return. A comment is considered whitespace.
The syntax differs in insignificant details from the language proposed in DeTreville's paper, and also from Prolog/Datalog. The main difference is the syntax of variables and constants. In the original Binder, as in Prolog on which it is based, capitalized symbols denote variables. The other symbols are constants. In a security language, symbols and variables stand for the names of people, programs, and computers. These names have different capitalization conventions. We must keep in mind that the main users of Soutei are not Prolog programmers. Rather, they are system and security administrators. Therefore, we should avoid glaring inconsistencies between the lexical conventions of the language and the domain.
There is a notably important reason to make the names of Soutei variables stand out. In the original Binder, an assertion
can(Pubkey,resource_r,read) :- pubkey(john,Pubkey).
pubkey(john,"0123436").
pubkey(doug,"abcde"). ...
allows the user john to read resource_r. However, if by mistake the administrator spelled the name of the
user in the conventional capitalization:can(Pubkey,resource_r,read) :- pubkey(John,Pubkey).
then he unwittingly allowed access to resource_r to
every registered user! The confusion between the domain
notation and the language notation can have grave
consequences. Therefore, we choose to prefix the names of all variables
with the question-mark character, to make the variable names really
stand out. That convention hopefully inhibits the errors of great
security consequence -- but it cannot assuredly eliminate them. We
must subject every Soutei assertion to a policy check, described later
on this page.
Thus the main syntactic difference from Prolog and the original Binder is that in our version, the names of all variables begin with the question mark. A single question mark stands for the anonymous variable. Other symbols -- capitalized or not -- are constants. Quoted strings are also considered constants. In fact, we do not draw any semantic distinction between symbolic constants and quoted strings. If the name of a constant starts with a question mark or contains spaces, parentheses, commas and other characters that are not permitted in Scheme identifiers, the name of the constant must be enclosed in double quotes. Otherwise, the name may be enclosed in double quotes. All names are case-sensitive.
We also extend the original Binder with numerical literals and literals for IP addresses. Internally, IP addresses are represented as 32 or 128-bit exact integers.
A Soutei assertion must satisfy safety constraints as described below. An assertion that fails to satisfy the safety property is rejected by the compiler and cannot be added to the system.
Our notion of safety corresponds to well-moded logical programs, as described in [Mercury-Modes]. However, the treatment of modes in Mercury is too operational, relying on notions such as `predicate call' and the instantiatedness of a variable `before' and `after' the call. In a bottom-up evaluation, there are no notions of `operator call' at all.
We are concerned about safety because of standard predicates such
as neq, the disequality predicate. If used without
restriction, the predicate destroys the formal properties of a logical
program, e.g., the existence of a minimal model -- let alone
monotonicity. Even the relation says is problematic unless
restricted, as in ?X says may(read) where ?X
is an uninstantiated variable. Should we try to enumerate all possible
namespaces and try may(read) in each of them? The
problems with neq and says can be eliminated
with run-time checks. However, that is not satisfactory: the monotonicity
property is compromised, seemingly unrelated changes to assertions may
lead to run-time errors, the ability of the system to optimize
assertions is restricted. Therefore, we would like to statically reject
assertions that are unsound or can cause run-time instantiatedness
failures. We would like to admit only those assertions that
can assuredly be evaluated without the above problems.
Thus we would like to introduce static safety and
monotonicity-preservation guarantees for mode-limited predicates and
especially for the limited form of negation -- disequality. Not only
we have to ensure that disequality can be evaluated in the context where
its arguments are fully instantiated. We also have to guarantee that
that the domain of neq arguments is invariant of remote
assertions. The latter preserves monotonicity: adding more
assertions to the system does not reduce the set of allowable security
actions. Our notion of monotonicity is identical to that of KeyNote:
`` An important principle in KeyNote's design is `assertion
monotonicity'; the policy compliance value of an action is always
positively derived from assertions made by trusted principals.
Removing an assertion never results in increasing the compliance
value returned by KeyNote for a given query.'' [RFC2704] [KeyNote]
Like in Datalog, to make sure neq and similar
predicates are safe, we introduce the notion of range-limited
variables: variables whose set of possible values is known to be
finite. However, the set of values may be defined by statements in
remote namespaces (assertions), which may need to be fetched and may
be unavailable due to network failures, etc. It is imperative to avoid
the situation where the system grants a request that would have been
denied had the network had operated normally.
Therefore, we introduce statically range limited
variables: whose range of values is fully known at the time the
query begins evaluation. For example, given application says
ipaddress(?IP), we know that the variable ?IP is
statically range limited, because the set of its possible values --
which is one, the IP address of the requesting client -- is fully known
at the time query begins evaluation. Similarly, if a namespace
defines a predicate access_mode by the two clauses:
access_mode(read). access_mode(write). then the variable
?X in an atom access_mode(?X) is statically
range limited because the set of possible values for ?X
is known and does not depend on any remote assertions.
To formulate statically verifiable safety conditions, we introduce the following type system.
Terms are associated with one of the three types:
S -- Statically range limitedL -- Range limitedA -- Any, including uninstantiatedThe types are ordered: A < L < S. We let the
meta-variable ttype range over these term types.
Every argument of a predicate and the first argument of the
relation says are assigned one of the following types:
PS, PL, RS, RL, A. Here the
letter P stands for `provides' and the letter R stands for
`required'. The types are ordered: RS < RL < A < PL < PS. We let the meta-variable ptype range over these types.
The first argument of the relation says has the type
RL. Predicates in the application namespace
have the types assigned to them. The types of other predicates are
inferred.
Informally, an assertion is safe if all the following three conditions hold:
PL or PS,RS, the
corresponding argument term has the type S,RL, the
corresponding argument term has the type L or S.The following is a formal system to determine the safety of an assertion. The results can also be used to reorder conjunctions.
Meta-variables:
term -- termatom -- atomatom* -- perhaps empty sequence of atomsatom+ -- a non-empty sequence of atomsvar -- variablettype -- term typeptype -- predicate argument typepred/n -- a predicate, local or context-qualified, of
arity n. The arity may be omitted if understood from the
context.i -- 1..n, where n is the
arity of the predicate in question.c -- ranges over all clauses that define a predicate
in question.The meta-constant [] stands for an empty sequence.
The notation pred/ni specifies the argument i of the predicate pred/n, whereas pred/nci
specifies the argument i of the predicate pred/n that appears in the head of the clause c.
Meta-functions:
Clauses(pred/n) -- all clauses that define the local predicate pred/nFV(atom) -- variables that appear in atomDom(Gamma) -- domain of a type environmentGExt(Gamma,var,ttype) -- extension of the type environment,
defined belowPredicate typing judgments:
|-pi pred/ni:ptype asserts that the argument i of
the predicate pred/n has the type ptype.
Axioms for the types of predicates
===> |-pi says1:RL
===> |-pi application says predi:ptype See the section about the application namespace.
===> |-pi term says predi:PL
forall c in Clauses(pred/n).|-pi pred/nci:ptype_c
ptype is lwb ptype_c
===> |-pi pred/ni:ptype
Clause c of pred/n is a fact
===> forall i in n.|-pi pred/nci:PS
Clause c of pred/n is a rule
===> forall i in n.|-pi pred/nci:PL
Type environment
The type environment Gamma associates variables within a clause
with their ttypes.
| [Gamma] | <Gamma> |
::= |
"[]" | ( <var : ttype> "," <Gamma> ) |
The extension function of the environment GExt(Gamma,var,ttype) is defined as follows:
var not in
Dom(Gamma)
===> var : ttype, Gamma
var : ttype1 in Gamma
ttype2 = max ttype ttype1
===> var : ttype2, Gamma\var
Typing of terms
Gamma|-t term:ttype asserts that the term has a ttype in the typing environment Gamma.
===> Gamma|-t constant:S
ttype1 <= ttype
===> x:ttype, Gamma|-t x:ttype1
Typing of the body of the rule: a sequence of atoms
Gamma|-ok atom* asserts that the sequence of atoms is well-typed
in the type environment Gamma.
===> []|-ok []
Gamma|-ok atom*
ti is a var
|-pi pred/ni:PL, Gamma' = GExt(Gamma,ti,L)
OR
|-pi pred/ni:PS, Gamma' = GExt(Gamma,ti,S)
===> Gamma'|-ok pred/n(t1,...tn), atom*
|-s1 clause asserts that the clause satisfies the safety
condition 1. This is the safety condition in the Datalog sense: a
<Head> must not contain variables that are not
used in its <Body>. In particular, a
<Fact> may not contain any variables at all. Another way
to look at this safety condition is as the justification of the
inductive assumption in the typing of predicates.
c is head :- []
FV(head) is []
===> |-s1 c
c is head :- atom+
Gamma|-ok atom+
forall v in FV(head).Gamma|-t x:L
===> |-s1 c
|-s2 clause and |-s3 clause assert that the clause
satisfies safety conditions 2 resp. 3.
c is head :- atom*
Gamma|-ok atom+
forall pred/n(t1,...tn) in atom*.forall ti in (t1,...tn).|-pi pred/ni:RS --> Gamma|-t ti:S
===> |-s2 c
c is head :- atom*
Gamma|-ok atom+
forall pred/n(t1,...tn) in atom*.forall ti in (t1,...tn).|-pi pred/ni:RL --> Gamma|-t ti:L
===> |-s3 c
The whole Soutei assertion is safe if every clause of it satisfies all three safety conditions.
A Soutei engine acts as a compliance checker that provides advice
to applications regarding specific actions. Actions and accompanying
data are described in terms of constants, atoms and
assertions. Assertions are grouped into named <Context>s, which are also called namespaces. To be more precise,
each <Atom> is associated with a particular
<Context>, via the distinguished predicate
says. There is also a local context for each
assertion. The local context is imputed to each atom without an
explicit context association. A context is identified by its name,
which is related to the issuer of the corresponding security
assertion. For example, the context identifier can be issuer's
distinguished name in a LDAP database. Alternatively, the context
identifier may be the issuer's public key or a hexadecimal string
encoding a SHA-1 hash of issuer's subject name. Such a hash is used in
OpenSSL as an index in a directory of certificates. The Soutei engine
treats context identifiers as opaque strings, with the exception of
two distinguished context names: system and application.
The Soutei engine starts up with an initial assertion, which has a
distinguished name system. The initial assertion is
normally written by the server security administrator and is placed
into a trusted configuration file.
An application invokes the Soutei engine by issuing a query. The
application gives the engine the context with a distinguished
name application. Rules and facts in the application
context describe the client and the requested action. The application
context also includes built-in predicates such as ip_of/2, and the distinguished predicate says/2.
The application asks the Soutei engine to prove an atom such as
system says may(X,Y,Z)
where X,Y,Z are the constants or variables that represent the resource, the action, or the principal. See the use cases below for more detail. The Soutei engine replies if the atom can be derived from the assertions at hand. If the atom can be proved, the engine returns a set of substitutions for the variables in the atom. If more than one set of substitutions prove the atom, only the first found set is returned.
We should stress that the predicate may is not
built-in. It is just the agreement between a particular application
and a policy writer. An application may choose to ask for
authorization advice using a different predicate with a different
number of parameters.
The application context defines facts and rules describing the authorization query. The context also defines built-in predicates. All statements in the application context are considered to be non-recursive. Hence the application context is implicitly an extensional database.
Statements of the application context describing the action and the request:
ipaddress/1|-pi ipaddress/11:PSpubkey_fingerprint/1|-pi pubkey_fingerprint/11:PSaccess_mode/1|-pi access_mode/11:PSAdditional predicates such as client's distinguished name or client's voice fingerprint can easily be added if a particular policy requires that.
The application context may provide built-in utility predicates.
ip_of/2ip_of(ip,ipnet) is provable if the IP
address ip is a part of the network ipnet,
specified as an IP network literal.|-pi ip_of/21:RL|-pi ip_of/22:RSneq/2|-pi neq1:RS|-pi neq2:RSThe application context also contains a distinguished predicate
says/2. An atom says(context_id,pAtom) is
provable if and only if the atom pAtom is provable in the
context context_id.
|-pi says1:RL
When the application receives a Soutei assertion the application
determines the issuer and derives the context identifier. If the
assertion was signed, the application checks the signature. The
application then compiles the assertion and, barring any errors,
extends the predicate says/2 with the compiled assertion
and context_id. Normally the application will cache received
assertions for some time (not exceeding the validity interval of the
certificate used to sign or carry the assertion). The predicate
says/2 therefore is an abstraction of that cache. The
application uses the signature bits of the signed certificate to
quickly determine if the received certificate is already in the
cache. If the received assertion is a part of an attribute certificate
with a non-empty holder, the assertion may not be cached. The
assertion can only be used for authorization decisions regarding the
holder.
saysThe original Binder paper [Binder] treats says as a quotation mark for imported assertions. In that
interpretation, ``context says'' is a modality of an atom. We however
interpret says in a different way. In our view, A says B means A |- B. The context identifier
becomes the denotation for a set of assumptions in a
natural-deduction-like proof. This view appears to be closely related
to a definitional logic of D.Miller, R.McDowell and
A.Tiu. Interestingly, this interpretation of says does
not seem to be mentioned in any of the papers related to Binder.
Treating says as the entailment relation lends
itself to a simple realization of Soutei in any (meta-)logic system
with first-class relations, such as [KANREN]. The examples
of induction proofs in KANREN illustrate the first-class treatment of
rules and facts. The Binder paper evaluates a set of assertions by
importing them all into one context, quoting their rules
correspondingly. We, on the other hand, refer to other contexts but do
not import them. We search for a proof of a formula in the context of
a particular assertion.
Role-based access control is a popular authorization technique. A trust management system [KeyNote] is a far more general mechanism that can trivially implement the most complex role-based authorizations. The Soutei engine, for example, bases its decisions entirely on the client identifiers provided by the requesting application. These identifiers may correspond to a particular user -- or to a particular role of that user. Soutei supports delegation by a principal of a (subset) of its privileges to another principal. A user therefore can delegate subsets of his permissions to various applications, agents, or representations of himself. Each such agent corresponds therefore to a particular role played by the user. Such a delegation is especially trivial if we chose Attribute certificates as the transport mechanism for Soutei assertions. A user can sign a number of attribute certificates based off his public key certificate -- each attribute certificate for a particular role and for a particular agent.
The Soutei engine lets the policy author specify hierarchies of roles and impose side conditions, e.g., a particular role can be used only if the request comes from a particular network or designated hosts.
The client identifier and the context identifier are treated by Soutei as opaque strings. The identifiers may be meaningful descriptions of real people, e.g., their e-mail or postal addresses. On the other hand, the identifiers may be meaningless unique strings that are given by an administrator to a client in a certificate or in some other assured way. The administrator can keep in a special context the record of these unique strings associated with human readable names of his choice:
capability("Dennis","RGVubmlzSnVsMjM=").
capability("John from the second floor, for a printer",
"Sm9obiBmcm9tIHRoZSBzZWNvbmQgZmxvb3IsIGZvciBhIHByaW50ZXI=").
If that context has the name capabilities, the policy
writer can use the human readable identifiers in his policies, for
example: may(printer,?id) :- capabilities says
capability("John from the second floor, for a printer",
?id), ...
or, if the fact the capability exists is sufficient,may(printer,?id) :- capabilities says capability(?,?id), ...
The re-direction afforded by the context such as capabilities can solve the ``stale resource name problem'': when
a resource is deleted, all access permissions to it should be
terminated. If another resource is created later with the same name,
the users of the old resource should not automatically have any access
rights to the new resource. In Soutei, resource names have no
particular significance and treated as opaque strings. The naming
conventions and the vocabulary of resources are defined exclusively by
requesting applications. Some applications may name the resource after
the SHA-1 hash of its content. Such names are effectively unique. We
can use translation contexts such as capabilities to
associate the unique names with some other attributes to help write
policies. The context names are themselves first-class and can be
associated with attributes in other contexts. Soutei lets policy
writers implement as extensive chains of reference and redirection as
necessary.
Soutei readily admits policies predicated on time: for example, the following statement permits write access to a file only during business hours, subject to supervisor's approval:
may("untitled.doc",write) :-
application says this-period(business-hours),
supervisor says may("untitled.doc",write).
In contrast, the following statement permits write access outside business hours:
may("untitled.doc",write) :-
application says this-period(?period),
application says neq(?period,business-hours),
supervisor says may("untitled.doc",write).
It is of course the job of the application to define what
constitutes business hours, and to determine if the time of the
request falls within that definition. The above examples assumed that
the application communicates its determination to Soutei via the
predicate this-period/1. An application programmer and a
policy writer could have chosen a different predicate and a different
set of terms for time intervals. The Soutei engine
could care less: the engine does not determine time. The engine merely
checks if application-provided facts about application-introduced terms
syntactically conform to the rules of the policy.
The next section explains how to introduce temporal order among the time intervals and to use it in policies.
So far, the policies were relating terms -- e.g., file names, access rights -- based solely on their equality or disequality. Some application domains however, such as time intervals, clearances, organizational charts, are ordered. We would like therefore to write policies that take the order into account, e.g., to permit access to a resource only if the user has clearance ``confidential'' and above.
One may doubt at first if such policies are at all expressible in
Soutei: after all, terms in Datalog lack any structure and so can be
compared only for equality. However, it is the fact that logic without
function symbols is equivalent to logic with function symbols, provided the unlimited supply of constants. For example, the
following assertion named user-list represents the list of
three elements, user1, user2, user3, in that order:
list(l1).
list-el(l1,user1,l2).
list-el(l2,user2,l3).
list-el(l3,user3,nil).
The distinguished constant nil represents the empty list. Now we can
write user-list says list(?l),
user-list says list-el(?l,?,?ln),
user-list says list-el(?ln,?user,?)
to find out the name of the second user.
The adjacency predicates such as list-el let us
specify arbitrary trees, lattices and partial orders. For example, we
can represent an organizational chart as the following assertion:
reports-to(VP-sales,CEO).
reports-to(VP-development, CEO).
reports-to(CFO,CEO).
reports-to(dept-sales-Japan,VP-sales).
reports-to(dept-sales-US,VP-sales).
reports-to(QA,VP-development).
reports-to(OS-division,VP-development).
reports-to(filesystem-group,OS-division).
If the above assertion is named org-chart, we can use it
to write the policy that permits access to a document named
``development milestones'' only to those employees that belong to the
development branch, from VP-development downwards: may("development milestones",?access) :-
known-access(?access),
application says this-user-div(?user,?ou),
path(?ou,VP-development).
path(?x,?x) :- org-chart says reports-to(?x,?). ; reflectivity
path(?x,?x) :- org-chart says reports-to(?,?x). ; reflectivity
path(?x,?y) :- org-chart says reports-to(?x,?y).
path(?x,?y) :- path(?x,?z), org-chart says reports-to(?z,?y).
Incidentally, the last clause of the path predicate exhibits left
recursion. Soutei can deal with it. The path predicate will work even
if the organizational chart is not a tree (e.g., two VPs share the
responsibility for same department) and has cycles. The example
assumed that the application tells the engine about the organizational
position of the requester via the predicate this-user-div/2. That data could be extracted from the employee's
PKI certificate, for example.
We can also write a policy that permits access to a document ``proposed reorg'' to employees in the OS-division and all their managers up the chain:
may("proposed reorg",read) :-
application says this-user-div(?user,?ou),
path(OS-division,?ou).
The assertion org-chart can be managed by a dedicated
person in an HR department, for example, to reflect changes in the
organizational structure. Unless the OS division is renamed, the above
policy needs no modifications. For example, a restructuring in sales
has no effect on the above policy, as it should not. If a new
position of COO is introduced to whom VP-development reports, the COO
could immediately read the ``proposed reorg'' document under the
policy.
It remains an interesting question the extent to which Soutei can emulate authorization systems such as constrained RT and others that explicitly deal with hierarchies, intervals and structured domains.
Just like KeyNote and Binder, the Soutei engine has the property of monotonicity: making more assertions known to the engine may potentially cause more authorization queries to be answered affirmatively -- but never fewer. Therefore, withholding an assertion from the decision engine can never cause the engine to advise an action that the engine will not advise otherwise.
The monotonicity property however makes the revocation of
previously granted privileges challenging (although the disequality
predicate neq/2 can greatly help here). We must first
remark that handling of revocations greatly depends on the chosen
mechanism of delivery of assertions to the engine.
If we use LDAP or other trusted database to store all assertions, and configure the Soutei engine to consult the database on each request or frequently enough, revocation becomes trivial. Removing from the database the assertion that originally granted the privilege to a particular client automatically revokes the privilege.
If assertions are delivered to the engine in signed messages or certificates, the validity of the certificate determines the validity of the assertion. If the certificate is expired, the corresponding assertion is effectively revoked. It is argued [Transport] that X.509 Attribute certificates are the most appropriate kind of certificates for Soutei assertions. Such certificates correspond to roles of the user or his agent, and are supposed to be issued for a very short validity period.
Hybrid assertion transport mechanisms lend themselves to flexible revocation strategies. For example, a policy can include the statement:
may(resource,?user,read) :- Admin says may(resource,?user,read),
LDAP says valid_user(?user).
That is, access to the resource is granted if both
statements can be proved: that Admin has granted the access right to the
user and that LDAP says the user is valid. The administrator may
grant the user privileges by giving him the corresponding
certificate. The user must present the certificate with his
requests. Proving LDAP says valid_user(?user) on the other
hand may involve an on-line check for the user in a trusted LDAP
database. Removing the user identifier from that database instantly
and effectively revokes the certificate Admin gave to the user.
We should also point out that if a client receives access to a resource via a delegation chain, removing the delegating assertion from anywhere in the chain terminates the access. At least one assertion in the chain -- the top one -- must come from a trusted source, a local configuration file. Assertions that come from such sources are easy to revoke.
Finally, the disequality predicate makes it easy to revoke access
for a specific user (a client on a specific network, etc). We should
modify the top, system assertion or other such assertion
by inserting an atom like neq(?IPAddress,#p10.10.1.127). No other assertion in the system and in delegation chains has to
be modified. The revocation takes effect immediately and we are sure of
that.
The slides from the June 7, 2005 demo of Soutei and its integration
with Navy Enterprise Single Sign-On (NESSO) and GIG-Lite (formerly,
Metcast) Channels can be found in the
demo/metcast-channels/doc/ directory of the
Soutei distribution.
The demo included examples of
delegation and Risk Adaptable Access Control (RAdAC).
To formulate the following executable use cases, we need to have a particular installation of Soutei in mind. We have chosen Metcast Channels [Metcast-Channels]. For the cases below, we have also chosen the assertion delivery mechanism: signed messages or X.509 certificates.
We start with the Metcast Channel database containing two empty
test channels MEMO and DEMO-IMG. We wish to
let any FNMOC client read and write MEMO. We let only
one remote user, named Joe, access the channel. We assign the user
Dean to be the administrator of DEMO-IMG. Dean shall control the
access to that channel.
To control the access to Metcast databases, we introduce a predicate
may/3. The atom may(database, resource, right) is provable if the requesting client has right to access
a particular Metcast database named resource.
The Initial assertion:
may(channel,MEMO,?a) :- application says ipaddress(?IP),
internal(?IP), access(?a).
may(channel,MEMO,?a) :- known_user(Joe), access(?a).
may(channel,"DEMO-IMG", ?Access) :-
pubkey(Dean,?Dean_key),
?Dean_key says may(channel,"DEMO-IMG", ?Access).
internal(#p10.10.1.1).
internal(?IP) :- application says ip_of(?IP,#n192.168.0.0/16).
known_user(?user) :- pubkey(?user,?key), pubkey_fingerprint(?key).
pubkey(Dean,"abcdef").
pubkey(Joe,"0123456789").
; Convenient abbreviations
pubkey_fingerprint(?x) :- application says pubkey_fingerprint(?x).
access(?a) :- application says access_mode(?a).
may(channel,DEMO-IMG,?a) :- application says access_mode(?a).. Dean specifies himself as the holder of the certificate.
may(channel,DEMO-IMG,?a) :- application says access_mode(?a). for the user Aaron.
may(channel,DEMO-IMG,read) :- known_user(Eric).
known_user(Eric) :-
application says pubkey_fingerprint("dddddd").
and the empty holder field and a validity period of one hour.
may(?c,?n,read) :- "eeeeee" says may(?c,?n,?).and the empty holder field. Ryan issues an attribute certificate to the user Greg:
may(channel,DEMO-IMG,?a) :- application says access_mode(?a). Greg is the
holder of the latter certificate.
may(channel,MEMO,?a) :- known_user(?Joe), access(?a).
may(channel,?MEMO,?a) :- known_user(Joe), access(?a)
[Binder] J. DeTreville. Binder, a logic-based security language. IEEE Security and Privacy, 2002.
<http://research.microsoft.com/research/pubs/view.aspx?tr_id=545>
[KeyNote]
<http://www.crypto.com/trustmgt/kn.html>
[Transport] Transport of Soutei assertions
[Metcast-Channels] Metcast Channels (see the Metnet site).
[KANREN] KANREN: A declarative applicative logic programming system
<http://kanren.sourceforge.net/>
[Mercury-Modes] The Mercury Language Reference Manual. Version 0.11.0. Modes.
<http://www.cs.mu.oz.au/research/mercury/information/doc-release/reference_manual_4.html>
This site's top page is http://soutei.sf.net/
Converted from SXML by SXML->HTML