B. Understanding Multiple Devices
As detailed in Section 3.4, device graphs can become complicated; we introduce a formal model to reason about them and what guarantees are available.
Definition B.1. A device family state is a tuple: Ft = hDt , dt , Rt , At , Pt , Bti Where: • t ∈ N0 is a non-negative integer which is used to order states in a sequence, which we refer to as “time.” • Dt is a finite set whose elements represent the devices at time t. • dt : Dt → N0 is a function that maps devices to the time t that they were provisioned. • Rt ⊆ Dt is the set of revoked devices at time t. x ∈ Rt means that x is revoked at time t or before. • At ⊆ Dt × Dt is the set of device approvals at time t. hx, yi ∈ At means that x approved y at time t or before. • Pt is the set of per-user-keys (PUKs). • Bt ⊆ Pt × Dt × Dt is the set of PUK boxes, where one device boxes the private keys of a PUK for itself or another device. That is, hk, x, yi ∈ Bt means that device x boxed k for device y at time t or before. It’s also worth defining, for convenience, a function that maps a device x to all the PUKs that it knows. Recall that x knows a PUK k if another device y boxed k for it; or symbolically, that hk, x, yi ∈ Bt . Note that in some cases, x = y. Definition B.2. Let pt : Dt → Pt be defined as: pt(x) = {k | ∃y ∈ Dt such that hk, y, xi ∈ Bt} We now define how a device family transitions from one configuration to another over time. Definition B.3. A device family consists of a sequence F = (F0, F1, . . . , Fn). Each of the Fi is a family state as defined above. F0 is the empty family state (all the components of the tuple are empty sets or functions with empty domain). Moreover, we require that the difference between any two consecutive states can be seen as the result of one of the following transitions below (which leave the components of the tuple which are not explicitly updated as unchanged):
DeviceAdd. Device x is provisioned at time t:
Preconditions: (a) x ∈/ Dt−1
Effects: (a) Dt ← Dt−1 ∪ {x} (b) dt ← dt−1 ∪ {hx, ti}
(c) Pt ← Pt−1 ∪ {k} for some new key k (d) Bt ← Bt−1 ∪ {hk, x, yi | y ∈ Dt\Rt} 2. DeviceRevoke. Device x is revoking devices S at time t:
Preconditions: (a) x ∈ Dt−1 (b) x ∈/ Rt−1 (c) S ⊆ Dt−1 (d) S ∩ Rt−1 = ∅
Effects: (a) Rt ← Rt−1 ∪ S (b) Pt ← Pt−1 ∪ {k} for some new PUK k (c) Bt ← Bt−1 ∪ {hk, x, yi | y ∈ Dt\Rt} Note that our model also allows the server to initiate a DeviceRevoke, in which case the PUK will not be rotated. We don’t model this transition here for simplicity.
PerUserKeyRotate. Device x rotates PerUserKey at time t (usually after another device self-revoked):
Preconditions: (a) x ∈ Dt−1 (b) x ∈/ Rt−1
Effects: (a) Pt ← Pt−1 ∪ {k} for some new PUK k. (b) Bt ← Bt−1 ∪ {hk, x, yi | y ∈ Dt\Rt}
BatchApprove. Device x approves devices at time t, meaning it approves all nonrevoked devices y such that dt(x) < dt(y).
Preconditions: (a) x ∈ Dt−1 (b) x ∈/ Rt−1
Effects: (a) At ← At−1 ∪ {hx, yi | y ∈ Dt\Rt , dt(x) < dt(y)} (b) Bt ← Bt−1 ∪ {hk, x, yi | y ∈ Dt\Rt , dt(x) < dt(y), k ∈ pt−1(x)} The thinking behind the batch approval operation is that a user should always revoke all devices when necessary, and therefore should be approving all the devices that can be approved whenever they approve any device. DeviceKeyRotate is not explicitly modeled here, as it would have the same preconditions and effects of a PerUserKeyRotate link. Note that At defines an undirected graph on the set Dt (where elements of At are the edges).
Definition B.4. We denote with et(x) ⊂ Dt the connected component of x in the graph defined on Dt by At . Let vt : Dt → N be the function defined as: vt(x) = min {dt(y) | y ∈ et(x)} We can define an equivalence relation between two devices with respect to a device family state Ft (which boils down to being part of the same connected component): Definition B.5. Given a device family Ft , ∀x, y ∈ Dt define x ≡t y iff vt(x) = vt(y). Note that, while revoked devices cannot perform new approvals, the approvals they make before being revoked are still considered part of the graph. For example, consider a family with 3 devices and the following transitions:
a is provisioned
b is provisioned
a approves b
c is provisioned
b approves c At this point (t = 5), we have: v5(a) = v5(b) = v5(c) = 1. Then (at t = 6) b self-revokes. v6(c) remains at 1, even though the only path from a to c at t = 6 crosses b, a revoked device. It’s worth noting that by definition of vt and the equivalence ≡t , the idea of approval is bidirectional. That is, if Alice provisions x then y, then approves y with x, then x and y are in the same equivalence class, even though she never approved x with y. We think this is a useful simplification. The rationale is that when y was added, Alice had access to the list of her devices on y which includes x, so we assume she implicitly approved x with y, since she didn’t revoke it when she had a chance.
Last updated