The basis of QCM is the named relational algebra, which can be found in any standard database textbook (e.g., [1]). A QCM program is a set of definitions,

where each is a relation symbol and each is a relational algebra expression. We require the definitions to typecheck, and we do not permit recursive definitions. We saw several examples of QCM programs in the last section.

QCM programs interact by exchanging database queries and responses. A response is a certificate

where *M* is a relational algebra query and *N* is a table.
A query is a certificate

where *M* is the relational algebra query, and *C* is a set of
response certificates submitted along with the query.

The exchange of messages and verification of signatures is specified by an automaton, which we do not describe fully here; the examples of the last section show some of the details. The main task of the automaton is to gather a set of inclusions,

that will be used to evaluate queries. These inclusions are gathered from responses to queries and also from certificates that are submitted to the automaton along with queries. The main correctness theorem states that the responses a principal issues in fact follow from these inclusions:

**Theorem:** If (** p says **), then
is implied by the inclusions
of

There are two important consequences of the theorem. The first is that programmers are justified in thinking of their programs as defining sets--according to the theorem, the answer to a query follows from the inclusions, and does not depend on the sequence of message exchanges used to gather the inclusions.

Second, we must be very careful in what we believe: if the inclusions
are *inconsistent* , then they imply *any* conclusion
. The following example, based on SDSI 1.1, shows that
carelessness in this matter can lead to a security breach. We define
two groups, and :

Suppose is maintained by a remote principal, *p* . In
order to decide whether or not a principal *q* is a member of
or , we require a document, signed by *p* ,
stating whether or not *q* is a member of : that is, a
certificate (** p says **), or (

In our full QCM paper, we show how this can be prevented by an automatic analysis that rejects certificates that could cause inconsistencies.