format: text

text:
# A logical reconstruction of SPKIA preliminary version of this appeared in the Proceedings of the 14th IEEE Computer Security Foundations Workshop, 2001, pp. 59–70.

## 1 Introduction

Rivest and Lampson (?) introduced SDSI—a Simple Distributed Security Infrastructure—to facilitate the construction of secure systems. In SDSI, principals (agents) are identified with public keys. In addition to principals, SDSI allows other names, such as poker-buddies. Rather than having a global name space, these names are interpreted locally, by each principal. That is, each principal associates with each name a set of principals. Of course, the interpretation of a name such as poker-buddies may be different for each agent. However, a principal can “export” his bindings to other principals using signed certificates. Thus, Ron may receive a signed certificate from the principal he names Joe describing a set of principals Joe associates with poker-buddies. Ron may then refer to this set of principals by the expression Joe’s poker-buddies. Rivest and Lampson (?) give an operational account of local names; they provide a name-resolution algorithm that, given a principal $`𝚔`$ and a name $`𝚗`$, computes the set of principals associated with $`𝚗`$ according to $`𝚔`$. In \[Halpern and van der Meyden 2001\], building on earlier work of Abadi (?), we give a logic LLNC, the Logic of Local Name Containment, with clean semantics that precisely captures SDSI’s operational name resolution algorithm.

However, our earlier work made a number of simplifying assumptions to bring out what we saw as the main issues of name spaces. In particular, we (along with Abadi) assumed that certificates never expired and were not revoked. SDSI has been incorporated into SPKI \[Ellison, Frantz, Lampson, Rivest, Thomas, and Ylonen 1999a, Ellison, Frantz, Lampson, Rivest, Thomas, and Ylonen 1999b\], which allows expiry dates for certificates and revocation, and deals with authorization and delegation in addition to naming. In this paper, we show how our earlier approach can be extended to deal with these features of SPKI.

By not having expiry dates and not allowing revocation, we get a monotonicity property: having more certificates can never mean that fewer keys are bound to a given name. Heavy use seems to be made of monotonicity in our earlier work.111Ninghui Li (?) has erroneously claimed that LLNC is nonmonotonic. See \[Halpern and van der Meyden 2001\] for a rebuttal and discussion of this claim. A number of authors have developed logical accounts of authorization based on nonmonotonic logics \[Woo and Lam 1993, Jajodia, Samarati, and Subramanian 1997, Li, Grosof, and Feigenbaum 1999, Li, Grosof, and Feigenbaum 2000\]. These are logics where conclusions can be retracted in the presence of more information (so that $`C`$ may follow from $`A`$ but not from $`AB`$). It has been suggested that revocation should be modeled using a nonmonotonic logic \[Li, Grosof, and Feigenbaum 1999\].222Although it does not go into details about the nonmonotonic features, \[Li, Grosof, and Feigenbaum 1999\] mentions a logic DL, whose notable features are said to include “The ability to handle non-monotonic policies. These are policies that deal explicitly with ‘negative evidence’ and specify types of requests that do not comply. Important examples include hot-lists of ‘revoked’ credentials …. ‘Non-monotonic’ here means in the sense of logic-based knowledge representation (KR).” Some of the authors of this paper have also taken an alternate position: Li and Feigenbaum (?) recommend that “a PKI should provide an interface that is monotonic”.  Dealing with nonmonotonicity adds significant complications to a logic, both conceptually and from a complexity-theoretic point of view (see, for example, \[Cadoli and Lenzerini 1994\]). Thus, there is a benefit to using a monotonic logic where possible. We show that there is no difficulty capturing expiry dates and revocation (at least as they appear in SPKI) using a monotonic logic. Interestingly, SPKI’s semantics maintains monotonicity even in the presence of revocation, in the sense that having more certificates (even more revocation certificates) still allows us to draw more conclusions about both name bindings and authorizations. (Roughly speaking, this is because, in SPKI, a certificate is ignored unless it is known not to have been revoked. Having a revocation certificate issued by $`𝚔`$ covering a certain time $`𝚝`$ ensures that there are no other revocation certificates issued by $`𝚔`$ covering $`𝚝`$, and thus allows us to conclude that certain certificates have not been revoked at time $`𝚝`$. Thus, by having more revocation certificates, we can draw more conclusions.)

We remark that, although SPKI is monotonic with respect to adding more certificates, it is not monotonic with respect to time. Keys that are bound to a name at time $`t`$ may no longer be bound to that name at time $`t^{}>t`$. (Indeed, this does not require revocation; it suffices that certificates have intervals of validity.)

SPKI gives semantics to certificates by first converting them to tuples, and then providing tuple reduction rules, which are used to reduce the tuples to a particularly simple form (corresponding to basic name binding and authorization decisions). We associate with each SPKI certificate a formula in our logic. Thus, we have two ways of giving semantics to SPKI certificates: through tuple reduction and through the logic. The focus of this paper is on examining the connection between these two approaches. Our analysis highlights places where SPKI’s informal description of tuple reduction is somewhat vague, and shows that extra reduction rules are necessary in order to capture general information about binding and authorization. Besides clarifying ambiguities, the logic allows for reasoning about the consequences of certain certifications and general reasoning about naming and authorization. (See Section 7 for further discussion of the potential uses of the logic.)

The rest of this paper is organized as follows. In the next section, we briefly describe the syntax of SPKI. In Section 3, we describe SPKI’s reduction rules. Section 4 describes the syntax and semantics of our logic for reasoning about SPKI, which extends LLNC. In Section 5, we prove our main results, which involve characterizing the power of SPKI reduction rules in terms of our logic. In Section 6, we compare our work to several other recent approaches to giving semantics to SPKI. We conclude in Section 7 with further discussion of the logic.

## 2 SPKI syntax

SPKI views authority as being associated with principals, which it identifies with public keys. Instead of global names, SPKI has incorporated SDSI’s notion of local name space. In SDSI/SPKI, a local name such as Joe is interpreted with respect to a principal, and its meaning may vary from principal to principal. There is no requirement that a local name refer to a unique principal. For example, a local name such as poker-buddies may refer to a set of principals. Within its name space, a principal may refer to the interpretation of names in another principal’s name space by means of compound names. For example, a principal may use the expression Joe’s poker-buddies to refer to the principals that the principal he refers to as Joe refers to as poker-buddies. SPKI calls such expressions compound (SDSI) names, and uses the syntax (name $`𝚗_1𝚗_2\mathrm{}𝚗_k`$), where the $`𝚗_i`$ are local names (called basic SDSI names in the SPKI document) for $`i>1`$ and $`𝚗_1`$ is either a local name or a key. Such an expression may also be represented as $`𝚗_1\text{’s}𝚗_2\text{’s}\mathrm{}𝚗_k`$. A fully-qualified name is one where $`𝚗_1`$ is a key and $`𝚗_2,\mathrm{},𝚗_k`$ are local names. While, in general, the interpretation of a compound name depends on the principal (so that the interpretation of Joe’s poker-buddies by key $`𝚔_1`$ depends on $`𝚔_1`$’s interpretation of Joe, and may be different from $`𝚔_2`$’s interpretation of Joe and Joe’s poker-buddies), the interpretation of a fully-qualified name is independent of the principal.

SPKI has other ways of identifying principals. For example, SPKI principals may also be the hash of a key, a threshold subject (an expression representing “any $`m`$ out of $`N`$ of the following subjects”, used to capture requirements for joint signatures), or the reserved word “Self”, representing the entity doing the verification. For simplicity, in this paper, the only principals we consider are those defined by compound names.

There are two types of certificates in SPKI, naming certificates, authorization certificates. SPKI also has certificate revocation lists (CRLs); for uniformity, we treat these as certificates as well. Again, this seems completely consistent with the SPKI treatment. A naming certificate has the form of a cryptographically signed message with contents

$$(\mathrm{𝚌𝚎𝚛𝚝}(\mathrm{𝚒𝚜𝚜𝚞𝚎𝚛}(\mathrm{𝚗𝚊𝚖𝚎}𝚔𝚗))(\mathrm{𝚜𝚞𝚋𝚓𝚎𝚌𝚝}𝚙)\text{valid}),$$

where $`𝚔`$ is a key (representing the issuer, whose signature should be on the certificate), $`𝚗`$ is a local name, $`𝚙`$ is a fully-qualified SDSI name,333 SPKI also allows $`𝚙`$ to be an unqualified name (that is, a string of local names), but notes that in this case it is to be interpreted as $`𝚔\text{’s}𝚙`$, which is a fully qualified name. For simplicity, we insist upon fully qualified names here. and $``$valid$``$ is an optional section describing validity constraints on the certificate. The $``$valid$``$ section may describe an interval during which the certificate is valid, expressed by means of a “not-before date” (expressed in the syntax as (not-before $``$date$``$)) and/or a “not-after date” (expressed as (not-after $``$date$``$)). It may also describe a sequence of “online test” expressions, which specify that the certificate should be verified either by checking a certificate revocation list (CRL) (intuitively, a list of certificates that have been revoked), by checking a revalidation list (a list of currently valid certificates), or by performing an online test. Each of these components is optional.

In this paper, we assume that the $``$valid$``$ field contains only validity intervals and a key authorized to sign revocation lists relevant to the certificate; the treatment for revalidation lists and other online tests is similar and does not add new subtleties.444SPKI also allows a certificate to specify a list of locations where the CRL may be obtained (rather than requiring that the actual CRL be sent), and to provide http requests to these locations with extra parameters, but we ignore these components since they do not interact with the semantic issues we address. We represent dates as natural numbers. From the not-before and not-after sections of a certificate we may obtain a validity interval $`𝚅=[𝚝_1,𝚝_2]`$ where $`𝚝_1,𝚝_2IN\{\mathrm{}\}`$ are respectively the not-before time and the not-after times indicated. If no not-before time is given, we take $`𝚝_1=0`$ and, similarly, if no not-after time is given, we take $`𝚝_2=\mathrm{}`$. We assume that $`𝚝_1𝚝_2`$, so that the validity interval is nonempty. We also allow the empty interval, which we denote $`\mathrm{}`$.

For simplicity, we abbreviate naming certificates as $`(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚗𝚙𝚅𝚔_r)`$, where $`𝚅`$ has the form $`[t_1,t_2]`$ and $`𝚔_r`$ is the key which is authorized to sign CRLs relevant to the certificate. The $`𝚔_r`$ component may not be present: if it is, then we say that the certificate is revocable by $`𝚔_r`$. We occasionally write $`(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚗𝚙𝚅𝚔_r)`$ to denote a generic naming certificate where $`𝚔_r`$ may or may not be present. A naming certificate binds the fully-qualified name $`𝚙`$ to the local name $`𝚗`$ in $`𝚔`$’s local name space during the period $`𝚅`$, provided that certificate does not appear in any CRLs signed by $`𝚔_r`$. Binding $`𝚙`$ to $`𝚗`$ means that the interpretation of $`𝚗`$ with respect to $`𝚔`$ includes the meaning of $`𝚙`$. For example, if Ron and Joe are principals, then the certificate $`(\mathrm{𝚌𝚎𝚛𝚝}\mathrm{𝚁𝚘𝚗}\mathrm{𝚍𝚘𝚌𝚝𝚘𝚛}(\mathrm{𝙹𝚘𝚎}^{}𝚜\mathrm{𝚍𝚘𝚌𝚝𝚘𝚛})[1,3])`$ binds Joe’s doctor to the local name doctor in Ron’s local name space from time 1 to time 3; moreover, this certificate is irrevocable.

Authorization certificates have the form

$$\left(\mathrm{𝚌𝚎𝚛𝚝}\left(\mathrm{𝚒𝚜𝚜𝚞𝚎𝚛}𝚔\right)\left(\mathrm{𝚜𝚞𝚋𝚓𝚎𝚌𝚝}𝚙\right)\left(\mathrm{𝚙𝚛𝚘𝚙𝚊𝚐𝚊𝚝𝚎}\right)𝙰\text{valid}\right),$$

where $`𝚔`$ is a key, $`𝚙`$ is a fully-qualified name,555SPKI also allows the subject to be an unqualified name. We make the simplifying assumption of qualified names just as we did above. $`𝙰`$ is what the SPKI document calls an authorization and we call an action expression, since it represents a set of actions, and $``$valid$``$ is a validity section, as described above. The “(propagate)” section is optional. Intuitively, the issuer uses such a certificate to grant the subject the authority to perform the actions in $`𝙰`$. Moreover, if “(propagate)” is present, then the subject is further authorized to propagate this authority to others.666 Note that if “(propagate)” is not present, then we treat this as there being no indication of whether the subject is authorized to propagate the authority to others, rather than it being the case that the subject is not permitted to propagate the authority. This allows it to be consistent for $`𝚔`$ to issue two certificates that are identical except that one contains “(propagate)” while the other does not. Under our interpretation, the former supersedes the latter. (This seems particularly reasonable if we assume that someone who is seeking permission to perform an action will present those certificates that maximize his/her rights.) The SPKI document is silent on this issue. We abbreviate authorization certificates as $`(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚙𝙳𝙰𝚅𝚔_r)`$, where $`𝙳`$ is a a Boolean (which stands for delegate) indicating whether or not propagation is permitted. Again, the $`𝚔_r`$ component is optional, and we use $`(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚙𝙳𝙰𝚅𝚔_r)`$ to denote a generic authorization certificate where the $`𝚔_r`$ component may or may not be present.

SPKI takes an action expression $`𝙰`$ to be an S-expression—a list of strings or sublists. It uses $`\mathrm{𝙰𝙸𝚗𝚝𝚎𝚛𝚜𝚎𝚌𝚝}`$ to denote the intersection of action expressions.777Howell and Kotz \[Howell and Kotz 2000\] have noted some problems with intersection for SPKI’s action expressions (or tags), namely that not all intersections of tags can be represented as a tag. The problem can be eliminated by extending the set of tags. We simply avoid the issue here by treating action expressions very abstractly, and assuming that they can always be intersected. As we suggested above, action expressions are best thought of as sets of actions. We abstract this by assuming that there is some set $`\mathrm{𝐴𝑐𝑡}`$ of actions and a set $`𝒜`$ of action expressions that, intuitively, represent sets of actions in $`\mathrm{𝐴𝑐𝑡}`$. We assume that $`𝒜`$ includes all finite subsets $`\{𝚊_1,\mathrm{},𝚊_n\}`$ of $`\mathrm{𝐴𝑐𝑡}`$. Moreover, we assume that, given two action expressions $`𝙰_1`$ and $`𝙰_2`$ in $`𝒜`$, we can easily compute a third action expression in $`𝒜`$, denoted $`𝙰_1𝙰_2`$, which intuitively represents the intersection of the sets represented by $`𝙰_1`$ and $`𝙰_2`$. (We capture this intuition by a semantic constraint below.) The reason that we allow expressions in $`𝒜`$, rather than just finite subsets of $`\mathrm{𝐴𝑐𝑡}`$, is that SPKI allows (some) expressions that represent infinite sets of actions. For example, SPKI allows an action expression of the form (ftp ftp.clark.net /pub/cme/\*), which allows access to directories ftp.clark.net that start with /pub/cme/ (see \[Ellison, Frantz, Lampson, Rivest, Thomas, and Ylonen 1999a, Section 6.3.1\]).

We assume that there is a fixed action interpretation $`\alpha _𝒜`$ that maps action expressions in $`𝒜`$ to subsets of $`\mathrm{𝐴𝑐𝑡}`$. We require that if $`𝙰`$ is a finite subset of $`\mathrm{𝐴𝑐𝑡}`$, then $`\alpha _𝒜(𝙰)=𝙰`$, and that $`\alpha _𝒜(𝙰_1𝙰_2)=\alpha _𝒜(𝙰_1)\alpha _𝒜(𝙰_2)`$. We also assume that we can decide (given $`𝙰_1`$ and $`𝙰_2`$) whether $`\alpha _𝒜(𝙰_1𝙰_2)=\alpha _𝒜(𝙰_2)`$ (intuitively, whether $`𝙰_1`$ denotes a subset of $`𝙰_2`$).

A CRL has the form

$$(\mathrm{𝚌𝚛𝚕}(\mathrm{𝚌𝚊𝚗𝚌𝚎𝚕𝚎𝚍}𝚌_\mathrm{𝟷},\mathrm{},𝚌_𝚗)𝚅)$$

where the $`𝚌_i`$ are hashes of certificates.888SPKI also allows delta-CRLs. We omit these since they do not introduce essentially new semantic issues. It is left implicit that the CRL needs to be signed by some key $`𝚔`$. For simplicity, we will assume that CRLs contain certificates themselves rather than hashes. We abbreviate a CRL as $`(\mathrm{𝚌𝚛𝚕}𝚔(\mathrm{𝚌𝚊𝚗𝚌𝚎𝚕𝚎𝚍}𝚌_\mathrm{𝟷},\mathrm{},𝚌_𝚗)𝚅).`$ Intuitively, this says that, according to the issuer $`𝚔`$, the certificates $`𝚌_\mathrm{𝟷},\mathrm{},𝚌_𝚗`$ are revoked during the interval $`𝚅`$. We require that each of the certificates $`𝚌_i`$ be revocable by $`𝚔`$ (otherwise $`𝚔`$ is attempting to revoke a certificate that it is not entitled to revoke).

Let $`𝒞^+(K,N,𝒜)`$ consist of all certificates over $`(K,N,𝒜)`$ (i.e., where all the keys are in $`K`$, all the names used are in $`N`$, and all the action expressions are in $`𝒜`$); let $`𝒞(K,N,𝒜)`$ be the subset of $`𝒞^+(K,N,𝒜)`$ consisting of all naming and authorization certificates; and let $`𝒞_R(K,N,𝒜)`$ be the subset of $`𝒞^+(K,N,𝒜)`$ consisting of all CRLs.

## 3 SPKI’s tuple reduction rules

The semantics of SPKI certificates is characterized by a description of the algorithm invoked to verify that a sequence of credentials supports an authorization decision \[Ellison, Frantz, Lampson, Rivest, Thomas, and Ylonen 1999a, Section 6\]. It is left to the prover (the agent presenting a set of credentials) to construct an appropriate sequence before submitting a request to the verifier.

Given a set $`C`$ of naming and authorization certificates and a set $`C_R`$ of CRLs, the algorithm first converts these certificates to a set of tuples, and reduces these tuples according to certain rules.

There are two types of tuples: 4-tuples, related to name binding certificates, and 5-tuples, related to authorization certificates. A 4-tuple has the form $`𝚔,𝚗,𝚙,𝚅`$ where the components are exactly as in the first four components of a naming certificate. Similarly, a 5-tuple has the form $`𝚔,𝚙,𝙳,𝙰,𝚅`$, where the components are exactly as in an authorization certificate. Note that neither the 4-tuples nor the 5-tuples mention the $`𝚔_r`$ component of authorization certificates. We use $`\tau _𝚌`$ to denote the 4- or 5-tuple corresponding to certificate $`𝚌`$.

The first step in the conversion is to check each certificate in $`C`$ to see if it has been revoked. Given a naming certificate $`𝚌=(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚗𝚙[𝚝_0,𝚝_1]𝚔_r)`$ and a CRL $`𝚌_R=(\mathrm{𝚌𝚛𝚕}𝚔_r^{}(\mathrm{𝚌𝚊𝚗𝚌𝚎𝚕𝚎𝚍}𝚌_\mathrm{𝟷},\mathrm{},𝚌_𝚗)[𝚝_\mathrm{𝟶}^{},𝚝_\mathrm{𝟷}^{}])`$, say that $`𝚌`$ is live with respect to $`𝚌_R`$ if

1. $`𝚌`$ is signed by $`𝚔`$, and
2. the following four conditions all hold:

1. $`𝚔_r=𝚔_r^{}`$,
    2. $`𝚌_R`$ is signed by $`𝚔_r^{}`$,
    3. $`[𝚝_0,𝚝_1][𝚝_0^{},𝚝_1^{}]\mathrm{}`$,
    4. $`𝚌\{𝚌_1,\mathrm{},𝚌_n\}`$.

Intuitively, $`𝚌`$ is live with respect to $`𝚌_R`$ if $`𝚌`$ is properly signed, the validity component in $`𝚌`$ requires checking a CRL, $`𝚌_R`$ is the certificate appropriate for the CRL and, according to the CRL, $`𝚌`$ has not been revoked. If $`𝚌`$ is live with respect to $`𝚌_R`$, define $`\tau (𝚌,𝚌_R)`$ to be the 4-tuple $`(𝚔𝚗𝚙[𝚝_0,𝚝_1][𝚝_0^{},𝚝_1^{}])`$. If $`𝚌`$ is an authorization certificate, there is an essentially identical notion of liveness with respect to $`𝚌_R`$ and corresponding 5-tuples $`\tau (𝚌,𝚌_R)`$. We leave details to the reader. Define $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)`$ to be the set of tuples $`\tau (𝚌,𝚌_R)`$ where $`𝚌C`$, $`𝚌_RC_R`$, and $`𝚌`$ is live with respect to $`𝚌_R`$, together with the set of tuples $`\tau _𝚌`$ where $`𝚌C`$ is irrevocable.

The mapping $`\tau (𝚌,𝚌_R)`$ is our attempt to capture the mapping described in \[Ellison, Frantz, Lampson, Rivest, Thomas, and Ylonen 1999a, Section 6\], which says:

> Individual certificates are verified by checking their signatures and possibly performing other work. They are then mapped to intermediate forms, called “tuples” here. The other work for SPKI or SDSI certificates might include processing of on-line test results (CRL, re-validation or one-time validation). … If on-line tests are involved in the certificate processing, then the validity dates of those on-line test results are intersected …with the validity dates of the certificate to yield the dates in the certificate’s tuple(s).

Note that the mapping $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)`$ is monotonic: if $`C^{}C`$, $`C_R^{}C_R`$, then $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C^{},C_R^{})\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)`$. Intuitively, a certificate $`𝚌C`$ that is revocable by $`𝚔_r`$ is considered to be valid at time $`𝚝`$ if there is clear evidence that $`𝚌`$ has not been revoked by $`𝚔_r`$ at time $`𝚝`$, where the “evidence” is that there is a CRL issued by $`𝚔_r`$ that covers time $`𝚝`$ that does not mention $`𝚌`$. The absence of a certificate $`𝚌`$ from any relevant CRL $`𝚌^{}`$ ensures that the statement being made by that certificate applies during the intersection of the intervals of $`𝚌`$ and $`𝚌^{}`$.

The intuition that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)`$ consists of the still valid certificates does not hold up so well when there can be more than one CRL relevant to the validity of a certificate $`𝚌`$ at a time $`𝚝`$. For suppose that $`𝚌`$ is revoked according to one certificate and not revoked according to another. One could reasonably argue that, in this situation, the two CRLs are in conflict about whether the certificate has been revoked, and either could apply. In particular, the outcome of an authorization decision would depend on which CRL is presented in support of a request. To avoid such nondeterminism, SPKI \[Ellison, Frantz, Lampson, Rivest, Thomas, and Ylonen 1999a, Section 5.2\] assumes that at any time, at most one CRL applies. We say a set $`C_R`$ of CRLs is consistent if it is not the case that there exist CRLs $`𝚌,𝚌^{}C_R`$, both issued by $`𝚔`$, with validity periods $`𝚅,𝚅^{}`$, respectively, such that $`𝚅𝚅^{}\mathrm{}`$. Restricting to consistent sets of CRLs ensures that it is safe to take any relevant CRL not containing a certificate as evidence for the validity of that certificate, since there cannot exist a CRL contradicting this conclusion. This assumption supports the monotonicity of $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)`$, and is essentially what allows us to use a monotonic logic, even in the presence of revocation.999Of course, in practice, it may well be that a set of CRLs is inconsistent. Both the SPKI document and our paper are silent on what to do in this case.

The semantics of SPKI given in \[Ellison, Frantz, Lampson, Rivest, Thomas, and Ylonen 1999a\] is in terms of tuple reduction. However, the presentation of how the tuples are intended to be used to make an authorization decision is not completely formal. \[SPKI Working Group 1998, Section 6\] states that “Uses of names are replaced with simple definitions (keys …), based on the name definitions available from reducing name 4-tuples” and that “Authorization 5-tuples are then reduced to a final authorization decision”. The rule for 5-tuple reduction required for the latter step is explicitly described (in \[Ellison, Frantz, Lampson, Rivest, Thomas, and Ylonen 1999a, Section 6.3\]); it combines two 5-tuples to produce another 5-tuple:

1. $`𝚔_1,𝚔_2,\mathrm{𝑡𝑟𝑢𝑒},𝙰_1,𝚅_1+𝚔_2,𝚙,𝙳_2,𝙰_2,𝚅_2𝚔_1,𝚙,𝙳_2,𝙰_1𝙰_2,𝚅_1𝚅_2`$.101010SPKI uses $`\mathrm{𝚅𝚒𝚗𝚝𝚎𝚛𝚜𝚎𝚌𝚝}`$ to denote the intersection of timing expressions; we use the simple $``$ symbol here. The intersection of timing intervals is defined in the obvious way. If $`𝚅_1𝚅_2`$ is empty, then $`𝚅_1𝚅_2=\mathrm{}`$, since we are using $`\mathrm{}`$ to denote the empty interval.

Intuitively, if $`𝚔_1`$ permits $`𝚔_2`$ to delegate authority to the actions in $`𝙰_1`$ during $`𝚅_1`$ and $`𝚔_2`$ gives $`𝚙`$ authority over the actions in $`𝙰_2`$ (and to further delegate authority, if $`𝙳_2`$ is $`\mathrm{𝑡𝑟𝑢𝑒}`$) for the interval $`𝚅_2`$, then this is tantamount to $`𝚔_1`$ giving authority to $`𝚙`$ over the actions in $`𝙰_1𝙰_2`$ (and to further delegate authority, if $`𝙳_2`$ is $`\mathrm{𝑡𝑟𝑢𝑒}`$) for the interval $`𝚅_1𝚅_2`$.

The way that 4-tuples are to be reduced is slightly less transparent. The discussion of 4-tuple reduction in \[Ellison, Frantz, Lampson, Rivest, Thomas, and Ylonen 1999a, Section 6.4\] does not describe rules by which 4-tuples may be reduced, but rather shows how fully qualified names may be rewritten using 4-tuples. However, the discussion suggests the following rule for 4-tuple reduction:

1. $`𝚔_1,𝚗,𝚔_2\text{’s}𝚖\text{’s}𝚙,𝚅_1+𝚔_2,𝚖,𝚔_3,𝚅_2𝚔_1,𝚗,𝚔_3\text{’s}𝚙,𝚅_1𝚅_2`$.

We allow $`𝚙`$ to be the empty string in this rule, treating an expression of the form $`𝚛\text{’s}𝚙`$ as equal to $`𝚛`$ in this case, to avoid the need for stating the rule that results from replacing $`𝚔_2\text{’s}𝚖\text{’s}𝚙`$ by $`𝚔_2\text{’s}𝚖`$ and replacing $`𝚔_3\text{’s}𝚙`$ by $`𝚔_3`$. We use this convention in stating other rules too. Intuitively, this rule says that if $`𝚔_1\text{’s}𝚗`$ is bound to $`𝚔_2\text{’s}𝚖\text{’s}𝚙`$ for the interval $`𝚅_1`$, and $`𝚔_2\text{’s}𝚖`$ is bound to $`𝚔_3`$ for the interval $`𝚅_2`$, then $`𝚔_1\text{’s}𝚗`$ will be bound to $`𝚔_3\text{’s}𝚙`$ for the interval $`𝚅_1𝚅_2`$.

The SPKI document also considers a generalization of this rule:

1. $`𝚔_1,𝚗,𝚔_2\text{’s}𝚖\text{’s}𝚙,𝚅_1+𝚔_2,𝚖,𝚚,𝚅_2𝚔_1,𝚗,𝚚\text{’s}𝚙,𝚅_1𝚅_2`$.

We consider in Section 5 the role of R2 vs. R2.

The step of the authorization decision process described as “Uses of names are replaced with simple definitions (keys …), based on the name definitions available from reducing name 4-tuples” is not further formalized. However, the following rule seems to capture this intuition:

1. $`𝚔_1,𝚔_2\text{’s}𝚗\text{’s}𝚙,𝙳,𝙰,𝚅_1+𝚔_2,𝚗,𝚔_3,𝚅_2𝚔_1,𝚔_3\text{’s}𝚙,𝙳,𝙰,𝚅_1𝚅_2`$.

Again, it is possible to generalize R3 much the same way as R2 generalizes R2.

1. $`𝚔_1,𝚔_2\text{’s}𝚗\text{’s}𝚙,𝙳,𝙰,𝚅_1+𝚔_2,𝚗,𝚚,𝚅_2𝚔_1,𝚚\text{’s}𝚙,𝙳,𝙰,𝚅_1𝚅_2`$.

As we shall see, the question of whether we use R2/R3 or R2/R3 has a nontrivial impact on the type of conclusions we can draw using tuple reduction; see, for example, Theorems 5.2 and 5.6.

SPKI intends that the tuple reduction rules play several different roles. Besides being used for specific authorization decisions, the tuple reduction process is intended to serve as a means of derivation of consequences of a set of certificates that can form the basis of a “certificate result certificate” that captures a set of authorizations that may be derived from a collection of certificates \[Ellison, Frantz, Lampson, Rivest, Thomas, and Ylonen 1999a, Section 6.6\]. As we shall see, in a precise sense, R1–3 suffice for making specific authorization decisions at a given time. However, to derive more general consequences of a set of certificates, we need to consider R2 and R3, as well as other rules discussed in Section 5. In the next section, we provide a semantics for SPKI that lets us provide semantics for the reduction rules; we then use that semantics in Section 5 to carefully examine the rules.

## 4 A logic for reasoning about SPKI

We now define a formal language $`_{\mathrm{𝑆𝑃𝐾𝐼}}(K,N,𝒜)`$ for reasoning about SPKI. $`_{\mathrm{𝑆𝑃𝐾𝐼}}(K,N,𝒜)`$ is an extension of the language LLNC defined in \[Halpern and van der Meyden 2001\]. The parameters $`N`$ and $`𝒜`$ (the set of names and the set of action expressions) do not play a significant role. However, for some of our results, the cardinality of the set $`K`$ does play a role. To simplify the notation, we often omit the parameters that play no significant role, and write, for example, $`_{\mathrm{𝑆𝑃𝐾𝐼}}`$ or $`_{\mathrm{𝑆𝑃𝐾𝐼}}(K)`$. We do the same in all other contexts where these parameters are used.

### 4.1 Syntax

Following \[Halpern and van der Meyden 2001\], given a set $`K`$ of keys and a set $`N`$ of local names, we define a principal expression (over $`K`$ and $`N`$) to be either a key in $`K`$, a local name in $`N`$, or an expression of the form $`𝚙\text{’s}𝚚`$ where $`𝚙`$ and $`𝚚`$ are principal expressions. The compound names of SPKI/SDSI can be viewed as principal expressions. Note that parenthesization matters for principal expressions; for example, $`(𝚗_1\text{’s}𝚗_2)\text{’s}𝚗_3`$ is different from $`𝚗_1\text{’s}(𝚗_2\text{’s}𝚗_3)`$. However, our semantics guarantees that the combination of names is associative, so that, in fact, the two principal expressions are equivalent (see Lemma 4.2. For definiteness, we assume that all principal expressions that arise in naming and authorization certificates are parenthesized to the right.111111Recall that, in SPKI, names are just written as $`(\mathrm{𝚗𝚊𝚖𝚎}𝚗_\mathrm{𝟷}\mathrm{}𝚗_𝚔)`$, so there is no parenthesization involved at all.

The primitives of $`_{\mathrm{𝑆𝑃𝐾𝐼}}(K,N,𝒜)`$ consist of

* principal expressions over $`K`$ and $`N`$;
* the set $`𝒞^+(K,N,𝒜)`$ of naming, authorization and revocation certificates that can be formed from $`K`$, $`N`$, and $`𝒜`$;
* a special constant $`\mathrm{𝚗𝚘𝚠}`$;
* validity intervals $`𝚅`$ consisting of pairs $`[𝚝_1,𝚝_2]`$ of times in $`IN\{\mathrm{}\}`$ with $`𝚝_1𝚝_2`$, together with the empty interval $`\mathrm{}`$.

The set of formulas of $`_{\mathrm{𝑆𝑃𝐾𝐼}}(K,N,𝒜)`$ is the smallest set such that

1. if $`𝚙`$ and $`𝚚`$ are principal expressions then $`𝚙𝚚`$ is a formula;
2. if $`𝚌𝒞(K,N,𝒜)`$, then $`𝚌`$ and $`\mathrm{𝑎𝑝𝑝𝑙𝑖𝑐}(𝚌)`$ are formulas;
3. if $`𝚔`$ is a key, $`𝚙`$ is a principal expression, and $`A𝒜`$, then $`\mathrm{𝑃𝑒𝑟𝑚}(𝚔,𝚙,A)`$ and $`\mathrm{𝐷𝑒𝑙}(𝚔,𝚙,A)`$ are formulas;
4. $`\mathrm{𝚗𝚘𝚠}V`$ is a formula;
5. if $`\varphi ,\psi `$ are formulas then $`\neg \varphi `$ and $`\varphi \psi `$ are formulas.

Intuitively, $`𝚙𝚚`$ says that all the keys in $`𝚚`$ are bound to $`𝚙`$. Since principal expressions are associated with sets of keys, this just says that the keys associated with $`𝚚`$ are a subset of those associated with $`𝚙`$. The formula $`𝚌`$ is true at a time $`𝚝`$ if the certificate $`𝚌`$ was issued before $`𝚝`$. (To make sense of this, the semantic object which determines whether formulas are true must include a list of the certificates that have been issued and the current time.) The formula $`\mathrm{𝑎𝑝𝑝𝑙𝑖𝑐}(𝚌)`$ is true at a time $`𝚝`$ if $`𝚌`$ is either irrevocable or if it is revocable, but is known not to have been revoked at time $`𝚝`$. Although we read $`\mathrm{𝑎𝑝𝑝𝑙𝑖𝑐}(𝚌)`$ as “$`𝚌`$ is applicable”, it is worth noting that $`\mathrm{𝑎𝑝𝑝𝑙𝑖𝑐}(𝚌)`$ could be true at time $`𝚝`$ even if $`𝚌`$ was not issued before time $`𝚝`$ or its validity interval does not include $`𝚝`$. There are other formulas in the logic that enable us to say that $`𝚌`$ has been issued (namely, the formula $`𝚌`$) and that the current time is in a given validity interval (namely, $`\mathrm{𝚗𝚘𝚠}V`$). Finally, as the notation suggests, the formula $`\mathrm{𝑃𝑒𝑟𝑚}(𝚔,𝚙,A)`$ says that $`𝚔`$ permits $`𝚙`$ to perform the actions in $`A`$ and $`\mathrm{𝐷𝑒𝑙}(𝚔,𝚙,A)`$ says that $`𝚔`$ permits $`𝚙`$ to delegate authority over the actions in $`A`$.

LLNC can be viewed as the fragment of $`_{\mathrm{𝑆𝑃𝐾𝐼}}`$ where the only certificates allowed are those of the form $`(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚗𝚙)`$, which corresponds to the LLNC formula $`𝚔\mathrm{𝑐𝑒𝑟𝑡}𝚗𝚙`$. There are no formulas in LLNC of the form $`\mathrm{𝚗𝚘𝚠}𝚅`$, $`\mathrm{𝑃𝑒𝑟𝑚}(𝚔,𝚙,A)`$, $`\mathrm{𝐷𝑒𝑙}(𝚔,𝚙,A)`$, or $`\mathrm{𝑎𝑝𝑝𝑙𝑖𝑐}(𝚌)`$ (since there is no notion of time in LLNC, and permission, delegation, and revocation are not treated).121212LLNC does allow formulas of the form $`𝚔\mathrm{𝑐𝑒𝑟𝑡}\varphi `$ for arbitrary formulas $`\varphi `$. However, if $`\varphi `$ is not of the form $`𝚗𝚙`$, then such formulas do not interact with the other constructs under the semantics of \[Halpern and van der Meyden 2001\]. Thus, LLNC does not gain additional expressive power from such formulas. Following SDSI, LLNC also has a notion of a global name. Since global names have been omitted in SPKI, we omit them in $`_{\mathrm{𝑆𝑃𝐾𝐼}}`$ as well.

### 4.2 Semantics

The semantics for $`_{\mathrm{𝑆𝑃𝐾𝐼}}`$ extends that of LLNC. We begin by outlining the main components of the semantic model.

In LLNC, there is a notion of a world. A world essentially describes which certificates have been issued. Since now we have time in the picture, we need a temporal analogue of a world. This is a run. Formally, a $`(K,N,𝒜)`$-run is a function $`r:IN𝒫(𝒞^+(K,N,𝒜))`$. (We use $`𝒫(X)`$ to denote the set of subsets of $`X`$ here and elsewhere). We are implicitly assuming a global clock and are taking time with respect to that global clock. Intuitively, $`r(𝚝)`$ is the set of appropriately signed certificates issued at time $`𝚝`$. That is, if $`𝚌`$ is a certificate, then $`𝚌r(𝚝)`$ if a certificate with contents $`𝚌`$ is issued at time $`𝚝`$ in run $`r`$. For compatibility with the SPKI document, we assume that the set of revocation certificates issued in $`r`$ (that is, the set of revocation certificates in $`_{𝚝IN}r(𝚝)`$) is consistent: there cannot be two CRLs with the same issuer whose validity intervals overlap.

As we said before, we assume that there is a set $`𝒜`$ of action expressions, which represent sets of actions in a set $`\mathrm{𝐴𝑐𝑡}`$, and a fixed action interpretation $`\alpha _𝒜`$ that maps expressions in $`𝒜`$ to subsets of $`\mathrm{𝐴𝑐𝑡}`$.

To interpret local names, LLNC has a construct called a local name assignment that associates with each key $`𝚔`$ and local name $`𝚗`$ the set of keys bound to $`𝚗`$ by $`𝚔`$. There is an analogous function here, but it now takes a time as an argument, since the association may vary over time. In addition, to take into account the new constructs in $`_{\mathrm{𝑆𝑃𝐾𝐼}}`$, there is a function that associates with each key $`𝚔`$, local name $`𝚗`$, and time $`𝚝`$ the set of actions that $`𝚔`$ has granted each other principal permission to perform, and describes whether or not that permission can be delegated. These functions can be extended from local names to all principal expressions; see below.

Formally,

* a (temporal) local name assignment (for $`K`$ and $`N`$) is a function $`L:K\times N\times IN𝒫(K)`$. Intuitively, for $`𝚔K`$, $`𝚗N`$ and $`𝚝IN`$, the set $`L(𝚔,𝚗,𝚝)`$ contains the keys associated at time $`𝚝`$ with the name $`𝚗`$ in $`𝚔`$’s name space.
* a (temporal) permission/delegation assignment (for $`K`$ and $`\mathrm{𝐴𝑐𝑡}`$) is a function $`P:K\times IN\times K\times \mathrm{𝐴𝑐𝑡}\{0,1,2\}`$ such that if $`P(𝚔_1,𝚝,𝚔_2,𝚊)=2`$ and $`P(𝚔_2,𝚝,𝚔_3,𝚊)=i`$, then $`P(𝚔_1,𝚝,𝚔_3,𝚊)i`$. Intuitively, $`P(𝚔,𝚝,𝚔^{},𝚊)`$ is 0 if at time $`𝚝`$, $`𝚔`$ has not granted $`𝚔^{}`$ the right to perform or delegate $`𝚊`$; it is 1 if principal $`𝚔`$ has granted permission to principal $`𝚔^{}`$ to perform action $`𝚊`$; it is 2 if, in addition, principal $`𝚔`$ has delegated authority to principal $`𝚔^{}`$ to propagate the right to perform action $`𝚊`$.131313As noted in \[SPKI Working Group 1998\], there is not much point to having a principal able to propagate the right to perform an action without having the right to perform it, since the principal may always grant itself that right. The meaning of the right to propagate is captured by the condition above: if, at time $`𝚝`$, $`𝚔_1`$ has granted $`𝚔_2`$ the right to propagate permission to perform $`𝚊`$, and $`𝚔_2`$ has granted permission to perform (propagate) $`𝚊`$, then, according to $`𝚔_1`$, principal $`𝚔_3`$ has the right to perform (propagate) $`𝚊`$. The reason that the condition says $`P(𝚔_1,𝚝,𝚔_3,𝚊)i`$ rather than $`P(𝚔_1,𝚝,𝚔_3,𝚊)=i`$ is that if $`i=1`$, for example, it is possible that $`𝚔_1`$ independently granted $`𝚔_3`$ the right to delegate $`𝚊`$, so that $`P(𝚔_1,𝚝,𝚔_3,𝚊)=2`$.

A $`(K,N,\mathrm{𝐴𝑐𝑡})`$ interpretation $`\pi `$ is a tuple $`L,P`$ consisting of a local name assignment $`L`$ for $`K`$ and $`N`$ and a permission/delegation assignment $`P`$ for $`K`$ and $`\mathrm{𝐴𝑐𝑡}`$. We omit the modifier $`(K,N,\mathrm{𝐴𝑐𝑡})`$ when it is not relevant to the discussion. However, it is important to note that the parameters that characterize the language also characterize the interpretations.

Given a local name assignment $`L`$, a key $`𝚔`$, and a time $`𝚝IN`$, we can assign to each principal expression $`𝚙`$ a set of keys $`[[𝚙]]_{L,𝚔,𝚝}`$. This set is defined by the following recursion:

* $`[[𝚔^{}]]_{L,𝚔,𝚝}=\{𝚔^{}\}`$, if $`𝚔^{}K`$ is a key,
* $`[[𝚗]]_{L,𝚔,𝚝}=L(𝚔,𝚗,𝚝)`$, if $`𝚗N`$ is a local name,
* $`[[𝚙\text{’s}𝚚]]_{L,𝚔,𝚝}=\{[[𝚚]]_{L,𝚔^{},𝚝}|𝚔^{}[[𝚙]]_{L,𝚔,𝚝}\}`$.

This definition is essentially identical to that in \[Abadi 1998, Halpern and van der Meyden 2001\], except that we have made the interpretation of local names depend on the time of evaluation.

It is now easy to prove some basic facts about principal expressions. First, we can show that a fully-qualified name is independent of the key.

###### Lemma 4.1

: If $`𝚙`$ is a fully qualified principal expression, then $`[[𝚙]]_{L,𝚔,𝚝}=[[𝚙]]_{L,𝚔^{},𝚝}`$ for all keys $`𝚔`$ and $`𝚔^{}`$.

Proof: By an easy induction on the structure of $`𝚙`$.

We also make precise our claim that the combination of names is associative.

###### Lemma 4.2

: For all principal expressions $`𝚙_1`$, $`𝚙_2`$, and $`𝚙_3`$, keys $`𝚔`$, and local name assignment $`L`$,

$$[[𝚙_1\text{’s}(𝚙_2\text{’s}𝚙_3)]]_{L,𝚔,𝚝}=[[(𝚙_1\text{’s}𝚙_2)\text{’s}𝚙_3]]_{L,𝚔,𝚝}.$$

Proof: By unwinding the definitions, it immediately follows that both $`[[𝚙_1\text{’s}(𝚙_2\text{’s}𝚙_3)]]_{L,𝚔,𝚝}`$ and $`[[(𝚙_1\text{’s}𝚙_2)\text{’s}𝚙_3]]_{L,𝚔,𝚝}`$ are equal to

$$\{[[𝚙_3]]_{L,𝚔_2,𝚝}:𝚔_2[[𝚙_2]]_{L,𝚔_1,𝚝},𝚔_1[[𝚙_1]]_{L,𝚔,𝚝}\}.$$

In order to capture the impact that CRLs have on the interpretation of naming and authorization certificates, we say that a certificate $`𝚌`$ is applicable at time $`𝚝`$ in a run $`r`$ if either $`𝚌`$ is not revocable, or $`𝚌`$ is revocable by a key $`𝚔_r`$ and for some $`𝚝^{}𝚝`$ we have $`(\mathrm{𝚌𝚛𝚕}𝚔_r(\mathrm{𝚌𝚊𝚗𝚌𝚎𝚕𝚎𝚍}𝚌_\mathrm{𝟷},\mathrm{},𝚌_𝚗)𝚅)r(𝚝^{})`$ for some $`(𝚌_\mathrm{𝟷},\mathrm{},𝚌_𝚗)`$ such that $`𝚌`$ is not one of the $`𝚌_i`$, and $`𝚝𝚅`$. Roughly speaking, this says that $`𝚌`$ is applicable at time $`𝚝`$ if has been declared not to have been revoked at $`𝚝`$ (under the assumption that at most one CRL is applicable at any given time). Note that a certificate $`𝚌`$ may be applicable at a time $`𝚝`$ outside its validity interval.

We now define what it means for a formula $`\varphi `$ to be true at a run $`r`$ with respect to an interpretation $`\pi =L,P`$, a key $`𝚔`$, and a time $`𝚝`$, written $`r,\pi ,𝚔,𝚝\varphi `$, by induction on the structure of $`\varphi `$:

* $`r,\pi ,𝚔,𝚝𝚙𝚚`$ if $`[[𝚙]]_{L,𝚔,𝚝}[[𝚚]]_{L,𝚔,𝚝}`$,
* $`r,\pi ,𝚔,𝚝𝚌`$ if $`𝚌r(𝚝^{})`$ for some $`𝚝^{}𝚝`$,
* $`r,\pi ,𝚔,𝚝\mathrm{𝑃𝑒𝑟𝑚}(𝚔_1,𝚙,A)`$ if for all $`𝚔_2[[𝚙]]_{L,𝚔_1,𝚝}`$ and all $`𝚊\alpha _𝒜(A)`$, we have $`P(𝚔_1,𝚝,𝚔_2,𝚊)1`$,
* $`r,\pi ,𝚔,𝚝\mathrm{𝐷𝑒𝑙}(𝚔_1,𝚙,A)`$ if for all $`𝚔_2[[𝚙]]_{L,𝚔_1,𝚝}`$ and all $`𝚊\alpha _𝒜(A)`$, we have $`P(𝚔_1,𝚝,𝚔_2,𝚊)=2`$,
* $`r,\pi ,𝚔,𝚝\mathrm{𝚗𝚘𝚠}V`$ if $`𝚝V`$,
* $`r,\pi ,𝚔,𝚝\mathrm{𝑎𝑝𝑝𝑙𝑖𝑐}(𝚌)`$ if $`𝚌`$ is applicable at time $`𝚝`$ in $`r`$,
* $`r,\pi ,𝚔,𝚝\varphi \psi `$ if $`r,\pi ,𝚔,𝚝\varphi `$ and $`r,\pi ,𝚔,𝚝\psi `$,
* $`r,\pi ,𝚔,𝚝\neg \varphi `$ if not $`r,\pi ,𝚔,𝚝\varphi `$.

We write $`r,\pi \varphi `$ if $`r,\pi ,𝚔,𝚝\varphi `$ for all principals $`𝚔K`$ and all times $`𝚝IN`$.

In the definitions so far, there is no connection between the run and the interpretation. Intuitively, we would like the interpretation, which contains information about the meaning of local names and permissions and delegations, to be determined from the information about the certificates that have been issued at each point in time that is represented in the run. We connect these ideas by means of the following definition. The interpretation $`\pi =L,P`$ is consistent with a run $`r`$ if, for all times $`𝚝IN`$,

1. for all naming certificates $`𝚌=(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚗𝚙𝚅𝚔_r)`$ in $`_{𝚝^{}𝚝}r(𝚝^{})`$, if $`𝚝V`$ and $`𝚌`$ is applicable at $`𝚝`$ in $`r`$, then $`[[𝚗]]_{L,𝚔,𝚝}[[𝚙]]_{L,𝚔,𝚝}`$;
2. for all authorization certificates $`𝚌=(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚙`$ $`𝙳𝙰𝚅𝚔_r)`$ in $`_{𝚝^{}𝚝}r(𝚝^{})`$, if $`𝚝V`$ and $`𝚌`$ is applicable at $`𝚝`$ in $`r`$, then for all $`𝚊\alpha _𝒜(𝙰)`$ and all keys $`𝚔^{}[[𝚙]]_{L,𝚔,𝚝}`$, we have

1. $`P(𝚔,𝚝,𝚔^{},𝚊)1`$,
    2. if $`𝙳=\mathrm{𝚝𝚛𝚞𝚎}`$ then $`P(𝚔,𝚝,𝚔^{},𝚊)=2`$.

In general, an interpretation can be consistent with a run while allowing facts to hold that do not follow from the certificates issued in the run. For an extreme example of this, let $`r`$ be the run in which no certificates are ever issued, and suppose that $`\pi `$ is the maximal interpretation, where $`L(𝚔,𝚗,𝚝)=K`$ and $`P(𝚔,𝚝,𝚔^{},𝚊)=2`$ for all keys $`𝚔`$, $`𝚔^{}`$, local names $`𝚗`$, actions $`𝚊`$, and times $`𝚝`$. Then $`\pi `$ is consistent with $`r`$. This is undesirable. Intuitively, we would like facts concerning rights and the meaning of local names to hold only if they are forced to do so by some certificate. To enforce this, we restrict the interpretation to be the minimal one consistent with the run. Our technique for doing so extends that used in \[Halpern and van der Meyden 2001\].

Formally, define an order $``$ on $`(K,N,\mathrm{𝐴𝑐𝑡})`$ interpretations by $`L,P,L^{},P^{}`$ if, for all keys $`𝚔`$, local names $`𝚗`$, and times $`𝚝`$, we have $`L(𝚔,𝚗,𝚝)L^{}(𝚔,𝚗,𝚝)`$ and for all keys $`𝚔^{}`$ and actions $`𝚊`$, we have $`P(𝚔,𝚝,𝚔^{},𝚊)P^{}(𝚔,𝚝,𝚔^{},𝚊)`$. Thus, $`L,PL^{},P^{}`$ if, for all $`𝚗`$, $`𝚔`$, and $`𝚝`$, at least as many keys are bound to $`𝚗`$ by $`𝚔`$ at time $`𝚝`$ in $`L^{}`$ as in $`L`$. In addition, at least as many keys are authorized to perform action $`𝚊`$ by $`𝚔`$ at time $`𝚝`$ in $`P^{}`$ as in $`P`$ and, of those keys authorized to perform the action $`𝚊`$, at least as many can delegate that authority in $`P^{}`$ as in $`P`$.

This order can easily be seen to give the set of $`(K,N,\mathrm{𝐴𝑐𝑡})`$ interpretations the structure of a lattice. Say that an element $`\pi `$ of a set $`S`$ of interpretations is minimal in $`S`$ if $`\pi \pi ^{}`$ for all $`\pi ^{}S`$.

###### Proposition 4.3

: For every run $`r`$, there exists a unique $`(K,N,\mathrm{𝐴𝑐𝑡})`$ interpretation minimal in the set of $`(K,N,\mathrm{𝐴𝑐𝑡})`$ interpretations consistent with $`r`$.

Proof: See the appendix.

We write $`\pi _r`$ for the minimal interpretation consistent with $`r`$. Intuitively, in the minimal interpretation consistent with $`r`$, there are no name bindings, permissions, or delegations that are not forced by $`r`$. Enforcing the requirement that the interpretation should be the minimal one consistent with the run leads to a variant of the semantics discussed above. We write $`r,𝚔,𝚝_c\varphi `$ if $`r,\pi _r,𝚔,𝚝\varphi `$. We say that a formula $`\varphi `$ is cl-valid (with respect to $`K,N,\mathrm{𝐴𝑐𝑡}`$) in $`_{\mathrm{𝑆𝑃𝐾𝐼}}(K,N,\mathrm{𝐴𝑐𝑡})`$, written $`_{\mathrm{𝑐𝑙},K,N,\mathrm{𝐴𝑐𝑡}}\varphi `$, if $`r,𝚔,𝚝_c\varphi `$ for all $`(K,N,\mathrm{𝐴𝑐𝑡})`$-runs $`r`$, keys $`𝚔K`$, and times $`𝚝`$. (The “cl” stands for closed, since in \[Halpern and van der Meyden 2001\] the semantics corresponding to $`_{\mathrm{𝑐𝑙}}`$ is termed the closed semantics, while the semantics corresponding to $``$ was termed the open semantics. We use “cl” here rather than “c” as in \[Halpern and van der Meyden 2001\] to denote the closed semantics, to avoid confusion with $`𝚌`$, which ranges over certificates.) The closed semantics is the one of most interest to us here, since it enforces the desired close connection between the certificates actually issued and the name bindings, permissions, and delegations. The open semantics is mainly used as a stepping-stone to defining the closed semantics. Validity with respect to the open semantics can also be viewed as capturing what is guaranteed to hold, no matter what additional certificates are issued. Interestingly, as shown in \[Halpern and van der Meyden 2001\], validity with respect to the open and closed semantics coincide for the logic LLNC. We believe that they also coincide for the logic $`_{\mathrm{𝑆𝑃𝐾𝐼}}`$, although we have not checked carefully.

It is not hard to check that the subscripts $`N`$ and $`\mathrm{𝐴𝑐𝑡}`$ play no role in $`_{\mathrm{𝑐𝑙},K,N,𝒜}`$; if a formula is valid for some choice of $`N`$ and $`\mathrm{𝐴𝑐𝑡}`$ (for a fixed $`K`$), then it is valid for all choices of $`N`$ and $`\mathrm{𝐴𝑐𝑡}`$. However, as observed in \[Halpern and van der Meyden 2001\] (where a complete axiomatization for LLNC was provided), the axioms do depend on the choice of $`K`$; in particular, they depend on the cardinality of $`K`$. For example, suppose $`K`$ has just one element, say $`𝚔`$. Then it is easy to see that $`_{\mathrm{𝑐𝑙},K,N,\mathrm{𝐴𝑐𝑡}}𝚗𝚔𝚔\text{’s}𝚗𝚔\text{’s}𝚖`$, for all $`𝚗,𝚖N`$. Since $`𝚗`$ is bound to $`𝚔`$, it follows that the interpretation of $`𝚔\text{’s}𝚗`$ must be $`\{𝚔\}`$, since $`𝚔`$ is the only key. Thus, the interpretation of $`𝚔\text{’s}𝚗`$ must be a superset of interpretation of $`𝚔\text{’s}𝚖`$, and so $`𝚔\text{’s}𝚗𝚔\text{’s}𝚖`$ holds. However, this argument depends critically on the assumption that $`K=\{𝚔\}`$. The formula $`𝚗𝚔𝚔\text{’s}𝚗𝚔\text{’s}𝚖`$ is not valid if there are at least two keys: If $`𝚔^{}`$ is a key distinct from $`𝚔`$, then it is possible that $`𝚔^{}`$ is bound to $`𝚔\text{’s}𝚖`$ and not bound to $`𝚔\text{’s}𝚗`$. In light of this discussion, we omit $`N`$ and $`\mathrm{𝐴𝑐𝑡}`$ from the subscript from here on in, but include $`K`$ when it plays an important role.

We can now make precise the intuition that in the minimal interpretation only name bindings and permissions and delegations forced by $`r`$ hold. Define the formula associated with the naming certificate $`𝚌=(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚗𝚙𝚅𝚔_r)`$ to be

$$\mathrm{𝚗𝚘𝚠}V(𝚔\text{’s}𝚗𝚙).$$

Similarly, the formula associated with the authorization certificate $`𝚌=(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚙𝙳𝙰𝚅𝚔_r)`$ is

$$\mathrm{𝚗𝚘𝚠}V[\mathrm{𝑃𝑒𝑟𝑚}(𝚔,𝚙,𝙰)(𝙳\mathrm{𝐷𝑒𝑙}(𝚔,𝚙,𝙰))].$$

Let $`\varphi _𝚌`$ be the formula associated with certificate $`𝚌𝒞`$.

###### Proposition 4.4

: The interpretation $`\pi `$ is consistent with a run $`r`$ iff for all times $`𝚝IN`$, keys $`𝚔K`$, and $`𝚌𝒞`$, we have $`r,\pi ,𝚔,𝚝𝚌\mathrm{𝑎𝑝𝑝𝑙𝑖𝑐}(𝚌)\varphi _𝚌`$.

Proof: Immediate from the definition of consistency.

Note that it follows from Proposition 4.4 that if $`\pi `$ is an interpretation consistent with run $`r`$ and a certificate $`𝚌𝒞`$ was issued in $`r`$ at or before time $`𝚝`$ and remains applicable at $`𝚝`$, then $`r,\pi ,𝚔,𝚝\varphi _c`$. Moreover, the minimal interpretation associated with $`r`$ is the minimal intepretation $`\pi `$ satisfying $`r,\pi ,𝚔,𝚝\varphi _c`$ for all certificates $`𝚌𝒞`$ that have been issued in $`r`$ at or before time $`𝚝`$ and remain applicable at $`𝚝`$. In this sense, the formulas associated with certificates precisely capture their meaning. It is also worth noting that $`_{\mathrm{𝑐𝑙}}𝚌\mathrm{𝑎𝑝𝑝𝑙𝑖𝑐}(𝚌)\varphi _𝚌`$ for all $`𝚌𝒞`$.

## 5 Soundness and completeness of tuple reduction

We are now in a position to compare the SPKI tuple reduction rules to our semantics. Intuitively, we would like to understand tuple reduction as drawing inferences about the run based on evidence provided in the certificates presented to the verifier. Thus, we want to show that all conclusions based on tuple reduction are true under our semantics and, conversely, all valid conclusions about bindings and authorizations that follow from the issuing of certain certificates are derivable from those certificates using tuple reductions. More precisely, we want to show that, given a finite set $`CC_R`$ of certificates, where $`C`$ consists of naming and authorization certificates and $`C_R`$ consists of CRLs, we have $`_{\mathrm{𝑐𝑙}}(_{𝚌^{}CC_R}𝚌^{})\varphi _𝚌`$ iff $`\tau _𝚌`$ can be derived from the tuples in $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)`$, using the tuple reduction rules. This can be broken up into two questions:

* soundness: if $`\tau _𝚌`$ can be derived from the tuples in $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)`$ using the tuple reduction rules, then $`_{\mathrm{𝑐𝑙}}(_{𝚌^{}CC_R}𝚌^{})\varphi _𝚌`$;
* completeness: if $`_{\mathrm{𝑐𝑙}}(_{𝚌^{}CC_R}𝚌^{})\varphi _𝚌`$, then $`\tau _𝚌`$ can be derived from the tuples in $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)`$ using the tuple reduction rules.

Of course, whether soundness and completeness hold depend in large part on which reduction rules are used. We are particularly interested in questions such as whether R2 and R3 are needed to derive all conclusions of interest about certificates and, if not, what conclusions they can be used to derive.

Showing that the tuple reduction rules discussed earlier are sound with respect to the $`_{\mathrm{𝑆𝑃𝐾𝐼}}`$ semantics is straightforward. To make this precise, if $`T`$ is a set of tuples and $`\tau `$ is a tuple, we write $`T_0^{}\tau `$ if there exists a sequence of tuples $`\tau _1,\mathrm{},\tau _k`$ such that $`\tau _k=\tau `$ and for each $`ik`$ either $`\tau _iT`$ or there exist $`j,j^{}<i`$ such that $`\tau _j+\tau _j^{}\tau _i`$ is an instance of one of R1, R2, or R3.

###### Theorem 5.1

: Suppose that $`C`$ is a finite subset of $`𝒞`$, $`C_R`$ is a finite set of CRLs, and $`𝚌𝒞`$. If $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}\tau _𝚌`$, then $`_c\left(_{𝚌^{}CC_R}𝚌^{}\right)\varphi _𝚌`$.

Since Theorem 5.1 is a special case of a more general soundness result, Theorem 5.3, we defer the proof until after the statement of the latter theorem.

Completeness is not at all straightforward; indeed, it does not hold for R1–R3. What does hold is a weak version of completeness. To understand this in more detail, we need a few definitions.

A concrete certificate is one whose corresponding tuple has the form $`𝚔,𝚗,𝚔^{},[𝚝,𝚝]`$ (in the case of naming certificates) or $`𝚔,𝚔^{},𝙳,\{𝚊\},[𝚝,𝚝]`$ (in the case of authorization certificates). That is, concrete certificates talk about the keys that are bound to names and the keys that are authorized to perform certain actions, and are concerned only with a single point in time and single actions.

The following result shows that R1, R2, and R3 suffice in a certain sense to deal with concrete certificates. We say that a naming certificate with 4-tuple $`𝚔,𝚗,𝚙,𝚅`$ subsumes a naming certificate with 4-tuple $`𝚔,𝚗,𝚙,𝚅^{}`$ if $`𝚅𝚅^{}`$. Similarly an authorization certificate with 5-tuple $`𝚔,𝚙,𝙳,𝙰,𝚅`$ subsumes an authorization certificate with 5-tuple $`𝚔,𝚙,𝙳^{},𝙰^{},𝚅^{}`$ if $`𝚅𝚅^{}`$ and $`\alpha _𝒜(𝙰)\alpha _𝒜(𝙰^{})`$ and $`𝙳𝙳^{}`$ is valid. (Recall that we have assumed that it is possible to tell if one action expression is a superset of another.) Clearly if $`𝚌`$ subsumes $`𝚌^{}`$, then $`_{\mathrm{𝑐𝑙}}\varphi _𝚌\varphi _𝚌^{}`$.

###### Theorem 5.2

: If $`𝚌`$ is a concrete certificate, $`C`$ is a finite subset of $`𝒞`$, $`C_R`$ is a finite set of CRLs, and $`_c\left(_{𝚌^{}CC_R}𝚌^{}\right)\varphi _𝚌`$, then there exists a certificate $`𝚌^{}`$ that subsumes $`𝚌`$ such that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}\tau _𝚌^{}`$.

Proof: See the appendix.

Theorem 5.2 tells us that if all we want to do is to check if a given key is currently bound to a given name or if a given key is currently authorized to perform a given action, then R1–R3 essentially suffice. (Clarke et al. (?) establish a closely related result. They define the semantics of names operationally using just R2’ (which they call rule composition), and then establish that all conclusions about whether a given key is bound to a given name can be derived using just R2.)

However, R1–R3 do not suffice if we want to do full-fledged reasoning about the consequences of a set of certificates. For example, in general, R1–R3 may not suffice to draw a conclusion of the form $`𝚔\text{’s}𝚗𝚙`$, where $`𝚙`$ is an arbitrary principal expression, even though it may be a logical consequence of the certificates issued. Such conclusions are of interest in the context of “certificate result certificates” (\[Ellison, Frantz, Lampson, Rivest, Thomas, and Ylonen 1999a\], Section 6.7), which are new certificates stating facts that are consequences of a set of certificates previously issued. Certificate result certificates help to reduce the amount of work a relying party needs to do when processing a request.

There are three impediments to getting a full completeness theorem that is a converse to Theorem 5.1. The first two are easily dealt with by adding rules.

First, we want to get rid of the restriction that allows conclusions only about keys. R2 and R3 do not suffice for this. For example, let $`𝚌_1`$, $`𝚌_2`$, and $`𝚌_3`$ be irrevocable naming certificates whose corresponding 4-tuples are $`𝚔_1,𝚗,𝚔_2\text{’s}𝚖\text{’s}𝚙,[𝚝,𝚝]`$, $`𝚔_2,𝚖,𝚚,[𝚝,𝚝]`$, and $`𝚔_1,𝚗,𝚚\text{’s}𝚙,[𝚝,𝚝]`$, respectively. Clearly $`_{\mathrm{𝑐𝑙}}𝚌_1𝚌_2\varphi _{𝚌_3}`$. However, we cannot get $`\tau _{𝚌_3}`$ from $`\tau _{𝚌_1}`$ and $`\tau _{𝚌_2}`$, since the only rule that could possibly be of help, R2, applies only to 4-tuples whose third argument is a key. To deal with this problem, we need R2. Similarly, R3 is needed to deal with the analogous problem for R3. We also need the following trivial axiom to deal with a special case:

* $`𝚔,𝚗,𝚔\text{’s}𝚗,[0,\mathrm{}]`$.

(The fact that there is nothing to the left of the $``$ is meant to indicate that the conclusion on the right-hand side can be reached in all circumstances.)

A naming certificate is point-valued if its time interval has the form $`[t,t]`$. A concrete certificate is point-valued but a point-valued naming certificate can have as its third component an arbitrary fully-qualified expression. As we shall see, R0, R1, R2, and R3 essentially suffice to get us conclusions about point-valued naming certificates, but do not suffice to get us conclusions about arbitrary time intervals and sets of actions. To see that they do not suffice, consider three irrevocable naming certificates $`𝚌_1`$, $`𝚌_2`$, and $`𝚌_3`$ whose corresponding 4-tuples are $`𝚔,𝚗,𝚙,[1,2]`$, $`𝚔,𝚗,𝚙,[3,4]`$, and $`𝚔,𝚗,𝚙,[1,4]`$. Clearly $`_{\mathrm{𝑐𝑙}}𝚌_1𝚌_2\varphi _{𝚌_3}`$. However, we cannot get $`\tau _{𝚌_3}`$ from $`\tau _{𝚌_1}`$ and $`\tau _{𝚌_2}`$, since none of the reduction rules increase the size of intervals. Similar issues arise with 5-tuples.

There are a number of ways to deal with this. Perhaps the simplest is just to add the following reduction rule:

1. $`𝚔,𝚗,𝚙,𝚅_1+𝚔,𝚗,𝚙,𝚅_2𝚔,𝚗,𝚙,𝚅_3`$ if $`𝚅_1𝚅_2𝚅_3`$.
2. $`𝚔,𝚙,𝙳,𝙰,𝚅_1+𝚔,𝚙,𝙳,𝙰,𝚅_2𝚔,𝚙,𝙳,𝙰,𝚅_3`$ if $`𝚅_1𝚅_2𝚅_3`$.
3. $`𝚔,𝚙,𝙳_1,𝙰_1,𝚅+𝚔,𝚙,𝙳_2,𝙰_2,𝚅𝚔,𝚙,𝙳_3,𝙰_3,𝚅`$ if $`𝙳_3𝙳_1𝙳_2`$ is a tautology and $`\alpha _𝒜(𝙰_1)\alpha _𝒜(𝙰_2)\alpha _𝒜(𝙰_3)`$.

Note that the rule

$$𝚔,𝚗,𝚙,𝚅_1𝚔,𝚗,𝚙,𝚅_3\mathrm{if}𝚅_1𝚅_3$$

is a special case of R4(a) (taking $`𝚅_1=𝚅_2`$). Similar comments apply to R4(b) and R4(c). How easy it is to apply R4(c) depends on how easy it is to check that $`\alpha _𝒜(𝙰_1)\alpha _𝒜(𝙰_2)\alpha _𝒜(𝙰_3)`$. If action expressions can represent infinite sets of actions, this may be nontrivial. We do not address this issue here. Of course, it is trivial to determine if $`𝚅_1𝚅_2𝚅_3`$.

We write $`T_1^{}\tau `$ (resp., if $`T_2^{}\tau `$) if there is a derivation of $`\tau `$ from $`T`$ using rules R0, R1, R2, and R3 (resp., R0, R1, R2, R3, and R4). There is no difficulty showing that $`_2^{}`$ is sound. Note that the soundness of $`_0^{}`$ and $`_1^{}`$ follow as special cases.

###### Theorem 5.3

: Suppose that $`C`$ is a finite subset of $`𝒞`$, $`C_R`$ is a finite set of CRLs, and $`𝚌𝒞`$. If $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_2^{}\tau _𝚌`$, then $`_c\left(_{𝚌^{}CC_R}𝚌^{}\right)\varphi _𝚌`$. In fact, if $`\pi `$ is an interpretation consistent with a run $`r`$ and $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_2^{}\tau _𝚌`$, then $`r,\pi \left(_{𝚌^{}CC_R}𝚌^{}\right)\varphi _𝚌`$.

Theorem 5.3 follows easily from the following two propositions, whose straightforward proof we leave to the reader. The first shows that the process of transforming a set of certificates into a set of tuples corresponds to a valid inference in the logic.

###### Proposition 5.4

: Suppose that $`𝚌_1`$ is a revocable certificate in $`𝒞`$, $`𝚌_2`$ is a CRL such that $`𝚌_1`$ is live with respect to $`𝚌_2`$, and $`𝚌_3=\tau (𝚌_1,𝚌_2)`$. Then if $`\pi `$ is an interpretation consistent with a run $`r`$ and $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_2^{}\tau _𝚌`$, then $`r,\pi 𝚌_1𝚌_2\varphi _{𝚌_3}`$. Similarly, if $`𝚌`$ is an irrevocable certificate in $`𝒞`$, then $`r,\pi 𝚌\varphi _𝚌`$.

The second proposition shows that single reductions are sound with respect to the closed semantics.

###### Proposition 5.5

: Suppose that $`𝚌_1`$, $`𝚌_2`$, and $`𝚌_3`$ are certificates and $`\tau _{𝚌_1}+\tau _{𝚌_2}\tau _{𝚌_3}`$ is an instance of R1, R2, R3, or R4. Then

$$_c\varphi _{𝚌_1}\varphi _{𝚌_2}\varphi _{𝚌_3}.$$

Moreover, if $`\tau _𝚌`$ is an instance of R0, then $`_c\varphi _𝚌`$.

As we show shortly, R4 (together with R0, R1, R2, R3) suffices for completeness provided that the set of keys is infinite. It does not suffice if the set of keys is finite. As we have seen, the set of valid formulas depends on the cardinality of the set $`K`$ of keys. Consider the very simplest case where $`K`$ consists of only one key $`𝚔`$. Suppose that $`𝚖`$ and $`𝚗`$ are names in $`N`$. Let $`𝚌`$ and $`𝚌^{}`$ be irrevocable naming certificate whose 4-tuples are $`𝚔,𝚗,𝚔,𝚅`$ and $`𝚔,𝚗,𝚔\text{’s}𝚖,𝚅`$, respectively. It is easy to see that $`_{\mathrm{𝑐𝑙},K}𝚌\varphi _𝚌^{}`$. This is true for essentially the same reasons that $`_{\mathrm{𝑐𝑙},K}𝚗𝚔𝚔\text{’s}𝚗𝚔\text{’s}𝚖`$. On the other hand, $`_{\mathrm{𝑐𝑙},K}𝚌\varphi _𝚌^{}`$ does not hold if $`|K|2`$ (and, in particular, if $`K`$ is infinite). It easily follows that $`\tau _𝚌^{}`$ is not derivable from $`\{𝚌\}`$. Additional derivation rules would be necessary to allow this derivation.

With a little more effort, examples like this can be given as long as $`K`$ is finite. That is, if $`K`$ is finite, then there exist finite sets $`C𝒞(K,N,𝒜)`$ and $`C_R𝒞_R(K,N,𝒜)`$ and a naming certificate $`𝚌`$ such that $`_{\mathrm{𝑐𝑙},K}(_{𝚌^{}CC_R}𝚌^{})\varphi _𝚌`$, but $`\tau _𝚌`$ cannot be derived from $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)`$ using R0, R1, R2, R3, R4. Nevertheless, these reduction rules are “almost” complete. We show that, for any fixed set $`C𝒞^+(K,N,𝒜)`$, as long as $`|K|>|C|+|𝚌|`$, then for all sets $`C_R`$, we have $`_{\mathrm{𝑐𝑙},K}(_{𝚌^{}CC_R}𝚌^{})\varphi _𝚌`$ iff $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_2^{}𝚌`$. (Here $`|𝚌|`$ denotes the length of the certificate $`𝚌`$ as a string of symbols, and $`|C|`$ denotes the sum of the lengths of the certificates in the finite set $`C`$.)

###### Theorem 5.6

: If $`𝚌`$ is a certificate, $`C`$ is a finite subset of $`𝒞`$, $`C_R`$ is a finite set of CRLs, $`|K|>|C|+|𝚌|`$, and $`_{c,K}\left(_{𝚌^{}CC_R}𝚌^{}\right)\varphi _𝚌`$, then $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_2^{}\tau _𝚌`$; moreover, if $`𝚌`$ is a point-valued certificate, then $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}\tau _𝚌^{}`$ for some certificate $`𝚌^{}`$ subsuming $`𝚌`$.

Proof: See the appendix.

Basically, Theorem 5.6 says that, by using R2, R3, and R4 in the tuple reduction rules, we can derive all conclusions about certificates, provided that $`K`$ is not “small”, in the sense that $`|K||C|+|𝚌|`$. This proviso is not at all unreasonable. The set $`K`$ is, after all, intended to model the collection of potential public keys being used by the principals. In order for such a set of keys to be secure for signatures and encryption, it needs to be a very large set, so as to render brute force attacks on encrypted messages impractical (i.e., the key length needs to be large enough). By contrast, $`C`$ models a set of certificates generated by the principals and presented in a particular authorization request, and $`𝚌`$ is a particular certificate. We do not expect the size of these to be of the same order of magnitude as $`K`$, so we would expect that $`|K||C|+|𝚌|`$ will hold in practice. Another way to think about things is to understand $`K`$ as modelling the set of all keys that could ever be used, if we allow the key length to be made arbitrarily large. In this case $`K`$ is an infinite set, so we immediately have that $`|K||C|+|𝚌|`$. Thus, in a precise sense, the rules R0, R1, R2, R3, and R4 together give us all interesting conclusions about certificates.

## 6 Related Work

As mentioned in the introduction, there have been a number of other recent approaches to giving semantics to SPKI. In this section, we compare these approaches to ours.

Howell and Kotz (?) give a semantics to names that closely resembles the semantics of Abadi (?). In particular, a name is associated with a relation on possible worlds, rather than a set of keys as is the case in our semantics. We criticized Abadi’s semantics in our earlier paper \[Halpern and van der Meyden 2001\]; many of our criticisms apply to the Howell-Kotz semantics as well. Perhaps most significantly, the semantics for name binding (as Howell and Kotz themselves say) is rather opaque; it is hard to explain exactly what the meaning of the relation on worlds is. Their logic also uses a “speaks-for” relation $`𝚙𝚚`$, where $`𝚙,𝚚`$ are principal expressions, to capture both the binding relationship between names (similar to our use of $``$) and the notion that $`𝚚`$ has delegated certain rights to $`𝚙`$. As we argued in \[Halpern and van der Meyden 2001\], we believe that these are distinct notions that should be modeled using different constructs. Indeed, Howell and Kotz themselves note that their axiom

$$𝚙𝚚𝚙\text{’s}𝚗𝚚\text{’s}𝚗$$

is “suprisingly powerful” and needs to be “tempered”, particularly when one considers the related notion “speaks for on topic $`T`$”. In our logic, the formula

$$𝚙𝚚𝚙\text{’s}𝚗𝚚\text{’s}𝚗$$

is valid, but this is not a problem for us, since we do not interpret “$``$” as “speaks-for”.

Just as we do, Howell and Kotz translate SPKI certificates to formulas in their logic. There seem to be some problems with their translation, although there are not enough formal details in the paper for us to be really sure that these are in fact problematic.

* To capture the difference between just being given permission to perform an action and being given permission to delegate authority to perform the action, they split a real principal $`𝚔`$ into two principals $`𝚔_u`$ and $`𝚔_b`$; $`𝚔_b`$ is supposed to deal with the situation where $`𝚔`$ can delegate authority, while $`𝚔_u`$ is supposed to deal with the situation where $`𝚔`$ cannot delegate authority. There is no formal semantics given to $`𝚔_u`$ and $`𝚔_b`$, so it is not clear (to us) the extent to which this approach works.
* Their approach to dealing with time seems to involve talking about time explicitly in the formula. But there is no type corresponding to time in the semantics, so there is nothing to connect the statements about time to the actual time. Again, since the discussion of how time is handled is quite informal (with no examples), it is hard to tell how well it will work.

Howell and Kotz do claim that their semantics is sound with respect to tuple reduction; there is no discussion of completeness.

Aura (?) defines the notion of a delegation network, which is essentially a graphical description of a collection of certificates. Although he does not have a formal logic to reason about authorization, given a delegation network $`DN`$, he does define a relation authorizes$`{}_{DN}{}^{}(𝚔_1,𝚔_2,𝚊)`$, which can be read as “$`𝚔_1`$ authorizes $`𝚔_2`$ to perform $`𝚊`$”. Given a collection of SPKI certificates, Aura defines a corresponding authorization network $`DN`$ and obtains a certain type of soundness and completeness result for reduction. Very roughly speaking, given a collection of certificates with corresponding delegation network $`DN`$, authorizes$`{}_{DN}{}^{}(𝚔_1,𝚔_2,𝚊)`$ holds iff there is a sequence of delegation networks $`DN_1,\mathrm{},DN_m`$ such that $`DN_{i+1}`$ is obtained from $`DN_i`$ by certificate reduction in a precise sense and in $`DN_m`$ there is an explicit certificate issued by $`𝚔_1`$ authorizing $`𝚔_2`$ to perform $`𝚊`$. This is not a soundness and completeness result in the logical sense that we have here, although it provides what can be viewed as an operational semantics for the SPKI 5-tuple reduction rule R1. One of the main differences from our work is that, where we deal with principal expressions, Aura’s framework deals with an explicitly given set of keys; there is nothing in his paper that corresponds to our discussion of name reduction. Aura also does not seem to have time or revocation in his framework, nor does he consider the delegation bit. On the other hand, he does deal with threshold principals (as do Howell and Kotz), while we do not.

Li (?) has also considered the semantics of SPKI/SDSI. He presents a logic program, and provides results showing that this program derives the same set of concrete conclusions about SDSI names as 4-tuple reduction and SDSI’s name resolution procedure REF (?). He also provides an extension of the logic program intended to capture concrete conclusions about authorization certificates. However, he also does not explicitly treat timing and revocation, as we have done, and does not consider general reasoning such as that captured by our rules. On the other hand, he does discuss threshold subjects, which we have not treated. Another approach to formally capturing SPKI’s semantics is presented by Weeks (?) as an example of a more general framework for trust management in a functional programming style. This work does not attempt to prove any correspondence with the tuple reduction rules.

Also related to our results in this paper is the work of Clarke et al. \[Clarke, Elien, Ellison, Fredette, Marcos, and Rivest 2001\], who consider the problem of discovering “certificate chains”, i.e. proofs that a given set of certificates entails a given concrete certificate. Our notion of derivation “$`_0^{}`$” is similar to their notion of “name-reduction closure”, and Theorem 5.2 is closely related to a result they state (Theorem 1) concerning the completeness of the name reduction closure. They do not explicitly take time and revocation into account, as we have done, and they also do not consider the more general sorts of consequences we have discussed. On the other hand, they do characterize the computational complexity of the certificate chain discovery problem for concrete certificates, whereas we have not discussed the complexity of the inference problems we treat. We are currently examining the complexity of certificate chain discovery in our more general setting.

## 7 Discussion

In this paper, we have given a semantics for SPKI certificates independent of the semantics given in terms of tuple reduction in the SPKI documentation \[Ellison, Frantz, Lampson, Rivest, Thomas, and Ylonen 1999a, Ellison, Frantz, Lampson, Rivest, Thomas, and Ylonen 1999b\]. This allowed us to examine the extent to which the SPKI tuple reduction rules are complete. The SPKI documents are ambiguous as to the purpose of the tuple reduction rules, and conflates their use for purposes of semantics, making concrete authorization decisions, and general reasoning (e.g., generating “certificate result certificates”). We have carefully separated the three concerns here, and have shown that the relations between them are somewhat subtle. In particular, we have shown that extra reduction rules are needed in order to do general reasoning about certificates. Our main technical results show that, in a precise sense, the reduction rules given in the SPKI document are complete with respect to concrete certificates; adding a few more rules gives us an “almost” complete system with respect to general reasoning about certificates. This “almost completeness” result seems to be the best we can do without having rules that take into account the cardinality of the set of keys.

We need to be careful about the interpretation of the conclusions for which we have shown the tuple reduction rules to be complete. The form of conclusion associated with the tuple reduction rules is $`_{\mathrm{𝑐𝑙}}(_{𝚌^{}CC_R}𝚌^{})\varphi _𝚌`$, where $`\varphi _𝚌`$ has the form $`\mathrm{𝚗𝚘𝚠}𝚅\varphi _𝚌^{}`$ (with the exact form of $`\varphi _𝚌^{}`$ depending on the type of certifcate that $`𝚌`$ is). This states that $`\varphi _𝚌^{}`$ holds for all times in $`𝚅`$ at which additionally, all the certificates in $`CC_R`$ have been issued. Consider the certificate $`𝚌=(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚗𝚔^{}[\mathrm{𝟶},\mathrm{𝟷𝟶}])`$. According to our semantics, if $`𝚌r(5)`$, (i.e., this certificate is issued at time 5), and no other certificates are issued in $`r`$, then $`𝚔\text{’s}𝚗𝚔^{}`$ holds in $`r`$ during the interval $`[5,10]`$, but not during the interval $`[0,4]`$. On the other hand, the tuple reduction rules (trivially) allow the derivation of the tuple $`𝚔,𝚗,𝚔^{},[0,10]`$, which suggests that $`𝚔\text{’s}𝚗𝚔^{}`$ also holds during the interval $`[0,4]`$.141414We have followed the SPKI definitions closely, but we remark that we could modify the definition of the tuple generated by a certificate and a CRL: if $`𝚌`$ has validity interval $`[𝚝_1,𝚝_2]`$, and the computation is done at $`𝚝_0`$, then we redefine the interval in $`\tau (𝚌,C_R)`$ to be interval $`[max(𝚝_0,𝚝_1),𝚝_2]`$. All our completeness results would go through with this change, and it would result in a better match between our semantics and the tuple reduction rules.

Whether this difference matters depends on the use that is made of derived tuples. For conclusions about the current time, the difference does not matter, since agents will only be making authorization decisions based on $`𝚌`$ after the time at which $`𝚌`$ is issued, i.e., after time 5. However, for conclusions requiring reasoning about the past, the difference may be an issue needing careful consideration. (Such reasoning occurs in proposals by Rivest (?), Stubblebine (?), and Stubblebine and Wright (?) that involve authorizing an action when the latest time for which the existence of a right to perform that action can be proved is “sufficiently recent”. Another example where reasoning about the past may be important is where an auditor is verifying that an authorization decision made in the past was justified by certificates issued at the time of the decision.) As it does not appear that reasoning about the past was a significant concern in the design of SPKI, we do not pursue this further here.

Another contribution of this paper is to show that nonmonotonic logic is not required in a logical modeling of revocation if one takes the SPKI perspective that revocation is not a change of mind but a revalidation. (This viewpoint is supported by the text in \[SPKI Working Group 1998, Section 5.2\]: “The CRL is … a completion of the certificate, rather than a change of mind.”) The logic of this paper, like our earlier logic LLNC for SDSI, is monotonic. This does not prevent some aspects of its semantics from behaving nonmonotonically. In particular, $`L(𝚔,𝚗,𝚝)`$ may decrease as $`𝚝`$ increases if, for example, a certificate is revoked at time $`𝚝^{}>𝚝`$ that was not revoked at time $`𝚝`$ or if the validity interval of a certificate passes. Similarly, the set of actions a principal is permitted to perform may decrease over time. Note also that the semantics does not require that if a certificate appears on a CRL then it will also appear on all later CRLs issued during the certificate’s validity interval.151515 Although it does not appear to have been noted by the authors of SPKI, this allows CRLs to be used to obtain temporary suspensions. All of these types of “nonmonotonic” behaviour are entirely consistent with the monotonic logic we have developed.

We have focused on the SPKI reduction rules. However, we feel that the logic $`_{\mathrm{𝑆𝑃𝐾𝐼}}`$ will be useful for more general reasoning about names and authorization in SPKI than just whether a particular principal is authorized to perform some actions. For example, we may want to know which principals are authorized to perform a certain action, which actions a principal is allowed to perform, which principals are bound to a particular name, and which names have a particular principal bound to them. In \[Halpern and van der Meyden 2001\], we showed how we could translate queries about names (like the last two) into Logic Programming queries, allowing us to take advantage of the well-developed Logic Programming technology for answering such queries. We believe that it should be relatively straightforward to extend the translation so that it can handle more general SPKI queries. It also seems useful to try to obtain a sound and complete axiomatization for the full logic $`_{\mathrm{𝑆𝑃𝐾𝐼}}`$.

We believe that it should not be difficult to get such a complete axiomatization, using ideas from our earlier paper on SDSI, but we have not pursued this question. We have also not considered a number of features of SPKI, like threshold subjects and the precise syntax of SPKI’s tags (authorization expressions). It seems that our approach should be extendible to handle these features, but we have not checked any details.

## Appendix A Appendix:Proofs

Proposition 4.3:  For every run $`r`$, there exists a unique $`(K,N,\mathrm{𝐴𝑐𝑡})`$ interpretation minimal in the set of $`(K,N,\mathrm{𝐴𝑐𝑡})`$ interpretations consistent with $`r`$.

Proof: Let $`_r`$ consist of all interpretations consistent with $`r`$. $`_r`$ is nonempty, since the maximal interpretation is clearly consistent with $`r`$. Given an interpretation $`\pi `$, let $`L_\pi `$ denote the $`L`$ component of $`\pi `$ and let $`P_\pi `$ denote the $`P`$ component of $`\pi `$. Define an interpretation $`\pi _0`$ by taking $`L_{\pi _0}(𝚔,𝚗,𝚝)=_{\pi _r}L_\pi (𝚔,𝚗,𝚝)`$ and taking $`P_{\pi _0}(𝚔_1,𝚝,𝚔_2,𝚊)=\mathrm{min}_{\pi _r}P_\pi (𝚔_1,𝚝,𝚔_2,𝚊)`$. We now show that $`\pi _0`$ is the minimal element of $`_r`$.

Clearly $`\pi _0\pi `$ for all $`\pi _r`$. Thus, we must only show that $`\pi _0_r`$. First we must show that for all naming certificates $`𝚌=(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚗𝚙𝚅𝚔_r)`$ in $`_{𝚝^{}𝚝}r(𝚝^{})`$, if $`𝚝V`$ and $`𝚌`$ is applicable at $`𝚝`$ in $`r`$, then $`[[𝚗]]_{L_{\pi _0},𝚔,𝚝}[[𝚙]]_{L_{\pi _0},𝚔,𝚝}`$. By definition $`[[𝚗]]_{L_{\pi _0},𝚔,𝚝}=_{\pi _r}[[𝚗]]_{L_\pi ,𝚔,𝚝}`$. Moreover, since each $`\pi _r`$ is consistent with $`r`$, we have that $`[[𝚗]]_{L_\pi ,𝚔,𝚝}[[𝚙]]_{L_\pi ,𝚔,𝚝}`$ for $`\pi _r`$. It follows immediately that $`[[𝚗]]_{L_{\pi _0},𝚔,𝚝}=_{\pi _r}[[𝚗]]_{L_\pi ,𝚔,𝚝}_{\pi _r}[[𝚙]]_{L_\pi ,𝚔,𝚝}`$. Thus, it suffices to show that $`_{\pi _r}[[𝚙]]_{L_\pi ,𝚔,𝚝}[[𝚙]]_{L_{\pi _0},𝚔,𝚝}`$. This follows by an easy induction on the structure of $`𝚙`$. For the base case, as we have already observed, we have equality; for the general case the argument is almost immediate from the definition.161616We remark that this is a significantly simpler proof than that given for the analogous minimality result for SDSI in our earlier paper \[Halpern and van der Meyden 2001, Theorem 3.1\].

Next we must show that $`P_{\pi _0}`$ is indeed a permission/delegation assignment, that is, that if $`P_{\pi _0}(𝚔_1,𝚝,𝚔_2,𝚊)=2`$ and $`P_{\pi _0}(𝚔_2,𝚝,𝚔_3,𝚊)=i`$, then $`P_{\pi _0}(𝚔_1,𝚝,𝚔_3,𝚊)i`$. But if $`P_{\pi _0}(𝚔_1,𝚝,𝚔_2,𝚊)=2`$ and $`P_{\pi _0}(𝚔_2,𝚝,𝚔_3,𝚊)=i`$, then $`P_\pi (𝚔_1,𝚝,𝚔_2,𝚊)=2`$ and $`P_\pi (𝚔_2,𝚝,𝚔_3,𝚊)i`$ for all $`\pi _r`$. Thus, $`P_\pi (𝚔_1,𝚝,𝚔_3,𝚊)i`$ for all $`\pi _r`$, so $`P_{\pi _0}(𝚔_1,𝚝,𝚔_3,𝚊)i`$.

Finally, we must show that $`P_{\pi _0}`$ satisfies the second requirement of consistency. So suppose that $`𝚌=(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚙`$ $`𝙳𝙰𝚅𝚔_r)`$ is an authorization certificate in $`_{𝚝^{}𝚝}r(𝚝^{})`$, $`𝚝V`$, and $`𝚌`$ is applicable at $`𝚝`$ in $`r`$. Then for all $`\pi _r`$, for all $`𝚊\alpha _𝒜(𝙰)`$, and all keys $`𝚔^{}[[𝚙]]_{L_\pi ,𝚔,𝚝}`$, we have

1. $`P_\pi (𝚔,𝚝,𝚔^{},𝚊)1`$,
2. if $`𝙳=\mathrm{𝚝𝚛𝚞𝚎}`$ then $`P_\pi (𝚔,𝚝,𝚔^{},𝚊)=2`$.

As we observed earlier, if $`𝚔^{}[[𝚙]]_{L_{\pi _0},𝚔,𝚝}`$, then $`𝚔^{}[[𝚙]]_{L_\pi ,𝚔,𝚝}`$ for all $`\pi _r`$. Thus, $`P_\pi (𝚔,𝚝,𝚔^{},𝚊)1`$ for $`\pi _r`$, so $`P_{\pi _0}(𝚔,𝚝,𝚔^{},𝚊)1`$. Moreover, if $`𝙳=\mathrm{𝚝𝚛𝚞𝚎}`$, then $`P_\pi (𝚔,𝚝,𝚔^{},𝚊)=2`$ for $`\pi _r`$, so $`P_{\pi _0}(𝚔,𝚝,𝚔^{},𝚊)=2`$. This completes the proof.

We next prove the completeness results (Theorems 5.2 and 5.6). To do this, we need some preliminary definitions and results.

Rules R2 and R3 are very similar in the way that they transform principal expressions. For the completeness proofs, it is convenient to capture the commonalities by introducing a new type of tuple that we call a 3-tuple. A 3-tuples has the form $`𝚙,𝚚,𝚅`$ where $`𝚙,𝚚`$ are fully qualified principal expressions and $`𝚅`$ is an interval. Intuitively, this tuple says that $`p`$ is bound to $`q`$ during the time interval $`𝚅`$.

We have the following rules for reasoning about 3-tuples:

1. $`𝚙,𝚙,[0,\mathrm{}]`$ for all fully qualified principal expressions $`𝚙`$.
2. if $`𝚙,𝚔_1\text{’s}𝚗\text{’s}𝚚,𝚅_1+𝚔_1,𝚗,𝚔_2,𝚅_2𝚙,𝚔_2\text{’s}𝚚,𝚅_1𝚅_2`$.

R5, like R0, is essentially an axiom. R6 is somewhat in the spirit of R2, in that the third component of the 4-tuple is a key, rather than an arbitrary full qualified name. R6 extends R6 in much the same way that R2 extends R2.

1. if $`𝚙,𝚔_1\text{’s}𝚗\text{’s}𝚚,𝚅_1+𝚔_1,𝚗,𝚛,𝚅_2𝚙,𝚛\text{’s}𝚚,𝚅_1𝚅_2`$.

We abuse notation somewhat and continue to write $`T_0^{}\tau `$ (resp., $`T_1^{}\tau `$) if $`\tau `$ can be derived from $`T`$ using the rules R1–R3, R5, and R6 (resp., R0, R1, R2, R3, R5, R6). The following two propositions collect the key properties of 3-tuples.

###### Proposition A.1

: Suppose that $`i\{0,1\}`$. If $`T`$ is a set of 4- and 5-tuples such that $`T_i^{}𝚙,𝚚,𝚅_1`$, then

1. if $`T_i^{}𝚔,𝚗,𝚙,𝚅_2`$ then $`T_i^{}𝚔,𝚗,𝚚,𝚅_1𝚅_2`$;
2. if $`T_i^{}𝚔,𝚙,𝙳,𝙰,𝚅_2`$ then $`T_i^{}𝚔,𝚚,𝙳,𝙰,𝚅_1𝚅_2`$;
3. if $`T_i^{}𝚙^{},𝚙,𝚅_2`$ then $`T_i^{}𝚙^{},𝚚,𝚅_1𝚅_2`$.

Proof: By a straightforward induction on the length of the derivation of $`T_i^{}𝚙,𝚚,𝚅_1`$.

###### Proposition A.2

: Suppose that $`i\{0,1\}`$. For all fully qualified names $`𝚙,𝚚`$ and local names $`𝚗`$, we have $`T_i^{}𝚙,𝚚,𝚅`$ iff $`T_i^{}𝚙\text{’s}𝚗,𝚚\text{’s}𝚗,𝚅`$.

Proof: Again, by a straightforward induction on the length of the derivation of $`T_i^{}𝚙,𝚚,𝚅_1`$.

For convenience, we treat 3-tuples as certificates. For the 3-tuple $`𝚌=𝚙,𝚚,𝚅`$, we take $`\tau _𝚌=𝚌`$ and define $`\varphi _𝚌`$ to be the formula $`\mathrm{𝚗𝚘𝚠}𝚅𝚙𝚚`$. This formula captures the intuition that the 3-tuple is essentially saying that $`𝚙`$ is bound to $`𝚚`$.

The following theorem, whose proof is just like that of Theorem 5.3, says that $`_1^{}`$ (and hence $`_0^{}`$) continues to be sound in the presence of the rules for 3-tuples.

###### Theorem A.3

: Suppose that $`C`$ is a finite subset of $`𝒞`$, $`C_R`$ is a finite set of CRLs, and $`𝚌`$ is either a certificate in $`𝒞`$ or a 3-tuple. If $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}\tau _𝚌`$, then $`_c\left(_{𝚌^{}CC_R}𝚌^{}\right)\varphi _𝚌.`$ In fact, if $`\pi `$ is an interpretation consistent with a run $`r`$ and $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}\tau _𝚌`$, then $`r,\pi \left(_{𝚌^{}CC_R}𝚌^{}\right)\varphi _𝚌`$.

With this background, we are ready to prove Theorem 5.2.

Theorem 5.2:  If $`𝚌`$ is a concrete certificate, $`C`$ is a finite subset of $`𝒞`$, $`C_R`$ is a finite set of CRLs, and $`_c\left(_{𝚌^{}CC_R}𝚌^{}\right)\varphi _𝚌`$, then there exists a certificate $`𝚌^{}`$ that subsumes $`𝚌`$ such that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}\tau _𝚌^{}`$.

Proof: We prove the contrapositive. Suppose that there does not exist a certificate $`𝚌^{}`$ that subsumes $`𝚌`$ such that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}\tau _𝚌^{}`$. We show that it is not the case that $`_c\left(_{𝚌^{}CC_R}𝚌^{}\right)\varphi _𝚌`$, by showing that there is a run $`r`$ such that $`r,𝚔,𝚝_c_{𝚌^{}CC_R}𝚌^{}`$ for all times $`𝚝`$ but $`r,𝚔,𝚝_0\vDash ̸_c\varphi _𝚌`$, where $`𝚝_0`$ is the time in the concrete certificate $`𝚌`$.

Construct $`r`$ as follows: define $`r(0)=CC_R`$ and $`r(n)=\mathrm{}`$ for all $`n>0`$. Clearly $`r,𝚔,𝚝_c_{𝚌^{}CC_R}𝚌^{}`$ for all times $`𝚝`$. To show that $`r,𝚔,𝚝_0\vDash ̸_c\varphi _𝚌`$, we need to identify the minimal interpretation consistent with $`r`$. Consider the interpretation $`\pi =L,P`$ defined as follows:

1. $`L(𝚔,𝚗,𝚝)`$ is the set of keys $`𝚔^{}`$ such that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔,𝚗,𝚔^{},𝚅`$ where $`𝚝𝚅`$.
2. $`P(𝚔,𝚝,𝚔^{},𝚊)=2`$ if $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔,𝚔^{},𝙰,\mathrm{𝑡𝑟𝑢𝑒},𝚅`$ for some action expression $`𝙰`$ with $`𝚊\alpha _𝒜(𝙰)`$ and $`𝚝𝚅`$; $`P(𝚔,𝚝,𝚔^{},𝚊)=1`$ if $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔,𝚔^{},𝙰,\mathrm{𝑓𝑎𝑙𝑠𝑒},𝚅`$ for some $`𝙰`$ with $`𝚊\alpha _𝒜(𝙰)`$ and $`𝚝𝚅`$ and it is not the case that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔,𝚔^{},𝙰^{},\mathrm{𝑡𝑟𝑢𝑒},𝚅^{}`$ for some $`𝙰^{}`$ with $`𝚊\alpha _𝒜(𝙰^{})`$ and $`𝚝𝚅^{}`$; and $`P(𝚔,𝚝,𝚔^{},𝚊)=0`$ otherwise.

We must check that $`P`$ is a legimitate permission/delegation assignment. In particular, suppose that $`P(𝚔_1,𝚝,𝚔_2,𝚊)=2`$ and $`P(𝚔_2,𝚝,𝚔_3,𝚊)=i1`$. We must show that $`P(𝚔_1,𝚝,𝚔_3,𝚊)=i`$. Since $`P(𝚔_1,𝚝,𝚔_2,𝚊)=2`$, $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔_1,𝚔_2,𝙰_1,\mathrm{𝑡𝑟𝑢𝑒},𝚅_1`$ for some $`𝙰_1`$ with $`𝚊\alpha _𝒜(𝙰_1)`$ and some $`𝚅_1`$ containing $`𝚝`$. Similarly, we must have that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔_2,𝚔_3,𝙳_2,𝙰_2,𝚅_2`$ where $`𝚝𝚅_2`$, for some $`𝙰_2`$ with $`𝚊\alpha _𝒜(𝙰_2)`$, some $`𝙳_2`$ such that if $`i=2`$ then $`𝙳=\mathrm{𝑡𝑟𝑢𝑒}`$, and some $`𝚅_2`$ containing $`𝚝`$. Using R1, it follows that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔_1,𝚔_3,𝙳_2,𝙰_1𝙰_2,𝚅_1𝚅_2`$. Since $`𝚊\alpha _𝒜(𝙰_1𝙰_2)`$ and $`𝚝𝚅_1𝚅_2`$, it follows that $`P(𝚔_1,𝚝,𝚔_3,𝚊)i`$, as desired.

Next we must show that this interpretation is the minimal one consistent with $`r`$. We first establish that it is consistent. Thus, we must show that the formulas associated with naming and authorization certificates are satisfied in $`r`$. To do this, we use the following lemma. (This lemma was our main motivation for introducing 3-tuples.)

###### Lemma A.4

: If $`𝚙`$ is a fully qualified principal expression, then $`𝚔^{}[[𝚙]]_{L,𝚔,𝚝}`$ iff
$`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚙,𝚔^{},V`$ for some interval $`𝚅`$ containing $`𝚝`$.

Proof: We proceed by induction on the structure of $`𝚙`$. If $`𝚙`$ is a key $`𝚔^{}`$ then, by definition, $`[[𝚔^{}]]_{L,𝚔,𝚝}=\{𝚔^{}\}`$. By R5, $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔^{},𝚔^{},[0,\mathrm{}]`$. For the converse, note that a straightforward induction on the length of the derivation shows that if $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔^{},𝚚,𝚅`$, then $`𝚚=𝚔^{}`$ and $`𝚅=[0,\mathrm{}]`$.

For the inductive step, suppose that $`𝚙=𝚚\text{’s}𝚗`$. We first suppose that $`𝚔^{}[[𝚙]]_{𝚔,L,𝚝}`$, and show that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚙,𝚔^{},𝚅`$ for some interval $`𝚅`$ containing $`𝚝`$. By definition of $`[[𝚙]]_{L,𝚔,𝚝}`$, there exists $`𝚔_1[[𝚚]]_{L,𝚔,𝚝}`$ such that $`𝚔^{}L(𝚔_1,𝚗,𝚝)`$. By the inductive hypothesis, we have $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚚,𝚔_1,𝚅_1`$ for some interval $`𝚅_1`$ containing $`𝚝`$. By Proposition A.2, it follows that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚚\text{’s}𝚗,𝚔_1\text{’s}𝚗,𝚅_1`$. By definition of $`L`$ and the fact that $`𝚔^{}L(𝚔_1,𝚗,𝚝)`$, we have $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔_1,𝚗,𝚔^{},𝚅_2`$ for some $`𝚅_2`$ containing $`𝚝`$. By R6, it follows that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚚\text{’s}𝚗,𝚔^{},𝚅_1𝚅_2`$. This is what we need, since $`𝚝𝚅_1𝚅_2`$.

For the converse, suppose that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚙,𝚔^{},𝚅`$ for some interval $`𝚅`$ containing $`𝚝`$. We must show that $`𝚔^{}[[𝚙]]_{L,𝚔,𝚝}`$. Since $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚙,𝚔^{},𝚅`$ and $`𝚙=𝚚\text{’s}𝚗`$, it follows that there must be some key $`𝚔_1`$ such that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚙,𝚔_1\text{’s}𝚗,𝚅_1`$ and $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔_1,𝚗,𝚔^{},𝚅_2`$, where $`𝚅=𝚅_1𝚅_2`$. By the definition of $`L`$, we have that $`𝚔^{}L(𝚔_1,𝚗,𝚝)`$. Since $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚚\text{’s}𝚗,𝚔_1\text{’s}𝚗,𝚅_{m1}`$, by Proposition A.2, we also have $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚚,𝚔_1,𝚅_{m1}`$. By the induction hypothesis, it follows that $`𝚔_1[[𝚚]]_{L,𝚔,𝚝}`$. It is now immediate that $`𝚔^{}[[𝚙]]_{L,𝚔,𝚝}`$.

Continuing with the proof of the theorem, recall that we must show that the formulas associated with certificates issued in $`r`$ are satisfied in $`r`$. Suppose that $`𝚌=(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚗𝚙𝚅𝚔_r)`$ is a naming certificate in $`_{𝚝^{}𝚝}r(𝚝^{})`$ that is applicable in $`r`$ at time $`𝚝𝚅`$. We need to show that $`[[𝚗]]_{L,𝚔,𝚝}[[𝚙]]_{L,𝚔,𝚝}`$. For this, note that either $`𝚔_r`$ is not present in $`𝚌`$ and and $`\tau (𝚌)=𝚔,𝚗,𝚙,𝚅`$, or there exists a CRL $`𝚌_RC_R`$ with respect to which $`𝚌`$ is live and $`\tau (𝚌,𝚌_R)=𝚔,𝚗,𝚚,𝚅^{}`$, where again $`𝚝𝚅^{}`$. In either case, it follows that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔,𝚗,𝚙,𝚅_1`$ for some $`𝚅_1`$ containing $`𝚝`$.

We now want to show that if $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔,𝚗,𝚙,𝚅_1`$, then $`[[𝚗]]_{L,𝚔,𝚝}[[𝚙]]_{L,𝚔,𝚝}`$. Suppose that $`𝚔^{}[[𝚙]]_{L,𝚔,𝚝}`$. By Lemma A.4, we have that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚙,𝚔^{},𝚅_2`$ for some $`𝚅_2`$ containing $`𝚝`$. Since $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔,𝚗,𝚙,𝚅_1`$, by Proposition A.1, it follows that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔,𝚗,𝚔^{},𝚅_1𝚅_2`$. Using the definition of $`L`$, it follows that $`𝚔^{}[[𝚗]]_{L,𝚔,𝚝}`$, as desired.

Next, suppose that $`𝚌=(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚙𝙳𝙰𝚅𝚔_r)`$ is an authorization certificate in $`_{𝚝^{}𝚝}r(𝚝^{})`$ that is valid in $`r`$ at time $`𝚝𝚅`$. As in the case of naming certificates, it follows that there is some interval $`𝚅_1`$ such that $`𝚝𝚅_1`$ and $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔,𝚙,𝙳,𝙰,𝚅_1`$. Suppose that $`𝚔^{}[[𝚙]]_{L,𝚔,𝚝}`$. By Lemma A.4, $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚙,𝚔^{},𝚅_2`$ for some $`𝚅_2`$ containing $`𝚝`$. By Proposition A.1, $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔,𝚔^{},𝙳,𝙰,𝚅_1𝚅_2`$. From the definition of $`P`$, it follows that

$$r,\pi ,𝚔,𝚝\mathrm{𝑃𝑒𝑟𝑚}(𝚔,𝚙,𝙰)(𝙳\mathrm{𝐷𝑒𝑙}(𝚔,𝚙,𝙰)),$$

as required.

To see that $`L,P`$ is in fact the minimal interpretation consistent with $`r`$, suppose that $`\pi ^{}=L^{},P^{}`$ is another interpretation consistent with $`r`$. We need to show that $`\pi \pi ^{}`$. We first show that $`LL^{}`$. Suppose that $`𝚔^{}L(𝚔,𝚗,𝚝)`$. By definition of $`L`$, $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔,𝚗,𝚔^{},𝚅`$ for some interval $`𝚅`$ containing $`𝚝`$. Since $`\pi ^{}`$ is consistent with $`r`$, by Theorem A.3,

$$r,\pi ^{}\left(\underset{𝚌^{}CC_R}{}𝚌^{}\right)(\mathrm{𝚗𝚘𝚠}𝚅𝚔\text{’s}𝚗𝚔^{}).$$

Moreover, we have that $`r,\pi ^{},𝚔,𝚝_{𝚌^{}CC_R}𝚌^{}`$, by defintion of $`r`$. Since $`𝚝𝚅`$, it follows that $`r,\pi ^{},𝚔,𝚝𝚔\text{’s}𝚗𝚔^{}`$, so $`𝚔^{}L^{}(𝚔,𝚗,𝚝)`$. Thus, $`LL^{}`$. The argument that $`PP^{}`$ is very similar, and is left to the reader.

It remains to show that $`r,𝚔,𝚝_0\vDash ̸_c\varphi _𝚌`$. To see this, suppose first that $`𝚌`$ is a naming certificate such that $`\tau _𝚌=𝚔,𝚗,𝚔^{},[𝚝_0,𝚝_0]`$. Since $`𝚌`$ is not subsumed by any 4-tuple derivable from $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)`$, it is immediate from the definition of $`L`$ that $`𝚔^{}L(𝚔,𝚗,𝚝_0)`$. From this it follows that $`r,\pi ,𝚔,𝚝_0\vDash ̸_c\varphi _𝚌`$. The argument for authorization certificates is similar.

We now prove Theorem 5.6.

Theorem 5.6:  If $`𝚌`$ is a certificate, $`C`$ is a finite subset of $`𝒞`$, $`C_R`$ is a finite set of CRLs, and $`|K|>|C|+|𝚌|`$, and $`_{c,K}\left(_{𝚌^{}CC_R}𝚌^{}\right)\varphi _𝚌`$, then $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_2^{}\tau _𝚌`$; moreover, if $`𝚌`$ is a point-valued certificate, then $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}\tau _𝚌^{}`$ for some certificate $`𝚌^{}`$ subsuming $`𝚌`$.

Proof: The proof proceeds much in the same spirit as the proof of Theorem 5.2, using 3-tuples. Suppose that it is not the case that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_2^{}\tau _𝚌`$ (or it is not the case that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}\tau _𝚌`$, in the case that $`𝚌`$ is a point-valued naming certificate). Again the idea is to construct a run $`r`$ such that $`r,𝚔,𝚝_c_{𝚌^{}CC_R}𝚌^{}`$ for all times $`𝚝`$ and that $`r,𝚔,𝚝_0\vDash ̸_c\varphi _𝚌`$ for some time $`𝚝_0`$. The construction of $`r`$ is somewhat more complicated than in the case of Theorem 5.2.

Given a principal $`𝚙`$, let $`\mathrm{𝐶𝑙}(𝚙)`$ be the smallest set $`S^{}`$ of principal expressions containing $`𝚙`$, such that if $`𝚙\text{’s}𝚗S^{}`$ then $`𝚙S^{}`$. It is easy to see that $`|\mathrm{𝐶𝑙}(𝚙)||𝚙|`$, where $`|𝚙|`$ is the length of $`𝚙`$ viewed as a string of symbols. If $`C^{}`$ is a set of certificates, let $`\mathrm{𝐶𝑙}(C^{})`$ be the union of $`\mathrm{𝐶𝑙}(𝚙)`$, for all the principal expressions $`𝚙`$ that appear in a certificate in $`C^{}`$ as well as the principal expressions $`𝚔\text{’s}𝚗`$ for 4-tuples $`𝚔,𝚗,𝚚,V`$ in $`C^{}`$. Again, it should be clear that $`|\mathrm{𝐶𝑙}(C^{})||C^{}|`$. We will be interested in the set $`S=\mathrm{𝐶𝑙}(C\{𝚌\})`$ of pricipal expressions. Note that since we have assumed that $`|K|>|C|+|c|`$, it follows that $`|K|>|S|`$.

Let $`T`$ be the set of time points containing $`0`$, $`\mathrm{}`$, and the left and right components of each interval in $`CC_R`$. Note first that only a finite number of intervals $`𝚅`$ can appear in a tuple $`𝚙_0,𝚚_0,𝚅`$ generated from $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)`$, since every interval in a tuple generated has both left and right components in $`T`$. Hence, $`T`$ is finite. Let $`𝒱`$ be the set of all point intervals $`[𝚝,𝚝]`$ where $`𝚝T\{\mathrm{}\}`$, together with all intervals $`[𝚝_1+1,𝚝_21]`$ such that $`𝚝_1,𝚝_2T`$, $`𝚝_1<𝚝_2`$ and for no $`𝚝T`$ do we have $`𝚝_1<𝚝<𝚝_2`$. (We take $`\mathrm{}1=\mathrm{}`$). Note that the intervals in $`𝒱`$ are pairwise disjoint and span $`IN`$. Moreover, if $`𝚅`$ is the validity interval of a tuple derivable from $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)`$ and $`𝚆𝒱`$, then either $`𝚅𝚆=\mathrm{}`$ or $`𝚅𝚆`$. Finally, note that $`𝒱`$ is finite, since $`T`$ is.

For each interval $`𝚆𝒱`$, define the equivalence relation $`_𝚆`$ on $`S`$ by $`𝚙_1_𝚆𝚙_2`$ if both $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚙_1,𝚙_2,𝚅^{}`$ for some $`𝚅^{}𝚆`$ and $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚙_2,𝚙_1,𝚅^{\prime \prime }`$ for some $`𝚅^{\prime \prime }𝚆`$. We write $`[𝚙]_𝚆`$ for the equivalence class of $`_𝚆`$ containing $`𝚙`$.

Let $`X`$ be a set of keys in $`K`$ of cardinality $`|S|`$. For each interval $`𝚆𝒱`$ and equivalence class $`x`$ of $`_𝚆`$, choose a key $`𝚔_{x,𝚆}`$ in $`X`$ in such a way that if $`xy`$, then $`𝚔_{x,𝚆}𝚔_{y,𝚆}`$. Without loss of generality, we may assume that $`𝚔_{[𝚔]_𝚆,𝚆}=𝚔`$ for each key $`𝚔S`$. (Note that $`[𝚔]_𝚆=\{𝚔\}`$ since, as we observed earlier, if $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚔,𝚚,𝚅`$, then we must have $`𝚙=𝚔`$.) For ease of exposition, we write $`𝚔_{𝚙,𝚆}`$ rather than $`𝚔_{[𝚙]_𝚆,𝚆}`$.

Consider the run $`r`$ where no certificates are issued after time 0 and $`r(0)`$ consists of the following certificates:

1. all certificates in $`CC_R`$,
2. for each $`𝚆𝒱`$, principal expression of the form $`𝚙\text{’s}𝚗`$ in $`S`$, principal expression $`𝚚S`$ such that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚙\text{’s}𝚗,𝚚,𝚅^{}`$ for some $`𝚅^{}𝚆`$, the naming certificate $`(\mathrm{𝚌𝚎𝚛𝚝}𝚔_{𝚙,𝚆}𝚗𝚔_{𝚚,𝚆}𝚆)`$,
3. for each $`𝚆𝒱`$, principal expression $`𝚚S`$, and key $`𝚔S`$ such that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚔,𝚚,𝙳,𝙰,𝚅^{}`$ for some $`𝚅^{}𝚆`$, the authorization certificate $`(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚔_{𝚚,𝚆}𝙳𝙰𝚆)`$.

Note that this is a finite set of certificates since $`𝒲`$ and $`S`$ are a finite sets.

We now construct an interpretation $`\pi =L,P`$ consistent with $`r`$. For $`𝚝IN`$, let $`𝚆(𝚝)`$ be the unique interval in $`𝒱`$ containing $`𝚝`$. Define $`L(𝚔,𝚗,𝚝)=\mathrm{}`$ unless $`𝚔`$ is $`𝚔_{𝚙,𝚆(𝚝)}`$ for some principal expression $`𝚙`$; $`L(𝚔_{𝚙,𝚆(𝚝)},𝚗,𝚝)=\{𝚔_{𝚚,𝚆(𝚝)}:\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚙\text{’s}𝚗,𝚚,𝚅^{},𝚅^{}𝚆(𝚝)\}`$. $`L(𝚔_{𝚙,𝚆(𝚝)},𝚗,𝚝)`$ is well defined since, if $`𝚙^{}_{𝚆(𝚝)}𝚙`$, then by Proposition A.2, $`(𝚙^{})\text{’s}𝚗_{𝚆(𝚝)}𝚙\text{’s}𝚗`$, hence $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚙\text{’s}𝚗,𝚚,𝚅^{}`$ iff $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}(𝚙^{})\text{’s}𝚗,𝚚,𝚅^{}`$. Similarly, $`P(𝚔,𝚝,𝚔^{},𝚊)=0`$ unless $`𝚔^{}`$ is $`𝚔_{𝚚,𝚆(𝚝)}`$, for some principal expression $`𝚚`$. If $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔,𝚚,\mathrm{𝑡𝑟𝑢𝑒},𝙰,𝚅`$, where $`𝚊\alpha _𝒜(𝙰)`$ and $`𝚅𝚆(𝚝)`$, then $`P(𝚔,𝚝,𝚔_{𝚚,𝚆(𝚝)},𝚊)=2`$; if $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔,𝚚,\mathrm{𝑓𝑎𝑙𝑠𝑒},𝙰,𝚅`$, where $`𝚊\alpha _𝒜(𝙰)`$ and $`𝚅𝚆(𝚝)`$ and it is not the case that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔,𝚚,\mathrm{𝑡𝑟𝑢𝑒},𝙰^{},𝚅^{}`$ for some $`𝙰^{}`$ such that $`𝚊\alpha _𝒜(𝙰^{})`$ and $`𝚅^{}𝚆(𝚝)`$, then $`P(𝚔,𝚝,𝚔_{𝚚,𝚆(𝚝)},𝚊)=1`$; otherwise, $`P(𝚔,𝚝,𝚔_{𝚚,𝚆(𝚝)},𝚊)=0`$.

We want to show that $`\pi `$ is the minimal interpretation consistent with $`r`$. We first need an analogue of Lemma A.4.

###### Lemma A.5

: For all $`𝚙S`$, keys $`𝚔`$, and times $`𝚝`$, $`[[𝚙]]_{L,𝚔,𝚝}=\{𝚔_{𝚚,𝚆(𝚝)}:𝚚S,\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚙,𝚚,𝚅^{},𝚅^{}𝚆(𝚝)\}`$.

Proof: We proceed by induction on the construction of $`𝚙`$. If $`𝚙`$ is a key or an expression of the form $`𝚔\text{’s}𝚗`$, the claim follows trivially from the definitions. Note we cannot have $`𝚙=𝚗`$ for a local name $`𝚗`$, by the construction of $`S`$. So suppose that $`𝚙`$ has the form $`𝚚\text{’s}𝚗`$. We first show that if $`𝚔^{}[[𝚚\text{’s}𝚗]]_{L,𝚔,𝚝}`$, then there exist $`𝚛S`$ and $`𝚅^{}𝚆(𝚝)`$ such that $`𝚔^{}=𝚔_{𝚛,𝚆(𝚝)}`$ and $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚚\text{’s}𝚗,𝚛,𝚅^{}`$. By definition of $`[[𝚚\text{’s}𝚗]]_{L,𝚔,𝚝}`$, we have that $`𝚔^{}L(𝚔^{\prime \prime },𝚗,𝚝)`$ for some key $`𝚔^{\prime \prime }[[𝚚]]_{L,𝚔,𝚝}`$. By the induction hypothesis, there exists $`𝚚_1S`$ such that $`𝚔^{\prime \prime }=𝚔_{𝚚_1,𝚆(𝚝)}`$ and $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚚,𝚚_1,𝚅^{}`$ for some $`𝚅^{}𝚆(𝚝)`$. It follows from Proposition A.2 that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚚\text{’s}𝚗,𝚚_1\text{’s}𝚗,𝚅^{}`$. By definition of $`L`$, since $`𝚔^{}L(𝚔_{𝚚_1,𝚆(𝚝)},𝚗,𝚝)`$, there exists a principal expression $`𝚚_2`$ such that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚚_1\text{’s}𝚗,𝚚_2,𝚅^{\prime \prime }`$, where $`𝚅^{\prime \prime }𝚆(𝚝)`$ and $`𝚔^{}=𝚔_{𝚚_2,𝚆(𝚝)}`$. By Proposition A.1, it follows that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚚\text{’s}𝚗,𝚚_2,𝚅^{}𝚅^{\prime \prime }`$. Since $`𝚅^{}𝚅^{\prime \prime }𝚆(𝚝)`$, we are done.

For the converse, suppose that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚚\text{’s}𝚗,𝚛,𝚅^{}`$, where $`𝚛S`$ and $`𝚅^{}𝚆(𝚝)`$. Since $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚚,𝚚,[0,\mathrm{}]`$, we have that $`𝚔_{𝚚,𝚆(𝚝)}[[𝚚]]_{L,𝚔,𝚝}`$, by the induction hypothesis. Moreover, by definition of $`L`$, we have $`𝚔_{𝚛,𝚆(𝚝)}L(𝚔_{𝚚,𝚆(𝚝)},𝚗)`$. It follows that $`𝚔_{𝚛,𝚆(𝚝)}[[𝚚\text{’s}𝚗]]_{L,𝚔,𝚝}`$.

We use Lemma A.5 to show that $`\pi `$ is consistent with $`r`$. Consider a naming certificate $`𝚌=(\mathrm{𝚌𝚎𝚛𝚝}𝚔_\mathrm{𝟷}𝚗𝚙𝚅_\mathrm{𝟷}𝚔_𝚛)C`$ that is applicable at time $`𝚝𝚅_1`$. Either $`𝚌`$ is irrevoccable, or there exists a CRL $`𝚌^{}`$ in $`r(0)`$ with validity interval $`𝚅_2`$ such that $`𝚝𝚅_2`$ and $`𝚌`$ is live with respect to $`𝚌^{}`$. As in the proof of Theorem 5.2, in either case, there is an interval $`𝚅^{}𝚅_1`$ containing $`𝚝`$ such that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_0^{}𝚔_1,𝚗,𝚙,𝚅^{}`$. Since $`𝚝𝚅_1`$, we must have $`𝚅^{}𝚆(𝚝)`$. By R5, $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚔_1\text{’s}𝚗,𝚔_1\text{’s}𝚗,[0,\mathrm{}]`$ so, using R6, it follows that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚔_1\text{’s}𝚗,𝚙,𝚅^{}`$. Now if $`𝚔_2[[𝚙]]_{L,𝚔_1,𝚝}`$, then by Lemma A.5, $`𝚔_2=𝚔_{𝚚,𝚆(𝚝)}`$ for some $`𝚚S`$ such that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚙,𝚚,𝚅^{\prime \prime }`$, where $`𝚅^{\prime \prime }𝚆(𝚝)`$. It follows from Proposition A.1(c) that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚔_1\text{’s}𝚗,𝚚,𝚅^{}𝚅^{\prime \prime }`$. Since $`𝚅^{}𝚅^{\prime \prime }𝚆(𝚝)`$, it follows from the defintion of $`L`$ that $`𝚔_2=𝚔_{𝚚,𝚆(𝚝)}[[𝚗]]_{L,𝚔_1,𝚝}`$, as required.

Next, consider certificates of the form $`(\mathrm{𝚌𝚎𝚛𝚝}𝚔_{𝚙,𝚆}𝚗𝚔_{𝚚,𝚆}𝚆)`$, where $`𝚆𝒱`$, $`𝚙\text{’s}𝚗,𝚚S`$, and $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚙\text{’s}𝚗,𝚚,𝚅^{}`$ for some $`𝚅^{}𝚆`$. Since such certificates are irrevocable, they are always applicable. If $`𝚝W`$, we have $`[[𝚗]]_{L,𝚔_{𝚙,𝚆},𝚝}=L(𝚔_{𝚙,𝚆},𝚗,𝚝)\{𝚔_{𝚚,𝚆}\}=[[𝚔_{𝚚,𝚆}]]_{L,𝚔_{𝚙,𝚆},𝚝}`$ by construction.

Next, suppose that $`𝚌=(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚙𝙳𝙰𝚅𝚔_r)`$ is an authorization certificate in $`C`$ that is applicable in $`r`$ at time $`𝚝𝚅`$. As in the case of naming certificates, it follow that there is some interval $`𝚅_1`$ such that $`𝚝𝚅_1`$ and $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚔,𝚙,𝙳,𝙰,𝚅_1`$. Suppose that $`𝚔^{}[[𝚙]]_{L,𝚔,𝚝}`$. By Lemma A.5, $`𝚔^{}=𝚔_{𝚚,𝚆(𝚝)}`$ for some $`𝚚S`$ such that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚙,𝚚,𝚅_2`$ for some $`𝚅_2𝚆(𝚝)`$. By Proposition A.1, it follows that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚔,𝚚,𝙳,𝙰,𝚅_1𝚅_2`$. From the definition of $`P`$ and the fact that $`𝚔^{}=𝚔_{𝚚,𝚆(𝚝)}`$, it follows that

$$r,\pi ,𝚔,𝚝\mathrm{𝑃𝑒𝑟𝑚}(𝚔,𝚔^{},𝙰)(𝙳\mathrm{𝐷𝑒𝑙}(𝚔,𝚔^{},𝙰)),$$

as required.

Finally, consider an authorization certificate in $`r(0)`$ of the form $`(\mathrm{𝚌𝚎𝚛𝚝}𝚔𝚔_{𝚚,𝚆}𝙳𝙰𝚆)`$. By definition, $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚔,𝚚,𝙳,𝙰,𝚅^{}`$ for some $`𝚅^{}𝚆`$. Again, it is immediate from the definition of $`P`$ that

$$r,\pi ,𝚔,𝚝\mathrm{𝑃𝑒𝑟𝑚}(𝚔,𝚔_{𝚚,𝚆},𝙰)(𝙳\mathrm{𝐷𝑒𝑙}(𝚔,𝚔_{𝚚,𝚆},𝙰)).$$

This completes the proof that $`\pi `$ is consistent with $`r`$.

To show that $`\pi `$ is the minimal interpretation consistent with $`r`$, suppose that $`\pi ^{}=(L^{},P^{})`$. Suppose that $`𝚔^{}L(𝚔,𝚗,𝚝)`$ and let $`𝚆=𝚆(𝚝)`$. Then there exist principal expressions $`𝚙`$ and $`𝚚`$ such that $`𝚔=𝚔_{𝚙,𝚆(𝚝)}`$, $`𝚔^{}=𝚔_{𝚚,𝚆}`$ and $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚙\text{’s}𝚗,𝚚,𝚅^{}`$ for some interval $`𝚅^{}𝚆`$. Thus, $`r(0)`$ contains the certificate $`(\mathrm{𝚌𝚎𝚛𝚝}𝚔_{𝚙,𝚆}𝚗𝚔_{𝚚,𝚆}𝚆)`$. This implies that if $`\pi ^{}=(L^{},P^{})`$ is another interpretation consistent with $`r`$ then we must also have $`𝚔^{}L^{}(𝚔,𝚗,𝚝)`$. A similar argument works in the case of $`P`$. Thus, $`\pi `$ is the minimal interpretation consistent with $`r`$.

It remains to show that $`r,𝚔,𝚝_0\vDash ̸_c\varphi _𝚌`$ for some choice of $`𝚝_0`$. If $`𝚌`$ is a point-valued certificate such that $`\tau _𝚌=𝚔,𝚗,𝚙,[𝚝_0,𝚝_0]`$, then since it is not the case that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_2^{}\tau _𝚌`$, it is also not the case that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚔\text{’s}𝚗,𝚙,V`$ for any interval $`V`$ containing $`𝚝_0`$. (Otherwise, from Proposition A.1, we would be able to use R0 and R4(a) to derive $`\tau _𝚌`$.) Hence, by Lemma A.5, it follows that $`𝚔_{𝚙,𝚆(𝚝_0)}L(𝚔,𝚗,𝚝_0)`$. Of course, we do have (using R0) that $`𝚔_{𝚙,𝚆(𝚝_0)}[[𝚙]]_{L,𝚔,𝚝_0}`$. Thus, $`r,𝚔,𝚝_0\vDash ̸_c\varphi _𝚌`$.

Next, suppose that $`𝚌`$ is an arbitrary naming certificate, with $`\tau _𝚌=𝚔,𝚗,𝚙,𝚅`$. Let $`𝒱^{}`$ consist of all intervals $`𝚅^{}𝒱`$ such that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚔\text{’s}𝚗,𝚙,𝚅^{}`$. $`𝒱^{}`$ is finite, since $`𝒱`$ is. Moreover, it cannot be the case that $`𝚅𝒱^{}`$, for otherwise, using R4(a) and R0, it would follow that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_2^{}\tau _𝚌`$. Choose $`𝚝_0𝚅𝒱^{}`$. It follows just as above that $`r,𝚔,𝚝_0\vDash ̸_c\varphi _𝚌`$.

Finally, suppose that $`𝚌`$ is an authorization certificate, with $`\tau _𝚌=𝚔,𝚙,\mathrm{𝑡𝑟𝑢𝑒},𝙰,𝚅`$. (The argument is similar if $`\mathrm{𝑡𝑟𝑢𝑒}`$ is replaced by $`\mathrm{𝑓𝑎𝑙𝑠𝑒}`$.) We claim that there must be some time $`𝚝_0`$ and action $`𝚊\alpha _𝒜(𝙰)`$ such that for no interval $`𝚅^{}`$ containing $`𝚝_0`$ and $`𝙰^{}`$ such that $`𝚊\alpha _𝒜(𝙰^{})`$ is it the case that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚔,𝚙,\mathrm{𝑡𝑟𝑢𝑒},𝙰^{},𝚅^{}`$. It follows from the claim that $`P(𝚔,𝚝_0,𝚔_{𝚙,𝚆_{𝚝_0}},𝚊)2`$, so $`r,𝚔,𝚝_0\vDash ̸_c\varphi _𝚌`$. This completes the proof of the theorem. For the proof of the claim, suppose, by way of contradiction, that for all $`𝚝𝚅`$ and all actions $`𝚊\alpha _𝒜(𝙰)`$, there exists an interval $`𝚅_{𝚝,𝚊}`$ containing $`𝚝`$ and an action expression $`𝙰_{𝚝,𝚊}`$ such that $`𝚊\alpha _𝒜(𝙰_{𝚝,𝚊})`$ such that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚔,𝚙,\mathrm{𝑡𝑟𝑢𝑒},𝙰_{𝚝,𝚊},𝚅_{𝚝,𝚊}`$. Note that there are only finitely many time intervals $`𝚅^{}`$ and action expressions $`𝙰^{}`$ such that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_1^{}𝚔,𝚙,\mathrm{𝑡𝑟𝑢𝑒},𝙰^{},𝚅^{}`$. For each $`𝚊\alpha _𝒜(𝙰)`$, let $`𝙰_𝚊`$ be the intersection of all the action expressions $`𝙰_{𝚊,𝚝}`$ for $`𝚝𝚅`$. Since this is a finite intersection, $`𝙰_𝚊𝒜`$. Moreover, even if $`\alpha _𝒜(𝙰)`$ is infinite, the number of distinct sets $`𝙰_𝚊`$ is finite. By R4(c), for each $`𝚝𝚅`$, we have that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_2^{}𝚔,𝚙,\mathrm{𝑡𝑟𝑢𝑒},𝙰_𝚊,𝚅_{𝚝,𝚊}`$. Since the union of the sets $`𝚅_{𝚝,𝚊}`$ contains $`𝚅`$, and there are only finitely many such sets, by R4(b) it follows that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_2^{}𝚔,𝚙,\mathrm{𝑡𝑟𝑢𝑒},𝙰_𝚊,𝚅`$. Finally, since $`\alpha _𝒜(𝙰)`$ is contained in the union of the sets $`\alpha _𝒜(𝙰_𝚊)`$, it follows from R4(c) that $`\mathrm{𝚃𝚞𝚙𝚕𝚎𝚜}(C,C_R)_2^{}𝚔,𝚙,\mathrm{𝑡𝑟𝑢𝑒},𝙰,𝚅`$, which is a contradiction.

#### Acknowledgments:

We thank Jon Howell and the reviewers of this paper for their useful comments.