Soutei: syntax, semantics, and use cases

Introduction

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.

Syntax of Soutei

Clauses with the same predicate must be consecutive.

Lexical entities:

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"). ...

     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.

Safety of assertions

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 limited
• L -- Range limited
• A -- Any, including uninstantiated

The 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:

• the type of every argument of every predicate defined in the assertion is inferred to be PL or PS,
• in every atom, if a predicate argument type is RS, the corresponding argument term has the type S,
• in every atom, if a predicate argument type is 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 -- term
• atom -- atom
• atom* -- perhaps empty sequence of atoms
• atom+ -- a non-empty sequence of atoms
• var -- variable
• ttype -- term type
• ptype -- predicate argument type
• pred/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/n
• FV(atom) -- variables that appear in atom
• Dom(Gamma) -- domain of a type environment
• GExt(Gamma,var,ttype) -- extension of the type environment, defined below

Predicate 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.

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*

Safety conditions of clauses

|-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.

Semantics of Soutei assertions

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.

Application Context

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

A predicate for the IP address of the client requesting the authorization decision.

|-pi ipaddress/11:PS

pubkey_fingerprint/1

A predicate for the public key fingerprint (i.e., the subject identity) of the requesting client.

|-pi pubkey_fingerprint/11:PS

access_mode/1

Access modes permitted by the application

|-pi access_mode/11:PS

Additional predicates such as client's distinguished name or client's voice fingerprint can easily be added if a particular policy requires that.

Built-in predicates

The application context may provide built-in utility predicates.

ip_of/2

An atom ip_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:RS

neq/2

The disequality predicate. It asserts that its two arguments are provably not equal. The equality is structural.

|-pi neq1:RS

|-pi neq2:RS

says predicate

The 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.

Logical interpretation of says

The 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.

Using Soutei

Role-based access control and Soutei

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.

Capabilities and Soutei

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=").

     may(printer,?id) :- capabilities says 
                             capability("John from the second floor, for a printer",
                                        ?id), ...

     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.

Policies predicated on time

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.

Lists, trees, organizational charts, and partial orders

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).

     user-list says list(?l),
     user-list says list-el(?l,?,?ln),
     user-list says list-el(?ln,?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).

     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).

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.

Revocation

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).

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.

Use cases

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 at Andrew Pimlott's site:
< https://www.metnet.navy.mil/~pimlotta/demo/slides/00.html>
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.

The list of certificates for the use cases can be found TBD.

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).

Scenario Local-MEMO

•  
  • Start the Soutei engine and load the initial assertions
  
   
•  
  • Write the document into MEMO from within FNMOC
  • Read the document back
  • Write another document from a metnet host
  • Read both documents
  Expect: All operations must succeed
   

Scenario Remote-MEMO

•  
  • See Scenario Local-MEMO through the point local-MEMO-1
  
   
•  
  • An attempt to access the MEMO channel in plain HTTP
  • Read the MEMO channel via HTTPS, but supplying no client public-key certificate
  • Read the MEMO channel via HTTPS, supplying an invalid client certificate (untrusted CA)
  • Read the MEMO channel via HTTPS, supplying an expired certificate
  • Read the MEMO channel via HTTPS, using a valid certificate, issued to the user Dean
  Expect: All attempts should be denied and logged.
   
•  
  • Write a document into the MEMO channel using HTTPS and a valid client public-key certificate issued to the user Joe
  • Read from the MEMO channel using HTTPS and the same certificate
  Expect: The channel should contain three documents. The remote user should obtain these three documents.
   

Scenario DEMO-IMG-simple

•  
  • Start the Soutei engine and load the initial assertions
  
   
•  
  • Try to write into DEMO-IMG from within FNMOC
  • Try to read from DEMO-IMG via HTTP
  • Try to read from DEMO-IMG via HTTPS without providing any client certificate
  • User Joe tries to read DEMO-IMG with his certificate
  • User Dean tries to read DEMO-IMG with his certificate
  Expect: All attempts should be denied and logged.
   
•  User Dean allows the full access to DEMO-IMG for himself.
  Dean issues an attribute certificate with the assertion may(channel,DEMO-IMG,?a) :- application says access_mode(?a).. Dean specifies himself as the holder of the certificate.
  • Dean sends his attribute certificate and his public-key certificate over HTTPS (in the header?) and writes a sample image into DEMO-IMG
  • The same but attempting to read the channel
  Expect: Channel should have the sample image. Dean was able to read it. Because the certificate has a non-empty holder name, the assertion is not added to the assertion cache.
   
•  
  • User Joe tries to read DEMO-IMG over HTTPS, with authentication
  • Dean sends his attribute certificate and his public-key certificate over HTTPS and attempts to read the channel MEMO
  • Joe tries to use Dean's attribute certificate from Dean-allows-himself to read DEMO-IMG. User Joe sends the certificate in an HTTP header and or? TLS
  • User Dean tries to read DEMO-IMG without providing the attribute certificate
  Expect: All attempts should be denied and logged.
   
•  Dean directly authorizes a user to access the channel.
  Dean issues an attribute certificate with the assertion may(channel,DEMO-IMG,?a) :- application says access_mode(?a). for the user Aaron.
  • Aaron sends the attribute certificate and his public-key certificate over HTTPS (in the header?) and reads the sample image from DEMO-IMG
  Expect: Aaron should get the image. The certificate is not cached.
   

Scenario DEMO-IMG-delegation-1

•  
  • Run Scenario DEMO-IMG-simple through the point init-tests-DEMO-IMG
  
   
•  Dean allows Eric to read from any channel he can read.
  Dean issues an attribute certificate with the assertion

       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.
  • Eric sends the attribute certificate and his public-key certificate over HTTPS (in the header?) and reads a sample image from DEMO-IMG
  • Eric attempts to read the channel again but without providing the attribute certificate
  Expect: Eric reads the image both times. Dean's assertion is added to the assertion cache.
   
•  
  • Joe attempts to read the channel DEMO-IMG.
  • Eric sends the attribute certificate and his public-key certificate over HTTPS (in the header?) and attempts to write another sample image into DEMO-IMG
  • Eric sends the attribute certificate and his public-key certificate over HTTPS (in the header?) and attempts to read MEMO
  • Eric attempts to read DEMO-IMG after one hour has passed
  Expect: All attempts should be denied and logged. Dean's assertion should no longer be in the assertion cache.
   
•  
  • Joe attempts to read the channel DEMO-IMG providing the renewed Dean's certificate
  Expect: All attempts should be denied and logged. Dean's assertion is added to the assertion cache.
   

Scenario DEMO-IMG-delegation-2

•  
  • Run Scenario DEMO-IMG-simple through the point init-tests-DEMO-IMG
  
   
•  Dean allows Ryan to delegate reading from any channel.
  Dean issues an attribute certificate with the assertion

       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.
  • Greg sends Dean's and Ryan's attribute certificates and his public-key certificate over HTTPS (in the header?) and reads a sample image from DEMO-IMG
  • Greg attempts to read the channel again but without providing Dean's attribute certificate
  Expect: Greg reads the image both times. Dean's assertion is added to the assertion cache.
   
•  
  • Joe attempts to read the channel DEMO-IMG
  • Greg sends both attribute certificates and his public-key certificate over HTTPS (in the header?) and attempts to write another sample image into DEMO-IMG
  • Greg sends both attribute certificates and his public-key certificate over HTTPS (in the header?) and attempts to read from MEMO
  Expect: All attempts should be denied and logged. Dean's assertion should be in the assertion cache.
   

Scenario Policy-Check

•  Checking the initial assertion
  • Check that there is a Metcast channel and a (remote or local) user that cannot access this channel
  • Check that there is a channel that is not writable by everybody
  • Check that there is no channel that can be accessed by every known user
  
   
•  Introduce a mistake into the initial assertion:
  may(channel,MEMO,?a) :- known_user(?Joe), access(?a).
  The spurious question mark before the user name turns the constant into a variable.
  • Run checks of policy-check-init-assertion
  Expect: Policy check should fail: every known user can read and write the channel MEMO.
   
•  Check that the user Dean is in full control over DEMO-IMG.
  • Check that no one can access DEMO-IMG unless Dean allows him to. That is, the explicit denial of access by Dean disallows all access to the channel.
  
   
•  Introduce a mistake into the initial assertion:
  may(channel,?MEMO,?a) :- known_user(Joe), access(?a)
  The spurious question mark before the name of the channel turns the constant into a variable.
  • Run checks of policy-check-delegation
  Expect: Policy check should fail: the user Joe is now allowed full access to the channel DEMO-IMG, regardless of Dean's wishes.
   

References

[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

[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>

Last updated December 7, 2005

Converted from SXML by SXML->HTML

$Id: Auth-use-cases.scm,v 2.8 2005/12/08 01:36:49 oleg Exp oleg $