A Logic of Sattestation

In this paper we

• •

  introduce concepts of identity and contextual properties for web addresses and an associated concept of trusted belief in the binding together of such identities with or without associated properties. [Section II]

• •

  introduce a formal language and axiomatic logic for reasoning about trust in attestations of identity (i.e. binding of a public key in a self-authenticating address with a traditional domain name, e.g., as resolvable via DNS), a logic that supports two specific types of trust delegation, also introduce a Kripke semantics for the language and show soundness of the logic with respect to that semantics. [Section III]

• •

  contrast and compare the introduced logic with logics of authentication, logics of local names, and authorization and access control logics. [Section IV]

• •

  prove that any statement a principal trusts is either initially trusted, or that there is a trust chain of delegations to this from initial trust assumptions. [Section VI]

• •

  present a saturation algorithm that effectively derives all possible trust statements from a finite set of initial trust assumptions and show it to be sound, complete, and terminating. [Section VII]

Basic concepts and implementations of SATAs and sattestations as described in this paper are set out in papers by Syverson together with various coauthors [5, 6, 7]. [6] introduces a concept of contextual trust illustrated in the “news” example cited above, as well as an implementation in the form of a list of sattestations a site can post that a browser WebExtension can select to trust. Appendix V presents examples following the JSON format for sattestation headers introduced in [7], which include contextual labels. [7] also mentions in one sentence the possibility of transitivity if a sattestor label is permitted, but does not say anything more about these. None of these papers describes any means, formal or otherwise, to reason about when a sattestation should be trusted. Nor do they mention any structure to labels and how these relate to each other (e.g., as introduced below in Section III-A). Further they do not provide a language for, or any conception of, transitive or iterated trust in any form.

The basic meaning we attach to “trust” is the same as given by Coker et al. [9]: “Principal $B$ trusts principal $A$ with regard to the statement $\varphi$ if and only if, from the fact that $A$ has said $\varphi$, $B$ infers that $\varphi$ was true at a given time.” [9] is about formalizing remote attestation for trusted hardware as in the Trusted Platform Modules of the Trusted Computing Group (TCG). While our basic notion of trust is in this sense the same, that paper also does not discuss transitivity or iteration of trust or anything like our concept of contextual trust.

Formalizing transitive trust has previously been described in the context of secure communication [10]. However, that paper is primarily focused on honest messages (known to be true by the sender when sent) and related concepts that help ground a theory of cooperative communication in distributed systems. We do not assume messages are honest, and most of our rules effectively set out conditions under which it is possible to make a valid trust inference from a message. There is also nothing analogous to our notion of contextual trust therein. We further discuss transitive and iterated trust in Section III-C.

Ours is a logic of identity, particularly a logic of identity for web addresses. We will present a detailed comparison to other logics in Section IV, after we have set out our concepts of identity and trust in Section II, and we have set out our logic and language in Section III.

An entity comprises an identity and properties. The identity is signified by a domain name $D$ and an onion address $O$. In our notation an arbitrary $(D,O)$ is only a potential entity, a may-be. It may or may not signify a real identity. If $D$ and $O$ are bound together, then $(D,O)$ is a real identity.¹¹1By analogy to Thomistic ontology [11], we would say $(D,O)$ has esse. In this case we write $\langle D,O,\mathsf{bound}\rangle$ or, more succinctly, $\langle D,O\rangle$.

Though it is often to be expected that any $D$ is bound with at most one $O$ and vice versa, this need not be the case. Amongst other things, this allows multiple domain names to be bound to a single onion address (roughly as multiple domains might be hosted at the same IP address) and allows multiple onion addresses bound to a single domain name (as might be useful during an updating of a domain’s associated onion address).

Properties are expressed using labels, including the $\mathsf{bound}$ label just noted.²²2The only essential property an identity has is $\mathsf{bound}$. All other properties are accidental. $\langle D,O,\ell\rangle$ signifies that $D$ and $O$ are bound and that this entity has property $\ell$. Having a property may entail having a less specific property. For example, a site with the property of being a U.S. Department of Justice (DOJ) site also has the more generic property of being a U.S. Government (USG) site. A site for French recipes could have separate properties pertaining to French things and pertaining to recipes. It could also have a single “French recipes” property; this could entail a more generic “French” property, or it could entail a more generic “recipes” property.³³3As noted when we formalize our treatment of labels in Sec. III-A, we require that, if two properties are more generic than a third property, then one of the first two properties is more generic than the other.

Sattestations never assert a set of properties of which some are claimed to be bound and others are not, and sattestations never assert multiple non-$\mathsf{bound}$ properties. Thus, we do not need to worry about capturing a scenario in which $\langle D,O\rangle$ is known to have $\ell\neq\mathsf{bound}$ and we are reasoning about whether or not it has a different property $\ell^{\prime}\neq\mathsf{bound}$ as well. Also, as mentioned above in Section I, there are currently two implemented SAT address formats in use [7]. The SATA notation we have introduced in this section and that we use in our logic is an abstraction that covers both of them.

Suppose $P$ is a generic principal—either a client or a SATA—that forms beliefs about entities. These beliefs are expressed in our logic using the   trusts   operator, e.g., as $P\textit{\, trusts}\,\,\langle D,O\rangle$. Our logic does not cope with incorrect beliefs; if $P\textit{\, trusts}\,\,\langle D,O\rangle$ holds, then $D$ is actually bound to $O$. On the other hand, we have no need of anything comparable to a knowledge (T) axiom, because we never express $\langle D,O\rangle$ except when indicating $P\textit{\, trusts}\,\,\langle D,O\rangle$ or that $P$ asserts $\langle D,O\rangle$ (or $\langle D,O,\ell\rangle$, for some label $\ell$).

Besides bindings, the other thing a principal, $P$, may trust is that a SATA has asserted something about the binding of an identity (either with just the label $\mathsf{bound}$ or possibly an additional label). We capture such assertions using the  says   operator, so that we have, e.g., $P\textit{\, trusts}\,\,(\left(D,O\right)\,\textit{says}\,\,\left<D^{\prime},O^{\prime}\right>)$ (sometimes omitting the outer parentheses). $P$’s trust in an assertion may follow from $P$ receiving or retrieving a sattestation header, as described in [7], or it may follow from $P$ retrieving a list of entities claimed to be bound from the appropriate page of a SATA-site, as described in [6]. As formalized below, the left-hand side of the  says   operator is always written as a may-be, even if the name and address are known to be bound.

We will formally set out our language and logic in the next section. For purposes of comparison with other logics we note that all atomic formulae of our language are in the following forms (and generalizations of them to be explained when introduced below).

relations between property labels:

$\ell\preceq\ell^{\prime}$

trust in a binding:

$P\textit{\, trusts}\,\,\langle D,O,\ell\rangle$

trust that others asserted a binding:

$P\textit{\, trusts}\,\,(\left(D^{\prime},O^{\prime}\right)\,\textit{says}\,\,\left<D,O,\ell\right>)$

Note that it could be practical to support reasoning about arbitrary principals asserting bindings. For example, a client on a company-provided computer might download a list of labeled SATAs from a file on a trusted connection to a company server without a SATA, or Alice might be sent one or more labeled SATAs in an authenticated email message from Bob. For simplicity, we will restrict the reasoning about assertions in our current language and logic to reasoning about assertions made by SATAs. We will simply make appropriate local trust assumptions about the binding and labels of SATAs if based on non-SATA sources. Further, we assume that SATAs only make sattestations they believe. Thus, if a SATA issues a sattestation, then what is asserted will be reflected in the local trust assumptions of that SATA.

Note that this means trust about assertions are always in formulae such as the above $P\textit{\, trusts}\,\,(\left(D^{\prime},O^{\prime}\right)\,\textit{says}\,\,\left<D,O,\ell\right>)$, and we never write $P\textit{\, trusts}\,\,(\left<D^{\prime},O^{\prime}\right>\,\textit{says}\,\,\left<D,O,\ell\right>)$. Even if $P$ trusts that $D$ and $O$ are bound; the dependence on this in the axioms of our logic is reflected in other antecedent clauses. The only trust a binding assertion indicates is which may-be asserted what binding.

The axioms of our logic reflect circumstances under which it is valid to infer trust in a binding. Our logic does not incorporate time or an entity gaining or losing a property (as might happen, even with $\mathsf{bound}$, when a domain is sold, a key rotated, etc.). We assume antecedents of a derivation hold when the derivation is made. If an antecedent ceases to be valid, reasoning can be restarted without that statement. Our approach might be extended, e.g., by considering time intervals over which antecedents are valid (and, from those, computing a time interval over which a derivation’s conclusion is valid).

Although we should expect in practice that a client would only accept a SATA binding if it has checked an appropriately associated (non-expired, non-revoked, CT logged, etc.) TLS Certificate, we do not here represent such checks or associated reasoning. More broadly, our purpose in this paper is not to set out a usable tool for formal analysis of sattestation systems in practice, though we believe one could be based on our logic. Rather, our goal is to lay the basis for a rigorous understanding of sattestation.

The central aspect of SATAs and sattestations that distinguish them from other approaches for authentication (X.509, PGP) or trusted naming (DNS, SPKI/SDSI) is that they are contextual rather than structural. Note that even if PGP supports locally based trust, it is still a purely structural determination. Trust derives from distance and/or numbers of independent paths to primarily trusted nodes in a web rather than X.509’s adequate delegation from hierarchical roots, but this is not based on any context (e.g., association with a particular profession, company, or government agency); thus, it is still a structural determination. Contexts are also not types, and we cannot directly represent contextual trust in a standard type system. The same entity can have multiple contextual properties, and, as we shall see, this makes a difference as to what can be inferred about them. But entities might not have contextual labels at all other than the generic $\mathsf{bound}$ label (so, roughly, are not necessarily typed).

Also, while X.509 and DNS work primarily at large scales, and local names and PGP work primarily at much smaller scales, sattestations scale both up and down. They might operate at a large scale, such as the USG example above, or similarly for large corporations, or organizations, in which case one would expect large classes of browsers to come preconfigured by default to trust those as sattestors. Besides making these widely available to consumers, requiring such on enterprise issued or configured equipment can also protect corporate or governmental internal connections by remote workers against phishing attacks, VPN certificate hijack, and other attacks that could leak sensitive information, such as [12].

Sattestations will also operate fine, however, on a level of small organizations, municipalities and groups of various kinds, possibly without the resources or manpower to perform ongoing checks of CT log monitors or other indicators of certificate problems or hijack. (And those only provide post hoc evidence in any case.) Perhaps especially at a small scale, a basis for contextual trust is in associations and trust structures that already or naturally exist within the culture of an organization. It is generally a higher bar to set oneself up to fool the organizers and participants in a community that one is a member of that community than to fool others with no vested interest in that community per se.

Sattestations also do not require organizations to take on the overhead and responsibility of becoming a CA, nor do those need the active support of such structural entities, even if they utilize and leverage CAs, CT logs, etc., for the trust provided. CAs might also offer sattestation services, and this can provide some additional assurance and attack resistance. But to the extent these services are based on purely structural criteria for issuance of sattestations, they will be bound for most domains by the trust that a DV (Domain Validation) level check of identity can provide, even if they do build security (in the form of public keys) into the web itself.

Though our focus is on the logic of SATAs and sattestation, we briefly describe their implementation and use in practice, especially in contrast to TLS certificates. SATAs and sattestations have had research implementation and deployment on both the client and server sides [13, 14], which have also been described in research publications [6, 7]. On the client side the implementation uses a WebExtension for Firefox or Tor Browser that checks headers such as shown in Sec. V, although the cited publications note that the longer-term desirability is implementation natively in browsers. In the Firefox deployment, clients receive the strengthened authentication and hijack resistance properties described herein. In The Tor Browser implementation, clients also receive the routing and lookup protections that come from routing over the Tor network and using onion service protocols (thus, e.g., lookup via the onion-service Distributed Hash Table rather than via DNS). Unlike Tor’s onion addresses, SATAs are fully backwards compatible: browsers knowing nothing of SATAs will offer none of these additional protections. But access using them will succeed as normal (assuming no attacks).

Because SATAs are represented in TLS certificates using subdomains of registered domains, site owners can straightforwardly obtain needed DV certificates for free, e.g., from Let’s Encrypt. Because SATAs are generally formatted in one of the two formats described in Section I, no reconfiguring is necessary to make a site SATA-compatible. Besides the TLS certificate just noted, a front end is all that is needed to provide the sattestation headers.

We start with the labels used in our logic. We assume that we have a “basic” label set $\widehat{\Lambda}$ whose elements are free of the distinguished operators $\mathsf{sattestor}()$ and $\mathsf{sattestor}^{*}()$. (These operators will be explained below.) We expand this to a set $\widehat{\Gamma}$ of “general” labels by single applications of either $\mathsf{sattestor}$ or $\mathsf{sattestor}^{*}$:

In presenting rules below, we assume that labels $\ell$, $\ell^{\prime}$, $\ell_{i}$ are elements of $\widehat{\Lambda}$, and we will use, e.g., $\Lambda^{\prime}$ and $\Lambda_{i}$ for subsets of $\widehat{\Lambda}$. We assume labels $g$, $g^{\prime}$, and $g_{i}$ are elements of $\widehat{\Gamma}$, and we will use, e.g., $\Gamma^{\prime}$ and $\Gamma_{i}$ for subsets of $\widehat{\Gamma}$.

The operators $\mathsf{sattestor}()$ and $\mathsf{sattestor}^{*}()$, which take as a single argument $\ell\in\widehat{\Lambda}$, always occur as labels for bound SATAs. E.g., $\left<D,O,\mathsf{sattestor}(\ell)\right>$ indicates that $(D,O)$ may assert the binding of $\ell$ to any SATA, while $\left<D,O,\mathsf{sattestor}^{*}(\ell)\right>$ indicates that $(D,O)$ may indefinitely delegate the binding of label $\ell$. In other words $(D,O)$ may assert for any $(D^{\prime},O^{\prime})$ that $\left<D^{\prime},O^{\prime},\ell\right>$ or that $\left<D^{\prime},O^{\prime},\mathsf{sattestor}(\ell)\right>$ or that $\left<D^{\prime},O^{\prime},\mathsf{sattestor}^{*}(\ell)\right>$. These notions are made more precise by our axioms and truth conditions below and are further glossed after those are presented.

We assume that there is a partial order $\prec$ on $\widehat{\Lambda}$; if $\ell_{1}\prec\ell_{2}$, then we say that $\ell_{1}$ “narrows” $\ell_{2}$ and that $\ell_{2}$ “broadens” $\ell_{1}$. We use $\preceq$ to allow for $\ell_{1}=\ell_{2}$, and we use $\succ$ and $\succeq$ for (weak) broadening. $\widehat{\Lambda}$ includes the distinguished label $\mathsf{bound}$, which we discuss further below and which is incomparable to all other labels in $\widehat{\Lambda}$. We make the following additional assumptions about $\prec$:⁴⁴4While the first two assumptions are stated in terms of what principals “can determine,” these are assumptions about information conveyed by labels that a principal may not have seen before rather than principals’ computational power. These assumptions are satisfied by the label system we use here and the canonical label representation described in the following paragraphs.

• •

  For every $\ell\in\widehat{\Lambda}$, the set $\uparrow\{\ell\}=\{\ell^{\prime}|\ell^{\prime}\succeq\ell\}$ is finite. Furthermore, given $\ell$, any principal can determine the elements of $\uparrow\{\ell\}$.

• •

  Given $\ell_{1}$ and $\ell_{2}$, any principal can determine whether $\ell_{1}\prec\ell_{2}$, $\ell_{1}\succ\ell_{2}$, $\ell_{1}=\ell_{2}$, or $\ell_{1}$ and $\ell_{2}$ are incomparable under $\prec$.

• •

  For every $\ell$, $\uparrow\{\ell\}$ is linearly (totally) ordered under $\prec$.

Equivalent to the third condition above is that $\prec$ induces the structure of an ordered, rooted forest on $\widehat{\Lambda}$. The root of each tree in the forest is the $\prec$-maximum element of that tree. We observe that

with equality holding on one side iff it holds on the other.

If every $\ell\in\widehat{\Lambda}$ can be represented by a distinct finite string, then, given our first and third assumptions on the label poset, we may without loss of generality represent each $\ell\in\widehat{\Lambda}$ as a finite string $\lambda(\ell)$, where these strings satisfy the property that $\ell_{1}\succeq\ell_{2}$ if, and only if, $\lambda(\ell_{1})$, concatenated with a distinguished symbol, is a prefix of $\lambda(\ell_{2})$.

To see the previous claim: Let ‘$\mathsf{:}$’ be a distinguished symbol, and (re-encoding if necessary) let $\sigma(\ell)$ be a finite, ‘$\mathsf{:}$’-free string representing the label $\ell$ (and no $\ell^{\prime}\neq\ell$). Given $\ell$, we define its string label $\lambda(\ell)$ as follows. Let $\widehat{\ell}$ be the maximum element in $\uparrow\{\ell\}$. Define $\lambda(\widehat{\ell})$ as $\sigma(\ell)$. Inductively, let $\ell^{\prime}$ be the largest element of $\uparrow\{\ell\}$ for which $\lambda(\ell^{\prime})$ has not yet been defined. Let $\ell^{\prime\prime}$ be the label covering $\ell^{\prime}$.⁵⁵5$x$ covers $y$ iff $x\succ y$ and $x\succeq z\succeq y$ implies $z=x$ or $z=y$. We define $\lambda(\ell^{\prime})$ as the concatenation (indicated by the $\widehat{\ }$ operator) $\lambda(\ell^{\prime\prime})\ \widehat{\ }\ \text{`}\mathsf{:}\text{'}\ \widehat{\ }\ \sigma(\ell^{\prime})$.

Because $\lambda(\ell^{\prime})$ is defined inductively in terms of the string representations of the elements of the finite, linearly ordered set $\uparrow\{\ell^{\prime}\}$, it will not be defined in conflicting ways in the process of defining the $\lambda$ labels of multiple elements of $\widehat{\Lambda}$.

By our inductive construction, in this canonical representation of labels, $\lambda(\ell_{1})\ \widehat{\ }\ \text{`}\mathsf{:}\text{'}$ is a prefix of $\lambda(\ell_{2})$ if, and only if, $\ell_{1}\succeq\ell_{2}$. Furthermore, if $s=\sigma(\ell)$ and $\lambda$ is any canonical label representation, then $\text{`}\mathsf{:}\text{'}\ \widehat{\ }s\ \widehat{\ }\ \text{`}\mathsf{:}\text{'}$ appears at most once as a substring of $\text{`}\mathsf{:}\text{'}\ \widehat{\ }\lambda\ \widehat{\ }\ \text{`}\mathsf{:}\text{'}$.

Our examples of labels will all have the form of canonical $\lambda$-labels as just described and as specified in the following grammar.

If we use two labels $\lambda_{1},\lambda_{2}$, then we have $\lambda_{1}\succ\lambda_{2}$ if, and only if, $\lambda_{1}\ \widehat{\ }\ \text{`}\mathsf{:}\text{'}$ is a prefix of $\lambda_{2}$.

Because we are using the canonical label format described above, no string may appear multiple times as a $\sigma$-string in a label; e.g., ‘$\mathsf{recipes:USG:DOJ:FBI:recipes}$’ is not permitted as one of our example labels.

We now present a grammar (Sec. III-B1) for terms that may appear in our logic, our logical axioms and local axiom schemata (Sec. III-B2), and the deduction rules (Sec. III-B3) that we use. The local axiom schemata describe the forms of axioms that a principal may optionally use; they capture trust decisions specific to a principal and not inherent in our logic. We provide further discussion of the axioms and local axiom schemata in Sec. III-C.

This section describes the intent behind our axioms and rule schemata as well as decisions for the linguistic and logic design choices we have made.

The only rules are Modus Ponens ($\mathsf{MP}$) and Adjunction ($\mathsf{\land I}$, a.k.a. And-Introduction). Local axiom schemata reflect local trust assumptions particular principals might hold about nonlogical trust relations between labels or which principals to trust as sattestor.

Axiom A1 effectively says that any SATA that $P$ trusts to have a particular property label is also trusted to have any broader label, e.g., being a U.S. Government Dept. of Justice SATA (label $\mathsf{USG:DOJ}$) implies being a U.S. Government SATA (label $\mathsf{USG}$). A1 guides other design choices and how labels should be interpreted. It is important to understand that in our view labels do not capture authorization. We instead view narrowing a label as providing more specific information: for $\ell\succ\ell^{\prime}$, we view $\left<D,O,\ell^{\prime}\right>$ as more specific than $\left<D,O,\ell\right>$.

The $\mathsf{bound}$ label is incomparable to all other labels. If it were narrower than one or more other labels, A1 would allow us to infer that a SATA had those labels simply because it is bound. And if $\mathsf{bound}$ were broader than one or more other labels, A9 would allow a SATA that is trusted to have $\mathsf{sattestor}(\mathsf{bound})$ to sattest to $\left<D,O,\ell^{\prime}\right>$ for any $D$ and $O$ and any of those narrower labels $\ell^{\prime}$. An analogous problem would also arise with A10 and $\mathsf{sattestor}^{*}(\mathsf{bound})$.

Axioms A2–A4 tell us a label that one can infer is bound to a particular SATA based on a label that a trusted sattestor has attested is bound to that SATA. The first antecedent conjunct of each of these (about the relation between the three labels occuring in the other antecedent conjuncts) allows for the possibility that the labels in each of them need not be identical but can be appropriate narrowings or broadenings of the others. These axioms also reflect (in the fourth antecedent conjunct of each) the goal of authority independence. As originally stated, authority independence means that a misbehaving or misled CA will not be trusted by itself to bind an onion address and a domain in a TLS certificate. The owner of the domain and the onion address must concur for this binding to be trusted by a SATA-aware client [6, 7]. The authority independence aspect introduced herein applies not to CAs but to sattestors: a sattestor’s assertion that a sattestee has a label will not be trusted unless the sattestee concurs. For Axiom A2, this is an explicit assertion of a label $\ell_{3}$ that weakly narrows the sattested label; for Axioms A3 and A4, this is a statement in which the sattestee acts as a sattestor in the appropriate way. We need three axioms to cover the different kinds of labels in the ultimate consequent: sattestor-free, delegatable sattestor, or simple sattestor, respectively.

For practical simplicity, a sattestor knows the label $\ell_{i}$ for which it is providing a sattestation and only states it under a role qualified to do so. We assume any sattestor can detect and resist an attacker attempting to somehow confuse that sattestor about the state it is in so as to cause it to utter a sattestation under a sattestor role different from one appropriate for the sattestation uttered. This allows us to avoid having to include a label $\mathsf{sattestor}(\ell_{j})$ (or respectively $\mathsf{sattestor}^{*}(\ell_{j})$) under which $(D_{1},O_{1})$ is making a sattestation in the second trust conjunct of Axiom A2—or indeed having a sattestor making any statement be anything beyond a may-be.

We do not include an analogue of Axiom A2 that replaces the restriction $\ell_{1}\succeq\ell_{2}\succeq\ell_{3}$ with the restrictions $\ell_{1}\succeq\ell_{2}$ and $\ell_{3}\succ\ell_{2}$, i.e., in which the label claimed by the sattestee is (strictly) broader than the label given by the sattestor. We now explain why.

If we derived the narrower label given by the sattestor—i.e., we derived $P\textit{\, trusts}\,\,\left<D_{2},O_{2},\ell_{2}\right>$—then we would be giving the sattestee a label that is more specific than what it claims about itself. This contradicts the motivation for requiring the sattestee to say a label consistent with what the sattestor says. For example, we would not want a sattestor to be able to give the label $\mathsf{USG:DOJ:FBI:recipes:French}$ to a site that only claims the label $\mathsf{USG:DOJ:FBI}$ for itself.

If we derived the broader label claimed by the sattestee—i.e., we derived $P\textit{\, trusts}\,\,\left<D_{2},O_{2},\ell_{3}\right>$—then the concern is a bit more subtle. As an example, consider labels that reflect the structure of a hierarchical organization. Suppose that $(D_{1},O_{1})$ is a directory site in the engineering division of ACME Corp. that can label other sites as research sites within that division, i.e., it has the property $\mathsf{sattestor}(\mathsf{ACME:Eng:research})$. Suppose that $(D_{2},O_{2})$ is an internal server for the marketing division of ACME Corp. $(D_{2},O_{2})$ claims that it is an ACME Corp. site by saying it has the label $\mathsf{ACME}$. If $(D_{1},O_{1})$ says that $(D_{2},O_{2})$ has the label $\mathsf{ACME:Eng:research}$, then—using the hypothetical axiom we are considering—we could derive that $(D_{2},O_{2})$ has the label $\mathsf{ACME}$. On one hand, this seems reasonable; if $(D_{2},O_{2})$ had the label $\mathsf{ACME:Marketing:internal}$, then it would also have the label $\mathsf{ACME}$ (by A1). On the other hand, the derivation that we are considering makes use of a sattestation by a site $(D_{1},O_{1})$ that is in a different administrative division from $(D_{2},O_{2})$ and whose $\mathsf{sattestor}()$ authority does not cover the division containing $(D_{2},O_{2})$. On balance, we think this is undesirable, so we do not include such a derivation here. If $(D_{2},O_{2})$ wanted the broader label $\ell_{3}$—here, $\mathsf{ACME}$—based on the sattestation from $(D_{1},O_{1})$, then it needs to claim the narrower label $\ell_{2}$—here $\mathsf{ACME:Eng:research}$—so that $\ell_{1}\succeq\ell_{2}\succeq\ell_{3}$, and A2 would apply.

Many notions called ‘trust’ are transitive, though this is also sometimes criticised [15]. Following previous work on SATAs, our notion is not inherently transitive. Just because $P$ trusts that a $\left<D,O,\ell\right>$ is bound and has property $\ell$, does not mean that $P$ trusts sattestations by $(D,O)$. And even if $P$ trusts sattestations by $(D,O)$, it may not trust $(D,O)$ to sattest who else is a sattestor. See [6] for an illustrative example.

Rather than simply prohibit transitive trust, our axioms (above) and truth conditions (below) set out the contextual assumptions under which we support it.

Axiom A5 ensures that a SATA trusted to be bound with any label is also trusted to be simply bound.

Axiom A6 tells us that if a principal trusts that a SATA has asserted anything, that SATA is trusted to be implicitly asserting that it is itself a bound SATA.

Axiom A7 indicates that when a principal trusts that a SATA is a delegatable-sattestor of a label it also trusts that SATA is simply a sattestor of that same label. Axiom A8 reflects that principal trust in an assertion about a delegatable-sattestor label similarly implies trust in an assertion about a simple sattestor of the label. Note that A8, combined with A7, allows for a simplification of the logic with respect to Axioms A2–A4. It could have been necessary to have two versions of each of those axioms: wherever $\mathsf{sattestor}()$ occurs in an antecedent clause of those axioms we could have also needed to have a version of the axiom with $\mathsf{sattestor}^{*}()$ in that clause. But Axioms A7 and A8 allow us to infer trust in a simple sattestor label (assertion about such a label) from trust in a delegatable-sattestor label (assertion about such a label).

Axioms A9 and A10 describe trust that a (delegatable) sattestor of any label is also a (delegatable) sattestor of any narrowing of that label.

Axiom A11 indicates that any statement is effectively a public announcement. Every principal knows every assertion made by any SATA. (Principals do not necessarily trust what is asserted; they only trust that it is asserted.) Note that we are not concerned in this logic with capturing reasoning about the sending of messages or authenticated propagation of information. Rather we are concerned with what can be inferred from assertions made by any principal together with assumptions regarding who is trusted to assert which bindings.

Axiom A12 comprises collectively the standard axioms for use of the sentential connective for conjunction. We will in general be liberal in our writing of conjunctions when the usage is clear and consistent with propositional logic, thus allowing, e.g., ‘$\varphi\land\psi\land\delta$’. (We have similarly allowed, .e.g., ‘$\ell_{1}\succeq\ell_{2}\succeq\ell_{3}$’.)

For the local axiom schemata, a principal would use an instance of 1 to trust that any SATA bound to a label $g_{1}$ is also bound to the label $g_{2}$. The 2 and 3 schemata allow a principal to trust a specified SATA to be a (delegatable) sattestor for any label. This is useful if the principal wants to trust whatever her employer (or a trustworthy friend, etc.) says.

A frame $\mathcal{F}$ comprises a tuple $(W,\{R_{P}\})$ where $W$ is a set of worlds, and for each principal $P$ there is a relation $R_{P}\subseteq W\times W$ on worlds such that $(w,w^{\prime})\in R_{P}$ indicates $w^{\prime}$ is accessible from $w$ by $P$. A model $\mathcal{M}$ consists of: a frame $\mathcal{F}$, a client $c$, a set $\mathcal{D}$ of domain names, a set $\mathcal{O}$ of onion addresses, a label set $\widehat{\Lambda}$ and a partial order $\prec$ on it, the set $\Phi$ of all well-formed formulae (all $\mathsf{form}$s in our grammar above), and a (world-dependent) assignment function $a_{w}$ based on those. Note that all names, labels (and the partial order on them), and statements are shared globally across worlds, while local differences (between worlds) are all reflected in the assignment function $a_{w}$. So, in a frame $\mathcal{F}=(W,\{R_{P}\})$, a world $w\in W$ is a tuple $(c,\mathcal{D},\mathcal{O},\widehat{\Lambda},\prec,\Phi,a_{w})$. Because we do not attempt in this logic to capture faulty trust reasoning (where a principal can trust something that is false), our accessibility relation on worlds $R$ is reflexive.

Ours is not a normal modal logic, primarily because we do not capture trust of arbitrary formulae. Given our motivating application, our focus is ultimately on reasoning about contextual trust (the binding of labeled SATAs) while relying on the types of utterances that are made in sattestations. While extensions of our logic may be of future interest from a logical perspective, here we intentionally restrict our language to trust in SATA bindings and specified types of assertions. Thus, as already noted, in our current language only a may-be can say anything. Further, the only thing that can be said is a bound SATA, which may have any type of label. And the only formulae that a principal can trust are those expressing such bound SATAs and those expressing utterances of bound SATAs by a may-be SATA. To minimize notation we do not introduce separate notation for the formulae that a may-be can say or for the formulae that a principal can trust. But it should be kept in mind that these cannot be arbitrary formulae.

To capture binding of identities we introduce a pair of functions $\beta_{1},\beta_{2}$ on $\mathcal{D}\times\mathcal{O}$, where $\beta_{1}((D,O))=$ the set of all $(D_{i},O_{i})\in\mathcal{D}\times\mathcal{O}$ s.t. $D_{i}$ is bound with $O$, and
$\beta_{2}((D,O))=$ the set of all $(D_{i},O_{i})\in\mathcal{D}\times\mathcal{O}$ s.t. $O_{i}$ is bound with $D$. Those preliminaries out of the way, we now set out the conditions that our assignment function must satisfy. The specification of an assignment function $a_{w}$ satisfying these then determines the truth conditions. For a world $w$ and a label $\ell$, $a_{w}(\ell)$ defines those $(D,O)$ for which $\left<D,O,\ell\right>$ in $w$. Similarly, $a_{w}(\Phi_{(D,O)})$ defines the set of statements that $(D,O)$ utters in $w$. We discuss constraints on the assignment function in Sec. III-C.

1. AF1

   $a_{w}(c)=c$, $a_{w}(D\in\mathcal{D})=D$, $a_{w}(O\in\mathcal{O})=O$

2. AF2

   $a_{w}(\ell\in\widehat{\Lambda})\subseteq\mathcal{D}\times\mathcal{O}$

3. AF3

   $a_{w}(\Phi_{(D,O)})\subseteq\{\varphi|\varphi\text{ is a }\mathsf{bd\_l\_pair}\}$

4. AF4

   $a_{w}(\beta_{1}((D,O)))\subseteq\beta_{1}((D,O))$,
   $a_{w}(\beta_{2}((D,O)))\subseteq\beta_{2}((D,O))$,

By uttering a formula, any SATA implicitly asserts that it is an entity. We thus restrict $a_{w}(\Phi_{(D,O)})$ so that if $a_{w}(\Phi_{(D,O)})$ is nonempty, then $\langle D,O,\mathsf{bound}\rangle\in a_{w}(\Phi_{(D,O)})$. (In general, note that an element of $a_{w}(\Phi_{(D,O)})$ is a $\mathsf{bd\_l\_pair}$ $\pi$ and not an $\mathsf{s\_stmt}$ of the form $(D,O)\,\textit{says}\,\,\pi$.) Also, the set of SATAs with a given label can vary from world to world. Nonetheless, we do not permit that $\ell^{\prime}\prec\ell$ in one world but not in another. Thus if $a_{w}(\ell^{\prime})\subseteq a_{w}(\ell)$ at any world $w$, then $a_{w^{\prime}}(\ell^{\prime})\subseteq a_{w^{\prime}}(\ell)$ at all worlds $w^{\prime}$. We reflect this in our truth conditions, which we set out following some preliminary remarks.

We give truth conditions to expressions in our language in terms of satisfaction at a world $w$. (We take the model, $\mathcal{W}$ to be set and implicit.) We begin with the various logically atomic formulae: first expressing the narrowing relation on labels, then various types of formulae for SATAs bound with different types of labels. Next we present truth conditions for formulae reflecting assertions, then trust formulae, and finally formulae containing logical connectives.

Our semantics is model-theoretic in structure, not operational, but we are also motivated by an operational perspective reflected in the truth conditions for various individual kinds of formulae. Together, the truth conditions allow us to evaluate $w\models\phi$, where $\phi$ is a $\mathsf{form}$ in our grammar. Truth conditions rely on the function $a_{w}$ and truth conditions weakly earlier in the list; for convenience, the first line of each truth condition indicates the type of $\phi$ for which it defines the truth of $w\models\phi$.

1. TC1

   [$\phi$ is $\mathsf{stmt:wk\_order}$]
   $w\models\ell\preceq\ell^{\prime}$ iff
   ($\ell^{\prime}\ \widehat{}:$ is an initial string of $\ell$) $\land$
   ( for all $w^{\prime}$, $a_{w^{\prime}}(\ell)\subseteq a_{w^{\prime}}(\ell^{\prime})$)

2. TC2

   [$\phi$ is $\mathsf{stmt:bd\_pair}$]
   $w\models\langle D,O,\mathsf{bound}\rangle$ iff
   $w\models\langle D,O\rangle$ iff
   ($a_{w}(D)=\mathsf{proj}_{1}(D^{\prime},O^{\prime})$
   for some $(D^{\prime},O^{\prime})\in a_{w}(\beta_{1}(D,O))$) $\land$
   ($a_{w}(O)=\mathsf{proj}_{2}(D^{\prime\prime},O^{\prime\prime})$
   for some $(D^{\prime\prime},O^{\prime\prime})\in a_{w}(\beta_{2}(D,O))$)

3. TC3

   [$\phi$ is $\mathsf{stmt:t\_stmt:bd\_l\_pair}$ with $g\in\widehat{\Lambda}\setminus\{\mathsf{bound}\}$]
   $w\models\langle D,O,\ell\rangle$ iff
   ($w\models\langle D,O,\mathsf{bound}\rangle$) $\land$ ($(D,O)\in a_{w}(\ell)\big{)}$

4. TC4

   [$\phi$ is $\mathsf{stmt:t\_stmt:bd\_l\_pair}$ with $g=\mathsf{sattestor}(\ell)$]
   $w\models\langle D,O,\mathsf{sattestor}(\ell)\rangle$ iff
   ($w\models\langle D,O,\mathsf{bound}\rangle$) $\land$
   (if ($\langle D^{\prime},O^{\prime},\ell^{\prime}\rangle\in a_{w}(\Phi_{(D,O)})$ $\land$
      $\langle D^{\prime},O^{\prime},\ell^{\prime\prime}\rangle\in a_{w}(\Phi_{(D^{\prime},O^{\prime})})$ $\land$
      $w\models\ell^{\prime\prime}\preceq\ell^{\prime}$ $\land$
      $w\models\ell^{\prime}\preceq\ell$)
   then $w\models\langle D^{\prime},O^{\prime},\ell^{\prime}\rangle$)

5. TC5

   [$\phi$ is $\mathsf{stmt:t\_stmt:bd\_l\_pair}$ with $g=\mathsf{sattestor}^{*}(\ell)$]
   $w\models\langle D_{1},O_{1},\mathsf{sattestor}^{*}((\ell))\rangle$ iff
   $w\models\langle D_{1},O_{1},\mathsf{sattestor}((\ell))\rangle$ $\land$
   ( if ($w\models\ell^{\prime\prime}\preceq\ell^{\prime}$ $\land$ $w\models\ell^{\prime}\preceq\ell$), then
   ((if ($\langle D_{2},O_{2},\mathsf{sattestor}^{*}(\ell^{\prime})\rangle\in a_{w}(\Phi_{(D_{1},O_{1})})$ $\land$
   $\langle D_{3},O_{3},\mathsf{sattestor}(\ell^{\prime\prime})\rangle\in a_{w}(\Phi_{(D_{2},O_{2})})$) then
   $w\models\langle D_{2},O_{2},\mathsf{sattestor}^{*}(\ell^{\prime\prime})\rangle$) $\land$
   (if ($\langle D_{2},O_{2},\mathsf{sattestor}(\ell^{\prime})\rangle\in a_{w}(\Phi_{(D_{1},O_{1})})$ $\land$
   $\langle D_{3},O_{3},\ell^{\prime\prime}\rangle\in a_{w}(\Phi_{(D_{2},O_{2})})$ ) then
   $w\models\langle D_{2},O_{2},\mathsf{sattestor}(\ell^{\prime\prime})\rangle$ )) )

6. TC6

   [$\phi$ is $\mathsf{stmt:s\_stmt}$, i.e., of form $\mathsf{maybe}\,\textit{says}\,\,\mathsf{bd\_l\_pair}$]
   $w\models(D,O)\,\textit{says}\,\,\varphi$ iff
   (for all $P$, $R_{P}(w,w^{\prime})\Rightarrow\varphi\in a_{w^{\prime}}(\Phi_{(D,O)})$) $\land$
   (if $\varphi=\langle D^{\prime},O^{\prime},\mathsf{sattestor}^{*}(\ell)\rangle$ for some $D^{\prime}$, $O^{\prime}$, and $\ell$,
   then $\langle D^{\prime},O^{\prime},\mathsf{sattestor}(\ell)\rangle\in a_{w^{\prime}}(\Phi_{(D,O)})$)

7. TC7

   [$\phi$ is $\mathsf{stmt:t\_stmt}$; $\varphi$ must be $\mathsf{s\_stmt}$ or $\mathsf{bd\_l\_pair}$]
   $w\models P\textit{\, trusts}\,\,\varphi$ iff
   $\forall w^{\prime}\in W$ (if $R_{P}(w,w^{\prime})$, then $w^{\prime}\models\varphi$)

8. TC8

   [$\phi$ is $\mathsf{form}\rightarrow\mathsf{form}$]
   $w\models\varphi\rightarrow\psi$ iff
   $w\not\models\varphi$ or $w\models\psi$.

9. TC9

   [$\phi$ is $\mathsf{form}\land\mathsf{form}$]
   $w\models\varphi\land\psi$ iff
   $w\models\varphi$ and $w\models\psi$.

Note that it is possible for circular dependencies involving TC5. Thus, e.g., the condition $w\models\left<D,O,\mathsf{sattestor}^{*}(\ell)\right>$ might depend on $w\models\left<D^{\prime},O^{\prime},\mathsf{sattestor}^{*}(\ell)\right>$ and vice versa. For our motivating scenario in Section V, this is not a problem: as shown by Thm. VI.4, a principal will not derive trust in a SATA of the form $\left<D,O,\mathsf{sattestor}^{*}(\ell)\right>$ unless this is rooted in an explicit local assumption (and not a cycle of dependencies). We now further describe scenarios motivating choices for the semantics of $\mathsf{sattestor}^{*}()$.