B.1. A Claim about Device Equivalence Classes

We have an important claim to flesh out: that all devices in the same equivalence class know the same PerUserKey secrets. This allows us to treat them the same throughout the UI, either for the purposes of propagating trust, or for the purposes of propagating secrets. Theorem B.1. For any device family, and any time t, ∀x, y ∈ Dt\Rt, if x ≡t y then pt(x) = pt(y). Before we get to the proof, it helps to proves some simpler lemmas about the structure of device families given our transition rules in Definition B.3. First, a simple observation:

Lemma B.2. For any device family, any time t, ∀x, y ∈ Dt\Rt, if hx, yi ∈ At then vt(x) = vt(y). Proof. If if hx, yi ∈ At , then the two are connected, and thus et(x) = et(y), from which we have vt(x) = vt(y).  The second lemma states that older devices know strictly more PerUserKey private halves than newer devices. For devices, a, b, c and d, provisioned in that order, it is clear to see that the later devices will always box for the earlier devices. But keep in mind that when b approves new devices, it never sends PerUserKeys back to earlier devices. So we must formally show that, for instance, c approving d does not transmit PerUserKeys from a that b didn’t know about. Lemma B.3. For any device family, at any time t, ∀x, y ∈ Dt\Rt, if dt(x) < dt(y) then pt(y) ⊆ pt(x). Proof. The proof is by induction over time t. For the base case, for any device family containing less than two devices (which includes any family at time t = 0), the claim is trivially true. For the inductive case, assume the lemma is true for time t − 1. Take arbitrary x, y ∈ Dt\Rt , such that dt(x) < dt(y). Consider the 4 possible state transitions:

1. DeviceAdd. A new device z is introduced at time t, meaning dt(z) = t. Note that it cannot be z = x as dt(x) < dt(y) ≤ t. If z = y, then let k be the PUK generated at Effect 1c. Bt gets hk, y, yi and hk, y, xi as a result of Effect 1d. Thus, pt(y) = {k} and k ∈ pt(x), which proves pt(y) ⊆ pt(x). If instead z 6∈ {x, y}, it must be that dt(x) < dt(y) < dt(z). By inductive assumption, pt−1(y) ⊆ pt−1(x). As before, let k be the PUK that is introduced at Effect 1c. At Effect 1d, Bt is augmented with hk, z, yi and hk, z, xi, and boxes for other devices. Thus, pt(x) = pt−1(x)∪{k}, and pt(y) = pt−1(y)∪{k}. Combining with the inductive assumption, it follows that pt(y) ⊆ pt(x).

2. DeviceRevoke and PerUserKeyRotate follow the same logic as device provisioning, so we leave out the argument for brevity.

3. BatchApprove is the interesting case. Device z approves all younger devices at time t. We consider three disjoint subcases: (a) dt(z) ≤ dt(x) < dt(y). As a result of Effect 4b, we get that pt(x) = pt−1(x) ∪ pt(z) and pt(y) = pt−1(y) ∪ pt(z). By inductive assumption we have that pt−1(y) ⊆ pt−1(x). Combining these three statements proves pt(y) ⊆ pt(x). (b) dt(x) < dt(z) < dt(y). Here we apply the inductive assumption to x and z, giving us that pt−1(z) ⊆ pt−1(x). Effect 4b doesn’t change pt−1(x) so therefore pt−1(x) = pt(x). Chaining these set relations together gives us that pt−1(z) ⊆ pt(x). Next, apply the inductive assumption to z and y, giving us that pt−1(y) ⊆ pt−1(z). By Effect 4b, pt(y) = pt−1(y) ∪ pt−1(z). By basic set theory, it is still the case that pt(y) ⊆ pt−1(z). By transitivity, pt(y) ⊆ pt(x). (c) dt(x) < dt(y) ≤ dt(z). Due to Effect 4a, devices y and x do not receive any new keys, i.e. pt(x) = pt−1(x) and pt(y) = pt−1(y). Combining with the inductive assumption pt−1(y) ⊆ pt−1(x) proves the subcase.  The next lemma establishes that older devices will always be grouped into older equivalence classes: Lemma B.4. For any device family F, any time t, ∀x, y ∈ Dt \ Rt, if dt(x) < dt(y) then vt(x) ≤ vt(y). Proof. Let k ∈ et(y) be such that dt(k) is minimal (in particular, vt(y) = dt(k)). We have 3 cases. Consider the case dt(k) < dt(x) (which implies k 6= y, as dt(x) < dt(y)). Consider a path from k to y along edges in At . There must be some ha, bi ∈ At along this path such that dt(a) < dt(x) ≤ dt(b). This implies that ha, xi ∈ At (as a must have approved x when it approved b), which means x ∈ et(y), and therefore vt(y) = vt(x). If dt(k) = dt(x), then x = k ∈ et(y) and vt(y) = vt(x). Finally, if dt(x) < dt(k), we have that by definition vt(x) ≤ dt(x) and thus vt(x) ≤ dt(x) < dt(k) = vt(y).  In the next lemma we show that a device performing an approval transition doesn’t change its own equivalence class. Lemma B.5. For any device family, any time t, ∀x ∈ Dt\Rt, if device x performs approval at time t, then vt(x) = vt−1(x). Proof. Assume for contradiction there exists a device family, and a time t such that x does a device approval transition at time t and vt(x) < vt−1(x). Pick i to be minimal in x’s equivalence class at time t, i.e. such that dt(i) = vt(x), and consider a path (without repeated nodes) from i to x. Since this path does not exist in At−1 (else it would be vt−1(x) ≤ dt(i) which leads to a contradiction), any such path must contain one of the edges hx, bi ∈ At \ At−1 (with dt(x) < dt(b)) added due to Effect 4a in the transition at time t. Since the path does not have repeated edges, the sub-path between b and i must be composed of edges in At−1, from which we derive vt−1(b) = dt−1(i). Putting it altogether, at time t − 1 we have that dt−1(x) < dt−1(b) but vt−1(x) > vt(x) = dt−1(i) = vt−1(b) which contradicts Lemma B.4.  Additionally, a device performing an approval cannot change the equivalence classes of older devices. Lemma B.6. For any device family, any time t, ∀x, y ∈ Dt\Rt such that dt−1(x) < dt−1(y), if y runs approval at time t then vt(x) = vt−1(x). Proof. The proof is similar to the one of the previous lemma. Assume for contradiction there exists a device family, and a time t such that y does a device approval transition

at time t and vt(x) < vt−1(x) for some device x such that dt(x) < dt(y). Pick i to be minimal in x’s equivalence class at time t, i.e. such that dt(i) = vt(x), and consider a path (without repeated nodes) from i to x. Since this path does not exist in At−1 (else it would be vt−1(x) ≤ dt(i) which leads to a contradiction), any such path must contain one of the edges hy, bi ∈ At \ At−1 (with dt(x) < dt(b)) added due to Effect 4a in the transition at time t. Since the path does not have repeated edges, the sub-path between b and i must be composed of edges in At−1, from which we derive vt−1(b) = dt−1(i). Putting it altogether, at time t − 1 we have that dt−1(x) < dt−1(y) < dt−1(b) but vt−1(x) > vt(x) = dt−1(i) = vt−1(b) which contradicts Lemma B.4.  Finally, we can prove Theorem B.1. The proof is by induction over t. It is trivially true at time t = 0, since there is only the null equivalence class. Assume it is true for time t − 1, and we prove true tor time t. We proceed case-wise, reasoning over the four transition types that could explain the transition from t − 1 to t. And now to the case-wise analysis:

1. DeviceAdd. A new device z is introduced at time t. In this case, since x ≡t y, z cannot be neither x nor y, and also x ≡t−1 y. We need to prove pt(x) = pt(y), but without loss of generality, we can prove one inclusion, and argue the other follows by symmetry. Given k ∈ pt(x), we need to prove k ∈ pt(y). We consider these subcases: (a) k ∈ pt−1(x). Then by inductive assumption, k ∈ pt−1(y). Since the set Bt only grows over time, it follows that k ∈ pt(y), which proves the case. (b) k /∈ pt−1(x). That is, there does not exist a w such that hk, w, xi ∈ Bt−1. Then it follows that at Effect 1d above, such a member was introduced. Recall that x, y ∈ Dt\Rt because the equivalence relation is only defined over devices in Dt\Rt . The loop in Effect 1d is over all devices in Dt\Rt , so x and y were both included. Thus, it follows that hk, w, yi ∈ Bt , and therefore that k ∈ pt(y).

2. DeviceRevoke. This case follows much like Case 1 (Device Provisioning), just above. In considering the two subcases k ∈ pt−1(x) is argued the same way. In the second subcase, k /∈ pt−1(x). Then the hk, w, yi triple must have been introduced at Effect 2c, and by similar argument as above hk, w, yi ∈ Bt , and therefore k ∈ pt(y).

3. PerUserKeyRotate. This case follows from the same reasoning as the other two cases above (provisioning and revocation).

4. BatchApprove. This is the most interesting case. Let w be the device that’s doing the approval at time t. Without loss of generality, assume that dt(x) < dt(y). The three cases to consider is how dt(w) is interwoven with dt(x) and dt(y). (a) dt(w) ≤ dt(x) < dt(y). By Lemma B.3, pt−1(x) ⊆ pt−1(w) and pt−1(y) ⊆ pt−1(w). As a result of Effect 4b, x and y will learn about all of the PerUserKeys that w knows. Combining with the prior observation, pt(x) = pt(y) = pt(w). (b) dt(x) < dt(w) < dt(y). This implies vt(x) ≤ vt(w) ≤ vt(y) by Lemma B.4, and since by assumption x ≡t y, it must be vt(x) = vt(w) = vt(y). By Lemmas B.5 and B.6, vt(x) = vt−1(x) and vt(w) = vt−1(w), and by transitivity, vt−1(x) = vt−1(w), and therefore x ≡t−1 w. We apply the inductive assumption to deduce

that pt−1(x) = pt−1(w). Again pt−1(x) isn’t affected by w’s approving newer devices, so pt−1(x) = pt(x) and therefore pt(x) = pt−1(w) by transitivity. By Lemma B.3, we know that pt−1(y) ⊆ pt−1(w). By Effect 4b, y gets all of w’s keys, and pt−1(w) is unchanged, so this gives pt(y) = pt(w) = pt−1(w). Chaining set equality, pt(x) = pt(y), which proves the case. (c) dt(x) < dt(y) ≤ dt(w). By assumption vt(x) = vt(y), and by Lemmas B.5 and B.6, vt−1(x) = vt(x) and vt−1(y) = vt(y). Chaining, vt−1(x) = vt−1(y) which means x ≡t−1 y. Applying the inductive assumption, pt−1(x) = pt−1(y). Device w running approval has no effect on pt−1(x) or pt−1(y). That is, pt−1(x) = pt(x) and pt−1(y) = pt(y). Chaining, pt(x) = pt(y) which proves it.