A Calculus of Temporal Uncertainty for Ordering Phone Timestamps over Clock Domains

1 Introduction

A timeline of phone evidence puts events in order by comparing timestamps. The comparison is safe only if the timestamps are readings of one clock and that clock was right. They rarely are. The call log is written by the device clock. A text message carries the time at which the network’s service centre received it. A cloud service adds its own server time, an application may format a local time, and a user types a time into a calendar entry. Every clock has its own error, and the errors are not independent: all readings of one clock share its offset. A reader who compares two readings of different clocks without saying how far the clocks may disagree has not shown which event came first.

A motivating example. Take a synthetic phone (Figure 1). A text message reached the service centre at 14:02:10 by the network clock and arrived on the phone at 14:02:12 by the device clock. A cloud service logged an upload at 14:02:25 by its server clock. The call log shows two calls, at 14:02:30 and 14:02:40 by the device clock. Did the upload precede the second call? Point timestamps say yes to all four ordering questions of Table 1. We assume that the device clock is within 120 s of true time, the network clock within 2 s and the server clock within 5 s, and that every reading is rounded to half a second. Under these bounds the answer is yes for the call at 14:02:40, because the arriving message limits how far ahead the device clock can be. For the call at 14:02:30 the answer is undecided, although the readings differ by 5 s. The order of the two calls is decided at once: both are read from the device clock, and its offset cancels. Table 1 gives six answers. Neither the point answer nor the interval answer alone shows which of these questions the evidence can settle; the calculus of this report does.

The problem. The literature on timelines treats timestamps as data to be normalised [1], as readings in time domains whose relations give a partial order [2], and as claims that need anchors against a trusted external time [3]. What is missing is a calculus that carries the uncertainty of each clock through the questions an examiner asks: which came first, how long between, were they together. It must say when the answer follows from the evidence, when it does not, and what to conclude when the stated bounds contradict each other.

Research questions. RQ1: which model of readings from several clocks gives sound order, duration and coincidence answers? RQ2: what does it decide beyond point timestamps and independent intervals, and with what error? RQ3: what happens when a stated bound is wrong, and can the calculus expose it? RQ4: what do phones show about the relation between the device clock and network time, and what share of cross-clock pairs is decided on them? Table 2 gives the answers in one line each.

Contributions. (1) A calculus in which readings belong to clock classes with shared, bounded offsets, evidence is a set of difference constraints, and shortest paths give exact answers (Sections 3 and 4). (2) Five properties with proofs and counterexamples: exactness, a closed form for the separation at which two readings are ordered, monotone refinement, conflict as an audit of assumptions, and a robustness radius (Section 4). (3) A checker and a synthetic evaluation with known event times, including bounds that are too small (Sections 5 and 6.2). (4) A measurement on Android phones of what the network arrival time of text messages says about the device clock, and of the share of message-call pairs it orders (Section 6.3).

2 Background and related work

2.1 Timestamps and clocks in forensic timelines

Early work on timestamps asked whether a clock was right. Willassen defined a clock hypothesis as a deviation from a common base clock and gave two tests that refute it, the first when causally connected events carry timestamps in the wrong order once the deviation is removed [4]. Gladyshev and Patel bound the time of an event by intervals propagated along happened-before relations, with a minimal delay on each relation, and note that a wrongly specified delay gives wrong results [6]. Marrington and colleagues automated the detection of such inconsistencies in timelines [24]. Schatz and colleagues correlate local timestamps with a second source of timestamps to infer the temporal behaviour of a computer [5]. Kaart and Laraghy studied timestamps on Android; as described by Vanini and colleagues, they compared operator timestamps held in messages with local ones on one phone to determine the time zone and clock settings [7, 3].

Three recent papers are close. Hornung and colleagues give a formal model of timestamp normalisation and show that normalising to a common domain leaves timestamps incomparable when their resolutions differ, so that the order of events cannot always be determined; the discrepancy between a device clock and true time is left to future work, by extending time anchors [1]. A companion paper by Hornung, Jonker and van Beek treats file timestamps formally [8]. Dreier and colleagues treat each timing source as a time domain with its own timeline and connect the domains through relations found in the evidence, which turns the flat timeline into a partial order, a hyper timeline [2]. They note that coincidence relations between domains can reduce the partial order towards a total order, that unknown skew prevents a direct comparison of readings, and that an earlier tool gives low-level timestamps a minimum and a maximum to express their resolution [25]. Vanini and colleagues define time anchors: artifacts that hold both a system time and a time from an external source taken as correct. The skew is the difference of the two; a few seconds are accepted as no skew, and anchors bracket other artifacts between them. Their list of anchoring artifacts includes a received message that records a sent and a received time [3]. Jang and colleagues compare device time with external time on Android phones to detect a manipulated clock and to estimate skew [9]. A survey by Breitinger, Studiawan and Hargreaves harmonises the terminology of timeline-based event reconstruction and lists open challenges [10].

2.2 Temporal reasoning and uncertain time

Dechter, Meiri and Pearl introduced temporal constraint networks, and in particular the simple temporal problem: time points, each pair constrained by an interval for their difference. Consistency is the absence of a negative cycle in the distance graph, and shortest paths give the minimal network, which holds the exact bounds [11]. Allen’s interval algebra reasons qualitatively about relations between intervals [12]. Dyreson and Snodgrass handle events whose valid time is only known to lie in a set of possible instants [13]. In distributed systems Lamport defined happened-before as a partial order and gave a bound on clock synchrony [14], Marzullo and Owicki studied how a distributed time service keeps the error of its time small [15], and Spanner exposes the uncertainty of its clock as an interval whose bounds are guaranteed to contain true time [16].

2.3 What the phone offers as clock evidence

A text message arrives with two times. The Android documentation describes the stored columns as the date the message was received and the date it was sent [17, 18]. In the code we read, the telephony provider defaults the first to the current system time, and the Messaging application of the Android Open Source Project writes the current system time of the receiving phone as the first (the sent time instead, if that clock is before September 2011) and the service-centre timestamp of the first part of the message as the second [18]. For a short message that timestamp is the time the message arrived at the service centre, to one second; the centre may alter it slightly to keep the stamps of messages to one phone distinct [19]. The first is a reading of the device clock and the second of the network clock, and a message cannot arrive before it reached the service centre. Earlier Lab reports measured how often device clocks step and fail simple checks [20], how the clocks behind reset indicators differ (UTC against device local time, and a header that prints a constant year) [21], and which stores keep records how long [22].

2.4 Position of this work

The machinery of this report is classical: a simple temporal network [11], with the interval clocks of distributed systems [15, 16]. We do not claim it as new, and three of its uses in forensics are not new either. Event time bounding by intervals along causal relations with minimal delays is the special case of our model without clock offsets [6]. Refuting a clock hypothesis by a causal pair that is ordered the wrong way is the idea of Willassen’s first test [4]. Reading the sent and received times of a message as a time anchor is in Vanini and colleagues [3], and operator timestamps in messages were compared with local ones on an Android phone before [7]. What we did not find in the forensic literature we searched (Section 5.4) is the combination of five things. (1) Readings modelled as members of clock classes that share an offset, so that the order of two readings of one clock holds whatever its offset is. (2) A closed form for the separation at which two readings are ordered, for each pair of classes, with bounds on offsets and an exactness theorem for every order, duration and coincidence query. (3) The message pair as a one-sided inequality that needs bounds, not a clock taken as correct, and its measurement on 13 phones. (4) Contradiction among stated bounds of several classes returned as a named set of constraints, which makes the calculus an audit of its own assumptions: Willassen’s test for one clock hypothesis, extended. (5) A scored comparison with point timestamps and independent intervals on phones with known event times. The hyper timeline of Dreier and colleagues [2] is a special case: its precedence and coincidence relations are “not later than” constraints of Section 3.4 (a coincidence has a range of zero) without numbers, and the calculus adds the numeric offsets. Time anchors [3] become constraints that tie two classes. The incomparability that Hornung and colleagues derive from differing resolutions [1] is the resolution term ρ of Theorem 2; clock offset is what the calculus adds. The Lab report on absence [23] asks whether an event could have been recorded; this report asks whether the order of recorded events can be read.

3 The calculus

3.1 Events, readings and clock classes

An event e happened at an unknown true time τ_e. A clock class c is a clock domain over a period in which its offset is constant, or varies at a bounded rate. The offset θ of a reading is the reading minus true time. A class states bounds a_c ≤ θ ≤ b_c (either may be infinite) and a drift bound δ_c ≥ 0. An observation o = (e, c, r, ρ) says that event e was read as r in class c with resolution ρ: the largest error of the reading in either direction (rounding, truncation). Table 3 lists the classes of this study. A phone changes class when a clock is set: each period between two settings is one class, and the step between two classes is itself evidence (Section 3.4).

3.2 Worlds

A world assigns a true time τ_e to every event and an offset θ_o to every observation such that:

• (W1) r_o − ρ_o ≤ τ_e + θ_o ≤ r_o + ρ_o;
• (W2) a_c ≤ θ_o ≤ b_c for an observation in class c;
• (W3) all observations of a class with δ = 0 have the same offset; for a class with δ > 0, two observations o, o′ satisfy |θ_o − θ_o′| ≤ δ|r_o − r_o′| / (1 − δ);
• (W4) the relations of Section 3.4 hold.

(W3) for δ > 0 follows from the assumption that the offset changes by at most δ per second of true time: the true elapsed time is within a factor 1/(1−δ) of the elapsed reading. We state (W3) for the recorded readings; the exact bound would add δ(ρ_o + ρ_o′)/(1−δ), which the evaluation does not need because it uses no drifting class. A timeline is consistent if it has a world. The stated bounds are assumptions of the examiner; the calculus returns what follows from them.

3.3 Queries

For events e, f the range of τ_f − τ_e is the set of its values over all worlds. Order: e is before f if τ_e < τ_f in every world, after if the opposite holds in every world, otherwise undecided. Duration: the range itself. Coincidence within Δ: yes if |τ_f − τ_e| ≤ Δ in every world, no if it exceeds Δ in every world, otherwise undecided. The robustness radius of a decided order is the ratio of the distance of the range’s centre from zero to its half-width: it measures the slack of the decision. For two single readings with no further evidence it is exactly the factor by which every bound and resolution could be multiplied before the decision fails (Proposition 5); with further evidence it is the factor by which the range can be widened about its centre.

3.4 Evidence

Four kinds of evidence add constraints. A not-later-than relation says τ_f − τ_e ∈ [lo, hi]: the arrival of a message is not earlier than its sending (lo = 0), a sequence number or a log line number orders two records, a process cannot finish before it starts. A known time says τ_e ∈ [lo, hi], as a receipt or a trusted external record does. An offset relation says θ_c′ − θ_c ∈ [lo, hi] for two classes without drift, as a documented clock step does. An anchor is an event read in two classes: eliminating its true time gives an offset relation θ_c′ − θ_c ∈ [r′ − r − ρ − ρ′, r′ − r + ρ + ρ′]. Combined with a not-later-than relation between two different events read in two classes, the message gives a one-sided offset relation: θ_W − θ_N ≤ r_arrival − r_sent + ρ_W + ρ_N.

3.5 The checker

Every constraint of Section 3.2 and 3.4 is a difference constraint on the variables τ_e and −θ_o, plus a node for time zero. The set of worlds is therefore the solution set of a simple temporal network [11]. The checker builds the distance graph and runs Floyd–Warshall; the range of τ_f − τ_e is read from two entries of the result, and a negative cycle shows inconsistency and names the constraints on it. For populations of events with one reading each, a class-level engine closes only the small graph of classes, so each pair costs a constant number of operations (Proposition 7). The code is standard-library Python (Section Artifact Availability).

4 Properties

Write d(u,v) for the shortest-path distance from u to v in the distance graph of a consistent timeline, where an edge from u to v of weight w stands for the constraint x_v − x_u ≤ w.

Proof. Every world satisfies each edge, so summing the edges of a path bounds τ_f − τ_e by the weight of the path; the shortest path gives τ_f − τ_e ≤ d(e,f), and the same with e and f exchanged gives the lower end. For tightness, set x_v = d(e,v) for every node v that can be reached from e. For every edge (u,v,w) between reached nodes the triangle inequality gives d(e,v) ≤ d(e,u) + w. No edge leads from a reached node to an unreached one; give the unreached nodes a solution of the constraints among them (one exists, the timeline being consistent) plus a constant large enough that every edge from them into the reached nodes holds. Then x satisfies all constraints; subtracting the value of the time-zero node gives a world, with x_e = 0 and x_f = d(e,f) (differences are unchanged). The lower end is attained by the same construction from f. If an end is infinite, no path constrains that direction and the difference is unbounded there. Since both ends are attained by worlds, a pair is undecided exactly when the range meets both sides of the question. Consistency is the absence of a negative cycle [11]. □

Proof. Eliminate the offsets: τ_f − τ_e = Δ − (θ_f − θ_e) − (ν_f − ν_e) with reading errors ν in [−ρ, ρ] that are free. In (a) the offsets are equal, so their difference is zero and the bounds drop out. In (b) the difference of offsets ranges over [−m, m], m the smaller of the drift allowance and the width of the bounds. In (c) the two offsets vary independently over their intervals; in (d) their difference ranges over the closure interval. Each range is attained, by Theorem 1 or directly, because the variables are free within the intervals. The statements were also checked by enumeration over an integer grid (Table 5). □

Corollary 2.1 (what independent intervals lose). If each reading is turned into an interval for true time on its own, [r − ρ − b, r + ρ − a], two readings of one class are ordered only when |Δ| > σ + (b − a). The calculus needs |Δ| > σ. When a class has no useful bound (a user-set clock, b − a = ∞) independent intervals order nothing within the class and the calculus orders every pair whose readings differ by more than the resolution. Table 4 shows the effect on the profile of Section 5.2.

Proof. The first statement is Theorem 3.1 of Dechter and colleagues [11]. The edges of a simple negative cycle are an inconsistent system by themselves; if one is removed, the remaining edges form a path, which has no cycle and so a solution. A world of the true situation satisfies every true constraint, so a timeline with no world contains a false one. □ The converse fails: a false bound that no reading contradicts is not detected. Table 7 measures how often that happens.

Proof. By Theorem 2 the range is linear in λ: its centre does not change and its half-width is λw. The range excludes zero if and only if |m| > λw. □ In Table 1 the first decision has radius 1.06: its range can be widened by about 6 per cent about its centre before it contains zero. A decision with radius 10 survives a tenfold widening.

Proof. (a) The range is the point Δ. (b) The edges are the relations. (c) Independent intervals use a subset of the constraints and by Theorem 3 the calculus decides everything they decide; Theorem 2(a) gives a pair that independent intervals cannot order. (d) The relation “τ_e < τ_f in every world” is asymmetric and transitive. □ The path through an anchor shows that pairwise evaluation is incomplete: in the package check P7 a pair of readings from a device clock and from an unbounded application clock is undecided on its own, and decided through a third reading of the same event in the device clock.

Proposition 7 (cost). The distance graph has one node for time zero, one per event, one per drift-free class and one per observation of a class with drift; Floyd–Warshall costs cubic time in the number of nodes. For populations of single readings only the classes enter the closure, and every pair is answered in constant time from the closure (check T1 compile of Table 5: the class-level engine equals the full solver).

Limits. The calculus is exact for its model and only for it. (i) A class has one offset or a bounded drift; a clock that steps without evidence must be cut into classes, and the class of a period nobody observed has no bound. (ii) Reading errors are free within the resolution and independent between readings. (iii) The bounds are the examiner’s; the calculus cannot tell a too-wide bound from a right one, and a too-narrow bound is exposed only by a second reading (Theorem 4). Section 6.2 measures (iii).

5 Evaluation design

5.1 Mechanical checks

We wrote the checks of Table 5 before the evaluation. Random consistent timelines with a hidden true world test soundness, exactness and convexity; brute-force enumeration on an integer grid tests the closed forms of Theorem 2; random extensions test monotonicity; inconsistent timelines test the cycle of Theorem 4; and scaled bounds test the radius of Proposition 5.

5.2 Synthetic phones

A synthetic phone has four stores and known true event times. Calls (20) are read in the device clock W. Messages (30) give two events each: the sending at the service centre, read in the network clock N, and the arrival, read in W, later by a latency (90 per cent exponential with mean 3 s, 10 per cent with mean 120 s). App events (30) are read in the server clock S, and 30 per cent of them also in W. Notes (10) are read in the user clock U. Events cluster in 12 bursts over three days (standard deviation 120 s). The true offsets are drawn at random: W within 1 s with probability 0.80, within 10 s with 0.15 and within 60 s with 0.05; N within 2 s, S within 5 s, U within 120 s. The declared bounds are W 60, N 3, S 10 and U 300 s, so they hold. Resolutions are 0.5 s, and 30 s for U. All values are assumptions of the simulation (PARAMS in the package), chosen by us and not measured.

The population is every pair of events of different stores whose true times differ by at most 600 s, excluding the two events of one message, whose order is the relation itself. A method answers each pair with before, after or undecided and is scored against the true order. The methods are point timestamps (P), independent intervals (I), the calculus with the class bounds alone (C0), and the calculus with the class bounds, the anchors (app events read in S and W) and the not-later-than relation of every message (C1). Coincidence within 5 s is scored the same way. The runs are repeated with every declared bound multiplied by κ = 0.5 and 0.25 (RQ3; for W the declared bound equals the true maximum, for N, S and U it is 1.5, 2 and 2.5 times larger), with the declared bound on W varied from 1 to 3600 s (Figure 2), and with a step of the device clock between two sets of calls.

5.3 Phones of the research corpus

We read 14 Android full file system extractions from the Lab’s research corpus; 13 of the 14 phones hold incoming text messages that carry a sent time. For each incoming message we read the arrival time (device clock) and the sent time (network clock), and for each call its time; no text, number or name was read. Messages whose sent time equals their arrival time to the millisecond carry the device clock in both fields and were set aside; we fixed this rule after the first look at the counts, because their share is large on two phones. The tightest anchor of a phone is the smallest difference between arrival and sent time plus the two resolutions (1 ms and 1 s): by Section 3.4 it bounds the device offset minus the network offset from above, at the time of its message. We use it in two ways. The phone-wide anchor is the tightest anchor over the whole history of a phone and assumes one device offset for that history. The local anchor of a pair is the tightest anchor among the messages that arrive within 7 days of the pair (windows of 1 and 30 days as a check) and assumes one offset for those days only. We added the local anchor after we found that the phone-wide anchor reverses pairs far from the message that sets it (Section 6.3). For the pairs we take every message and every call whose readings differ by at most 600 s. There is no true order on the corpus, so the answer of a method is compared with the order of the readings: it agrees, it reverses, or it is undecided. Priors on the device clock are 5, 60 and 3600 s, and on the network clock 5 s. A phone whose anchor contradicts the prior is reported and set aside from the pair counts of that prior. For clock steps we use the aggregates of an earlier report [20] and no new reading of time-sync records.

5.4 Literature search

We queried arXiv, Zenodo, Crossref, OpenAlex, dblp and Semantic Scholar with 24 queries on timestamp normalisation, time anchors, hyper timelines, clock skew and manipulation, temporal constraint networks, interval clocks and message timestamps. Some interfaces answered only in part, and the ACM Digital Library, DFRWS and Forensic Science International: Digital Investigation cannot be queried by machine, so we searched them through a web search restricted to their sites. The queries and results are kept in the Lab’s private notes. We read the abstracts of the closest papers and the text of those marked as fetched in the reference list.

6 Results

6.1 The checker agrees with the proofs

All 14 mechanical checks pass (Table 5). The extremal worlds of Theorem 1 are worlds in every tested case and attain both ends of every range; the closed forms of Theorem 2 equal brute-force enumeration in every case; the class-level engine equals the full solver; and the returned conflict cycles are inconsistent and minimal. The checks test the code against the proofs and the proofs against enumeration; they do not test the model against phones.

6.2 Synthetic phones

Bounds correct. Point timestamps order 96.9 per cent of the 147,669 near-simultaneous cross-store pairs correctly and 3.1 per cent wrongly (Table 6). Independent intervals never err and order 59.7 per cent. The calculus with class bounds orders 65.0 per cent, and with the anchors and the message relations 80.3 per cent, with no wrong decision among 147,669 pairs (RQ2). The 3.1 per cent for point timestamps is an average over pair types and depends on the offsets and the pair window we chose: pairs that involve a user-entered time (19.6 per cent of the pairs) are 12.7 per cent wrong, all other pairs 0.75 per cent; with a window of 60 s the share is 9.6 per cent and with 3,600 s it is 2.5 per cent (the package with the window changed). On the pairs without a user-entered time, C1 orders 97.7 per cent and independent intervals 72.6 per cent. The gain of C0 over I is the same-class cancellation of Theorem 2; the gain of C1 over C0 is the chain through the anchors and the not-later-than relations: a poorly bounded device clock is pinned by the well-bounded network and server clocks. For coincidence within 5 s, point timestamps answer 1.74 per cent of the pairs wrongly; the calculus answers 79.1 per cent and leaves 20.9 per cent undecided, with no wrong answer.

Width of the declared bound. The advantage of the evidence grows as the declared bound on the device clock widens (Figure 2). For pairs of a device-clock and a network-clock reading, independent intervals order 93.8 per cent of the pairs at a bound of 10 s, 73.3 per cent at 60 s, 9.4 per cent at 300 s and none at 3600 s; the calculus with the evidence orders 92.2, 96.6, 96.1 and 96.3 per cent. With a wide bound on the device clock the evidence fixes the offset relative to the network clock from the messages and the anchors, so the width of the prior stops mattering. At declared bounds below 60 s the bound fails on some phones (the true device offset exceeds it on about 4 per cent of phones at 10 s and on more than 20 per cent at 1 s), the checker flags those phones, and their pairs count as undecided; this is why independent intervals are ahead at 1 to 10 s.

Bounds too small. When every declared bound is multiplied by 0.5 or 0.25 (Table 7), the true world can lie outside the model. The checker returns a conflict on 9 of 300 phones at one half and 35 at one quarter. At one quarter, 55 of the 265 phones that are not flagged have a wrong C1 decision (a flagged phone has no decision, so none can be both). Independent intervals order 0.19 per cent of the pairs wrongly at one quarter against 0.09 per cent for C1. Thus a bound that is too small is exposed when two readings contradict it, and otherwise the decisions can be wrong with no signal (RQ3). The robustness radius of Proposition 5 is the tool for the second case: a decision between two single readings with a radius above the factor by which a bound might be wrong survives it.

Steps of the device clock. A step that separates two sets of events is invisible in point timestamps (Table 8). For steps of 60 to 600 s, point timestamps order 5.9 per cent of the pairs across the step wrongly; for steps of 600 to 3600 s, 43.8 per cent. The calculus without the step leaves every such pair undecided, because the bound of each segment is as wide as the step could be, and it makes no error; with the step as evidence of ±1 s it orders every pair. The 100 per cent undecided without the step follows from the ±4000 s bound we chose, which exceeds every step; the table shows the mechanism, not a rate, and it does not say how often a ledger exists on a real phone.

6.3 Phones of the research corpus

Clock evidence from earlier reports. Table 9 restates the aggregates of [20]. In the time-sync records of 31 iPhones, the wall clock stepped against the kernel clock by 1 s or more between 66,549 of 500,548 consecutive record pairs, and every iPhone shows at least one such step; 23 show a step of more than a minute and 18 of more than an hour. Four of seven Android bug reports record a change of the clock since boot. So for the iPhones of the corpus a device-clock class that spans months has no constant offset at the scale of seconds. Same-class cancellation (Theorem 2(a)) holds within a period without steps, and the resolution assigned to a class must cover the small steps that the records show; the last sentence of the Decisions paragraph reports a sensitivity to that resolution on Android.

The anchor. On 13 of the 14 Android phones the incoming messages carry a network sent time (Table 10); on 4 of them we set aside 23,934 messages whose sent time equals the arrival time. The median delay between the two is 1.9 s on a typical phone, and 70.6 per cent of messages arrive within 2 s of their sent time. The tightest anchor bounds the device clock above the network clock by at most 1.9 s on all 13 phones (median 0.3 s). On 5 phones the bound is negative: some messages arrived before the service centre says they were sent, by up to 23.6 s. That cannot happen if both clocks are right, so on these phones the device clock was behind the network clock by at least the bound, or the service-centre clock was ahead (Figure 3). Under a 5 s bound on both clocks the difference of offsets cannot be below −10 s, and the 2 phones with a bound below that value are refuted. At 60 s none is. On the 2 refuted phones the early messages lie on 4 and 17 separate days within histories of several years, so the 5 s bound is refuted for those days, not shown to fail for the whole life of the phone.

Decisions. Table 11 gives the order decisions for the pairs of a message and a call. With a prior of 60 s on the device clock, independent intervals order 74.8 per cent of the pairs of a network sent time and a call time. The phone-wide anchor raises this to 89.7 per cent and the local anchor to 85.1 per cent (RQ4); with windows of 1 and 30 days the local share is 84.6 and 85.4 per cent. The phone-wide anchor reverses the order of the readings in 45 pairs on 3 phones (0.48 per cent): the call is shown to have happened before the sending time of the message although its reading is later. These pairs lie on phones with a negative bound, and each lies more than 1,100 days from the message that sets the bound; the local anchor reverses none. We therefore take the local figures as the result and the phone-wide figures as what the constant-offset assumption would give. The 14.9 per cent that the local anchor leaves undecided are pairs for which the readings are too close for the evidence. For pairs of the arrival time and a call, both in the device clock, independent intervals order 66.7 per cent at 60 s and the calculus 100.0 per cent, because the offset cancels. At a prior of 3600 s independent intervals order no pair, within the device clock or across clocks, while the calculus keeps 46.8 per cent (local) or 51.4 per cent (phone-wide) of the cross-clock pairs through the anchor. When the resolution of the device clock is set to 1 s or 5 s, to cover the small steps of Table 9, the phone-wide calculus orders 99.5 and 96.2 per cent of the arrival-call pairs, and 86.7 and 82.7 per cent of the sent-call pairs, at the prior of 60 s.

7 Discussion

What a report should state. A statement about order or duration needs a small table: the clock classes involved, a bound for each with its basis, the evidence relating them, and for each decision the range and the radius. Where the answer is undecided, the report says which bound would settle it. Table 1 is such a table for one example. The calculus does not find bounds. It makes explicit what a conclusion rests on and returns a conflict when the bounds contradict each other, as in the second example of the package, where a message that arrives 40 s before the service centre received it contradicts bounds of 30 s on the device clock and 2 s on the network clock, and the checker names the five constraints involved. An earlier Lab report found a similar situation on a real phone: a candidate date estimate whose central assumption failed by 526 days, exposed by comparing two anchors [21]. In this calculus the two anchors would be two offset relations that cannot hold together.

Anchors to look for. The message is one anchor. The calculus makes any reading of one event in two clocks usable: a device record that contains a server-supplied time, a network time update in a log, a receipt. We measured only the message. The causal relation bounds the device clock from one side only; a second anchor would bound it from the other.

The device clock is not constant. The aggregates of Table 9 show that device clocks step by seconds often and by minutes or hours rarely. A class that spans a long period needs a resolution large enough for the small steps and a cut at each larger step. The cut needs evidence; the earlier report shows where it can come from on an iPhone, the time-sync records. We did not look for a source on Android. Where no ledger exists and the only bound is wider than the step, the right answer is undecided (Table 8).

8 Threats to validity and limitations

Construct. The model assumes a constant offset within a class, a drift bound, and reading errors that are free within the resolution and independent. A clock that slews continuously, a service that writes the time of a batch, or an application that rounds to the hour breaks one of these; the remedy is a class with a larger resolution, not a different theorem. The synthetic parameters of Section 5.2 are our choices. The results show how the calculus behaves under them and say nothing about how large the true offsets of phones are.

Internal. The tightest anchor is a minimum over messages, so one wrong sent time at the service centre sets it, and it holds at the time of that message. Using it for a whole history assumes one offset for years, which the clock steps of Table 9 and the early messages on a few days of the refuted phones contradict; the local anchor shortens the assumption to 15 days and does not remove it. The service centre may alter its stamp slightly [19], and a message restored from an earlier handset may keep that handset’s arrival time; we did not test either. Across the corpus 203 messages on 5 phones arrive more than 2 s before their sent time; on each of the 2 refuted phones this is not one message but 15 to 184 of them. We did not test the service-centre clock. The rule that sets aside messages with equal times was fixed after the first look at the counts. The sent time is the service-centre time for the Messaging application we read [18]; other applications, including those of the vendors of most phones in the corpus, may write the field differently, and the equal-time rule catches only one such case.

External. The corpus phones are 14 Android phones, most from one vendor, and they are not a sample of any population. The step evidence is from iPhones, the anchor from Android, and the pairs are messages and calls only. No claim here transfers to other vendors, other message applications or other years without a new measurement.

Conclusion. There is no true order on the corpus, so the decisions on real phones are compared with the readings and with each other, not with what happened. The reversals of the phone-wide anchor are consequences of its constant-offset assumption (Section 6.3). A controlled run, with a phone whose clock is set and logged, would measure the error rate of the calculus on real stores; we did not perform one.

Limitations. The corpus evaluation covers one anchor on Android. There is no iOS anchor, no server-time anchor, no step ledger and no measurement of the user clock. The synthetic evaluation compares three simple methods. It does not compare the calculus with another formal model of timestamps, because we found none that offers numeric offsets on phone data. The calculus is not a method for finding clock manipulation; it takes bounds as input and says what follows.

9 Conclusion

Two readings of one clock share its error; readings of different clocks do not. A calculus that keeps track of which is which orders pairs that point timestamps cannot be trusted on and declines pairs that they order too readily. It is exact for its model and it exposes contradictions among its assumptions. On synthetic phones it made no wrong decision under correct bounds, where point timestamps ordered 3.1 per cent of near-simultaneous pairs wrongly. On 13 Android phones the arrival of a text message bounded the device clock above network time by 1.9 s or less at each phone’s tightest point, and refuted a 5 s bound on 2 of them.

Future work, in order of value: (1) a controlled run on a phone whose clock is set and logged, to measure the error of the decisions on real stores; (2) more anchors, first server-supplied times in application records and network time updates in logs; (3) a step ledger for Android; (4) an iOS anchor; (5) a hyper-timeline front end that adds classes and bounds to a partial order.