The basis of QCM is the named relational algebra, which can be found in any standard database textbook (e.g., ). 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 p 's automaton.
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 (p says ). Suppose an `error' occurs and we are presented with both certificates. This might seem impossible, but the set of students is bound to change (students graduate) so an adversary could collect contradictory certificates over time and submit them together. Since , by the first definition we have . And then since , we have --even though q was never a teacher or administrator!
In our full QCM paper, we show how this can be prevented by an automatic analysis that rejects certificates that could cause inconsistencies.