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
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.
Clauses with the same predicate must be consecutive.
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
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
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
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
is an uninstantiated variable. Should we try to enumerate all possible
namespaces and try
may(read) in each of them? The
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
ipaddress(?IP), we know that the variable
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
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
ttype range over these term types.
Every argument of a predicate and the first argument of the
says are assigned one of the following types:
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
have the types assigned to them. The types of other predicates are
Informally, an assertion is safe if all the following three conditions hold:
RS, the corresponding argument term has the type
RL, the corresponding argument term has the type
The following is a formal system to determine the safety of an assertion. The results can also be used to reorder conjunctions.
atom*-- perhaps empty sequence of atoms
atom+-- a non-empty sequence of atoms
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.
nis the arity of the predicate in question.
c-- ranges over all clauses that define a predicate in question.
 stands for an empty sequence.
pred/ni specifies the argument
i of the predicate
specifies the argument
i of the predicate
pred/n that appears in the head of the clause
Clauses(pred/n)-- all clauses that define the local predicate
FV(atom)-- variables that appear in
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
pred/n has the type
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
The type environment Gamma associates variables within a clause
The extension function of the environment
GExt(Gamma,var,ttype) is defined as follows:
var not in
===> 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 
ti is a var
|-pi pred/ni:PL, Gamma' = GExt(Gamma,ti,L)
|-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+
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*
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*
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,
<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:
The Soutei engine starts up with an initial assertion, which has a
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
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
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:
Additional 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(ip,ipnet)is provable if the IP address
ipis a part of the network
ipnet, specified as an IP network literal.
The application context also contains a distinguished predicate
says/2. An atom
provable if and only if the atom
pAtom is provable in the
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
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
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
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
not seem to be mentioned in any of the papers related to Binder.
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
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
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
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
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).
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
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
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
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
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
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
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.
[Transport] Transport of Soutei assertions
[Metcast-Channels] Metcast Channels (see the Metnet site).
[KANREN] KANREN: A declarative applicative logic programming system
[Mercury-Modes] The Mercury Language Reference Manual. Version 0.11.0. Modes.
This site's top page is http://soutei.sf.net/
Converted from SXML by SXML->HTML