1 \documentclass[11pt]{article}
\r
2 \newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}
\r
6 \usepackage{graphicx}
\r
7 \usepackage{mathrsfs}
\r
8 \usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx
\r
10 \newtheorem{theorem}{Theorem}
\r
11 \newtheorem{prop}{Proposition}
\r
12 \newtheorem{lem}{Lemma}
\r
13 \newtheorem{defn}{Definition}
\r
14 \newcommand{\note}[1]{{\color{red} \bf [[#1]]}}
\r
15 \newcommand{\push}[1][1]{\hskip\dimexpr #1\algorithmicindent\relax}
\r
21 Each device has: user id + password
\r
24 hash1(user id), hash1(password)
\r
26 Symmetric Crypto keys is:
\r
27 hash2(user id | password)
\r
29 Server has finite length queue of entries + max\_entry\_identifier +
\r
32 \subsection{Entry layout}
\r
35 \item Sequence identifier
\r
36 \item Random IV (if needed by crypto algorithm)
\r
37 \item Encrypted payload
\r
42 \item Sequence identifier
\r
43 \item Machine id (most probably something like a 64-bit random number
\r
44 that is self-generated by client)
\r
45 \item HMAC of previous slot
\r
47 \item HMAC of current slot
\r
50 A data entry can be one of these:
\r
52 \item All or part of a Key-value entry
\r
53 \item Slot sequence entry: Machine id + last message identifier
\r
54 \newline {The purpose of this is to keep the record of the last slot
\r
55 from a certain client if a client's update has to expunge that other
\r
56 client's last entry from the queue. This is kept in the slot until
\r
57 the entry owner inserts a newer update into the queue.}
\r
58 \item Queue state entry: Includes queue size \newline {The purpose
\r
59 of this is for the client to tell if the server lies about the number
\r
60 of slots in the queue, e.g. if there are 2 queue state entry in the queue,
\r
61 e.g. 50 and 70, the client knows that when it sees 50, it should expect
\r
62 at most 50 slots in the queue and after it sees 70, it should expect
\r
63 50 slots before that queue state entry slot 50 and at most 70 slots.
\r
64 The queue state entry slot 70 is counted as slot number 51 in the queue.}
\r
65 \item Collision resolution entry: message identifier + machine id of a
\r
67 \newline {The purpose of this is to keep keep track of the winner of
\r
68 all the collisions until all clients have seen the particular entry.}
\r
71 \subsection{Live status}
\r
73 Live status of entries:
\r
75 \item Key-Value Entry is dead if either (a) there is a newer key-value pair or (b) it is incomplete.
\r
77 \item Slot sequence number (of either a message version data
\r
78 or user-level data) is dead if there is a newer slot from the same machine.
\r
80 \item Queue state entry is dead if there is a newer queue state entry.
\r
81 {In the case of queue state entries 50 and 70, this means that queue state
\r
82 entry 50 is dead and 70 is live. However, not until the number of slots reaches
\r
83 70 that queue state entry 50 will be expunged from the queue.}
\r
85 \item Collision resolution entry is dead if this entry has been seen
\r
86 by all clients after a collision happens.
\r
89 When data is at the end of the queue ready to expunge, if:
\r
91 \item The key-value entry is not dead, it must be reinserted at the
\r
92 beginning of the queue.
\r
94 \item If the slot sequence number is not dead, then a message sequence
\r
95 entry must be inserted.
\r
97 \item If the queue state entry is not dead, it must be reinserted at the
\r
98 beginning of the queue.
\r
103 Client sends a sequence number. Server replies with either: all data
\r
104 entries or all newer data entries.
\r
106 \paragraph{Writes:}
\r
107 Client sends slot, server verifies that sequence number is valid,
\r
108 checks entry hash, and replies with an accept message if all checks
\r
109 pass. On success, client updates its sequence number. On failure,
\r
110 server sends updates slots to client and client validates those slots.
\r
112 \paragraph{Local state on each client:}
\r
113 A list of machines and the corresponding latest sequence numbers.
\r
115 \paragraph{Validation procedure on client:}
\r
117 \item Decrypt each new slot in order.
\r
118 \item For each slot:
\r
119 (a) check its HMAC, and
\r
120 (b) check that the previous entry HMAC field matches the previous
\r
122 \item Check that the last-message entry for our machine matches the stored HMAC of our last message sent.
\r
123 \item For all other machines, check that the latest sequence number is
\r
124 at least as large (never goes backwards).
\r
125 \item That the queue has a current queue state entry.
\r
126 \item That the number of entries received is consistent with the size
\r
127 specified in the queue state entry.
\r
130 Key-value entries can span multiple slots. They aren't valid until
\r
133 \subsection{Resizing Queue}
\r
134 Client can make a request to resize the queue. This is done as a write that combines:
\r
135 (a) a slot with the message, and (b) a request to the server. The queue can only be expanded, never contracted; attempting to decrease the size of the queue will cause future clients to throw an error.
\r
137 \subsection{Server Algorithm}
\r
138 $s \in SN$ is a sequence number\\
\r
139 $sv \in SV$ is a slot's value\\
\r
140 $slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\ \\
\r
142 \textit{SL = set of live slots on server} \\
\r
143 \textit{max = maximum number of slots (input only for resize message)} \\
\r
144 \textit{n = number of slots} \\ \\
\r
145 \textbf{Helper Function} \\
\r
146 $MaxSlot(SL_s)= \tuple{s, sv} \mid \tuple{s, sv}
\r
147 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \geq s_s$ \\
\r
148 $MinSlot(SL_s)= \tuple{s, sv} \mid \tuple{s, sv}
\r
149 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \leq s_s$ \\
\r
150 $SeqN(slot_s = \tuple{s, sv})=s$ \\
\r
151 $SlotVal(slot_s = \tuple{s, sv})=sv$ \\
\r
153 \begin{algorithmic}[1]
\r
154 \Function{GetSlot}{$s_g$}
\r
155 \State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$}
\r
159 \begin{algorithmic}[1]
\r
160 \Function{PutSlot}{$s_p,sv_p,max'$}
\r
161 \If{$(max' \neq \emptyset)$} \Comment{Resize}
\r
162 \State $max \gets max'$
\r
164 \State $\tuple{s_n,sv_n} \gets MaxSlot(SL)$\Comment{Last sv}
\r
165 %\State $s_n \gets SeqN(\tuple{s_n,sv_n})$
\r
166 \If{$(s_p = s_n + 1)$}
\r
168 \State $\tuple{s_m,sv_m} \gets MinSlot(SL)$\Comment{First sv}
\r
169 \State $SL \gets SL - \{\tuple{s_m,sv_m}\}$
\r
170 \Else \Comment{$n < max$}
\r
171 \State $n \gets n + 1$
\r
173 \State $SL \gets SL \cup \{\tuple{s_p,sv_p}\}$
\r
174 \State \Return{$(true,\emptyset)$}
\r
176 \State \Return{$(false,\{\tuple{s,sv}\in SL \mid
\r
182 \subsection{Client Algorithm}
\r
183 \subsubsection{Reading Slots}
\r
184 \textbf{Data Entry} \\
\r
185 $de$ is a data entry \\
\r
186 $k$ is key of entry \\
\r
187 $v$ is value of entry \\
\r
188 $kv$ is a key-value entry $\tuple{k,v}$, $kv \in DE$ \\
\r
189 $ss$ is a slot sequence entry $\tuple{id,s_{last}}$,
\r
190 id + last s of a machine, $ss \in DE$ \\
\r
191 $qs$ is a queue state entry (contains $max$ size of queue), $qs \in DE$ \\
\r
192 $cr$ is a collision resolution entry $\tuple{s_{col},id_{col}}$,
\r
193 s + id of a machine that wins a collision, $cr \in DE$ \\
\r
194 $DE$ is a set of all data entries, possibly of different types, in a single message \\
\r
195 $s \in SN$ is a sequence number \\
\r
196 $id$ is a machine ID\\
\r
197 $hmac_p$ is the HMAC value of the previous slot \\
\r
198 $hmac_c$ is the HMAC value of the current slot \\
\r
199 $Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\
\r
200 $slot_s = \tuple{s, E(Dat_s)} =
\r
201 \tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\
\r
203 \textit{$d$ = delta between the last $s$ recorded and the first $s$ received} \\
\r
204 \textit{$id_{self}$ = machine Id of this client} \\
\r
205 \textit{$max_g$ = maximum number of slots (initially $max_g > 0$)} \\
\r
206 \textit{m = number of slots stored on client (initially $m = 0$)} \\
\r
207 \textit{$sl_{last}$ = info of last slot in queue =
\r
208 $\tuple{s_{last},sv_{last},id_{last}}$ (initially $\emptyset$)} \\
\r
209 \textit{DT = set of $\tuple{k,v}$ on client} \\
\r
210 \textit{MS = associative array of $\tuple{id, s_{last}}$ of all clients on client
\r
211 (initially empty)} \\
\r
212 \textit{$LV$ = live set of $kv$ entries on client, contains
\r
213 $\tuple{kv,s}$ entries} \\
\r
214 \textit{$SS_{live}$ = live set of $ss$ entries on client} \\
\r
215 \textit{$CR_{live}$ = live set of $cr$ entries on client} \\
\r
216 \textit{$MS_g$ = set MS to save all $\tuple{id, s_{last}}$ pairs while
\r
217 traversing DT after a request to server (initially empty)} \\
\r
218 \textit{SK = Secret Key} \\
\r
219 \textit{$SM$ = associative array of $\tuple{s, id}$ of all slots in previous reads
\r
220 (initially empty)} \\ \\
\r
221 \textbf{Helper Functions} \\
\r
222 $MaxSlot(SL_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}
\r
223 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \geq s_s$ \\
\r
224 $MinSlot(SL_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}
\r
225 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \leq s_s$ \\
\r
226 $Slot(SL_s,s_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}
\r
227 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s = s_s$ \\
\r
228 $SeqN(\tuple{s, sv})=s$ \\
\r
229 $SlotVal(\tuple{s, sv})=sv$ \\
\r
230 $CreateLastSL(s,sv,id)=\tuple{s,sv,id}=sl_{last}$ \\
\r
231 $CreateEntLV(kv_s,s_s)=\tuple{kv_s,s_s}$ \\
\r
232 $Decrypt(SK_s,sv_s)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\
\r
233 $GetSeqN(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=s$ \\
\r
234 $GetMacId(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=id$ \\
\r
235 $GetPrevHmac(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=hmac_p$ \\
\r
236 $GetCurrHmac(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=hmac_c$ \\
\r
237 $GetDatEnt(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=DE$ \\
\r
238 $GetLiveSS(SS_{live},ss_s)= ss$ \textit{such that} $ss \in SS_{live}
\r
239 \wedge \forall ss_s \in SS_{live}, ss = ss_s$ \\
\r
240 $GetLiveCR(CR_{live},cr_s)= cr$ \textit{such that} $cr \in CR_{live}
\r
241 \wedge \forall cr_s \in CR_{live}, cr = cr_s$ \\
\r
242 $GetLivEntLastS(LV_s,kv_s)= s$ \textit{such that} $\tuple{kv, s} \in LV_s
\r
243 \wedge \forall \tuple{kv_s, s_s} \in LV_s, kv_s = kv$ \\
\r
244 $GetKV($key-value data entry$)=\tuple{k_s,v_s} = kv_s$ \\
\r
245 $GetSS($slot-sequence data entry$)=\tuple{id_s,s_{s_{last}}} = ss_s$ \\
\r
246 $GetQS($queue-state data entry$)=qs_s$ \\
\r
247 $GetCR($collision-resolution data entry$)=\tuple{s_s,id_s} = cr_s$ \\
\r
248 $GetKey(kv = \tuple{k, v})=k$ \\
\r
249 $GetVal(kv = \tuple{k, v})=v$ \\
\r
250 $GetId(ss = \tuple{id, s_{last}})=id$ \\
\r
251 $GetSLast(ss = \tuple{id, s_{last}})=s_{last}$ \\
\r
252 $GetS(cr = \tuple{s, id})=s$ \\
\r
253 $GetId(cr = \tuple{s, id})=id$ \\
\r
254 $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v}
\r
255 \in DT_s \wedge \forall \tuple{k_s, v_s} \in DT_s, k = k_s$ \\
\r
256 $MaxLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
\r
257 \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \geq s_{s_{last}}$ \\
\r
258 $MinLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s
\r
259 \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \leq s_{s_{last}}$ \\
\r
260 $MinCRSeqN(CR_s)= s$ \textit{such that} $\tuple{s, id} \in CR_s
\r
261 \wedge \forall \tuple{s_s, id_s} \in CR_s, s \leq s_s$ \\
\r
262 $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s
\r
263 \wedge \forall \tuple{s_s, id_s} \in SM_s, s \geq s_s$ \\
\r
265 \begin{algorithmic}[1]
\r
266 \Procedure{Error}{$msg$}
\r
267 \State $Print(msg)$
\r
272 \begin{algorithmic}[1]
\r
273 \Function{GetQueSta}{$DE_s$}
\r
274 \State $de_{qs} \gets ss$ \textit{such that} $ss \in DE_s,
\r
275 de_s \in D \land type(de_s) = "qs"$
\r
276 \If{$de_{qs} \neq \emptyset$}
\r
277 \State $qs_{ret} \gets GetQS(de_{qs})$
\r
279 \State $qs_{ret} \gets \emptyset$
\r
281 \State \Return{$qs_{ret}$}
\r
285 \begin{algorithmic}[1]
\r
286 \Function{GetSlotSeq}{$DE_s$}
\r
287 \State $DE_{ss} \gets \{de | de \in DE_s \land type(de) = "ss"\}$
\r
288 \State \Return{$DE_{ss}$}
\r
292 \begin{algorithmic}[1]
\r
293 \Function{GetColRes}{$DE_s$}
\r
294 \State $DE_{cr} \gets \{de | de \in DE_s \land type(de) = "cr"\}$
\r
295 \State \Return{$DE_{cr}$}
\r
299 \begin{algorithmic}[1]
\r
300 \Function{UpdateLastSeqN}{$id_s,s_s,MS_s$}
\r
301 \State $s_t \gets MS_s[id_s]$
\r
302 \If{$s_t = \emptyset$}
\r
303 \State $MS_s[id_s] = s_s$ \Comment{First occurrence}
\r
305 \State $MS_S[id_s] \gets max(s_t, s_s)$
\r
307 \State \Return{$MS_s$}
\r
311 \begin{algorithmic}[1]
\r
312 \Function{UpdateKVLivEnt}{$LV_s,kv_s,s_s$}
\r
313 \State $s_t \gets GetLivEntLastS(LV_s,kv_s)$
\r
314 \If{$s_t = \emptyset$}
\r
315 \State $LV_s \gets LV_s \cup \{\tuple{kv_s,s_s}\}$\Comment{First occurrence}
\r
317 \If{$s_s > s_t$}\Comment{Update entry with a later s}
\r
318 \State $LV_s \gets (LV_s - \{\tuple{kv_s,s_t}\}) \cup
\r
319 \{\tuple{kv_s,s_s}\}$
\r
322 \State \Return{$LV_s$}
\r
326 \begin{algorithmic}[1]
\r
327 \Function{AddSSLivEnt}{$SS_{s_{live}},de_s$}
\r
328 \State $ss_s \gets GetSS(de_s)$
\r
329 \State $ss_t \gets GetLiveSS(SS_{s_{live}},ss_s)$
\r
330 \If{$ss_t = \emptyset$}
\r
331 \State $SS_{s_{live}} \gets SS_{s_{live}} \cup \{ss_s\}$\Comment{First occurrence}
\r
333 \State \Return{$SS_{s_{live}}$}
\r
337 \begin{algorithmic}[1]
\r
338 \Function{AddCRLivEnt}{$CR_{s_{live}},cr_s$}
\r
339 \State $cr_t \gets GetLiveCR(CR_{s_{live}},cr_s)$
\r
340 \If{$cr_t = \emptyset$}
\r
341 \State $CR_{s_{live}} \gets CR_{s_{live}} \cup \{cr_s\}$\Comment{First occurrence}
\r
343 \State \Return{$CR_{s_{live}}$}
\r
347 \begin{algorithmic}[1]
\r
348 \Function{UpdateSSLivEnt}{$SS_{s_{live}},MS_s$}
\r
349 \State $s_{s_{min}} \gets MinLastSeqN(MS_s)$
\r
350 \ForAll{$ss_s \in SS_{s_{live}}$}
\r
351 \State $s_{s_{last}} \gets GetSLast(ss_s)$
\r
352 \If{$s_{s_{min}} > s_{s_{last}}$}\Comment{Remove if dead}
\r
353 \State $SS_{s_{live}} \gets SS_{s_{live}} - \{ss_s\}$
\r
356 \State \Return{$SS_{s_{live}}$}
\r
360 \begin{algorithmic}[1]
\r
361 \Function{UpdateCRLivEnt}{$CR_{s_{live}},MS_s$}
\r
362 \State $s_{s_{min}} \gets MinLastSeqN(MS_s)$
\r
363 \ForAll{$cr_s \in CR_{s_{live}}$}
\r
364 \State $s_s \gets GetS(cr_s)$
\r
365 \If{$s_{s_{min}} > s_s$}\Comment{Remove if dead}
\r
366 \State $CR_{s_{live}} \gets CR_{s_{live}} - \{cr_s\}$
\r
369 \State \Return{$CR_{s_{live}}$}
\r
373 \begin{algorithmic}[1]
\r
374 \Function{UpdateSM}{$SM_s,CR_s$}\Comment{Remove if dead}
\r
375 \State $s_{cr_{min}} \gets MinCRSeqN(CR_s)$
\r
376 \State $SM_s \gets SM_s - \{\tuple{s_s,id_s} \mid \tuple{s_s,id_s}
\r
377 \in SM_s \wedge s_s < s_{cr_{min}}\}$
\r
378 \State \Return{$CR_{s_{live}}$}
\r
382 \begin{algorithmic}[1]
\r
383 \Procedure{CheckLastSeqN}{$MS_s,MS_t,d$}
\r
384 \For {$\tuple{id, s_t}$ in $MS_t$}\Comment{Check $MS_t$ based on the newer $MS_s$}
\r
385 \State $s_s \gets MS_s[id]$
\r
386 \If{$d \land s_s = \emptyset$}
\r
387 \State \Call{Error}{'Missing $s$ for machine $id$'}
\r
388 \ElsIf{$id = id_{self}$ and $s_s \neq s_t$}
\r
389 \State \Call{Error}{'Invalid last $s$ for this machine'}
\r
390 \ElsIf{$id \neq id_{self}$ and $s_{s_{last}} < s_{t_{last}}$}
\r
391 \State \Call{Error}{'Invalid last $s$ for machine $id$'}
\r
393 \State $MS_t[id] \gets s_s$
\r
399 \begin{algorithmic}[1]
\r
400 \Procedure{CheckCollision}{$MS_s,SM_s,cr_s$}
\r
401 \If{$cr_s \neq \emptyset$}
\r
402 \State $s_s \gets GetS(cr_s)$
\r
403 \State $id_s \gets GetId(cr_s)$
\r
404 \State $s_{s_{last}} \gets GetLastSeqN(MS_s,id_s)$
\r
405 \If{$s_{s_{last}} < s_s$}
\r
406 \State $id_t \gets SM_s[s_s]$
\r
407 \If{$id_s \neq id_t$}
\r
408 \State \Call{Error}{'Invalid $id$ for this slot update'}
\r
415 \begin{algorithmic}[1]
\r
416 \Function{ValidSlotsRange}{$|SL_s|,s_{s_{min}},s_{s_{max}}$}
\r
417 \State $sz_{SL} \gets s_{s_{max}} - s_{s_{min}} + 1$
\r
418 \If{$sz_{SL} \neq |SL_s|$}
\r
419 \State \Call{Error}{'Sequence numbers range does not match actual set'}
\r
421 \State $s_{s_{last}} \gets MaxSMSeqN(SM)$
\r
422 \If{$s_{s_{min}} \leq s_{s_{last}}$}
\r
423 \State \Call{Error}{'Server sent old slots'}
\r
425 \State \Return{$s_{s_{min}} > s_{s_{last}} + 1$}
\r
429 \begin{algorithmic}[1]
\r
430 \Procedure{CheckSlotsRange}{$|SL_s|$}
\r
431 \State $s_{s_{max}} \gets MaxLastSeqN(MS)$
\r
432 \State $s_{self} \gets MS[id_{self}]$
\r
433 \State $sz_{expected} \gets s_{s_{max}} - s_{self} + 1$
\r
434 \If{$|SL_s| \neq sz_{expected}$}
\r
435 \State \Call{Error}{'Actual number of slots does not match expected'}
\r
440 \begin{algorithmic}[1]
\r
441 \Function{StoreLastSlot}{$MS_s,sl_l,s_s,sv_s,id_s$}
\r
442 \State $s_{min} \gets MinLastSeqN(MS_s)$
\r
443 \If{$s_{min} \neq \emptyset \land s_{min} = s_s$}\Comment{$MS$ initially empty}
\r
444 \State $sl_l \gets CreateLastSL(s_s,sv_s,id_s)$
\r
446 \State \Return{$sl_l$}
\r
450 \begin{algorithmic}[1]
\r
451 \Function{UpdateDT}{$DT_s,DE_s,LV_s,s_s$}
\r
452 \State $DE_{s_{kv}} \gets \{de_s | de_s \in DE_s, type(de_s) = "kv"\}$
\r
453 \ForAll{$de_s \in DE_s$}
\r
454 \State $kv_s \gets GetKV(de_s)$
\r
455 \State $LV_s \gets \Call{UpdateKVLivEnt}{LV_s,kv_s,s_s}$
\r
456 \State $k_s \gets GetKey(kv_s)$
\r
457 \State $\tuple{k_s,v_t} \gets GetKeyVal(DT_s,k_s)$
\r
458 \If{$\tuple{k_s,v_t} = \emptyset$}
\r
459 \State $DT_s \gets DT_s \cup \{\tuple{k_s,v_s}\}$
\r
461 \State $DT_s \gets (DT_s - \{\tuple{k_s,v_t}\}) \cup
\r
462 \{\tuple{k_s,v_s}\}$
\r
465 \State \Return{$DT_s$}
\r
469 \begin{algorithmic}[1]
\r
470 \Procedure{ProcessSL}{$SL_g$}
\r
471 \State $MS_g \gets \emptyset$
\r
472 \State $\tuple{s_{g_{min}},sv_{g_{min}}} \gets MinSlot(SL_g)$
\r
473 \State $\tuple{s_{g_{max}},sv_{g_{max}}} \gets MaxSlot(SL_g)$
\r
474 \State $d \gets \Call{ValidSlotsRange}{|SL_g|,s_{g_{min}},s_{g_{max}}}$
\r
475 \For{$s_g \gets s_{g_{min}}$ \textbf{to} $s_{g_{max}}$}\Comment{Process slots
\r
476 in $SL_g$ in order}
\r
477 \State $\tuple{s_g,sv_g} \gets Slot(SL_g,s_g)$
\r
478 \State $Dat_g \gets Decrypt(SK,sv_g)$
\r
479 \State $id_g \gets GetMacId(Dat_g)$
\r
480 \State $SM \gets SM \cup \{\tuple{s_g,id_g}\}$
\r
481 \State $s_{g_{in}} \gets GetSeqN(Dat_g)$
\r
482 \If{$s_g \neq s_{g_{in}}$}
\r
483 \State \Call{Error}{'Invalid sequence number'}
\r
485 \State $DE_g \gets GetDatEnt(Dat_g)$
\r
486 \State $hmac_{p_{stored}} \gets GetPrevHmac(Dat_g)$
\r
487 \If {$ \neg(s_g = 0 \land hmac_{p_g} = 0) \land hmac_{p_{stored}} \neq hmac_{p_g}$}
\r
488 \State \Call{Error}{'Invalid previous HMAC value'}
\r
490 \If{$\Call{Hmac}{DE_g,SK} \neq GetCurrHmac(Dat_g)$ }
\r
491 \State \Call{Error}{'Invalid current HMAC value'}
\r
493 \State $hmac_{p_g} \gets Hmac(DE_g,SK)$\Comment{Update $hmac_{p_g}$ for next check}
\r
494 \State $qs_g \gets \Call{GetQueSta}{DE_g}$\Comment{Handle qs}
\r
495 \If{$qs_g \neq \emptyset \land qs_g > max_g$}
\r
496 \State $max_g \gets qs_g$
\r
498 %Check for last s in Dat
\r
499 \State $id_g \gets GetMacId(Dat_g)$\Comment{Handle last s}
\r
500 \State $MS_g \gets \Call{UpdateLastSeqN}{id_g,s_g,MS_g}$
\r
501 %Check for last s in DE in Dat
\r
502 \State $DE_{g_{ss}} \gets \Call{GetSlotSeq}{DE_g}$\Comment{Handle ss}
\r
503 \If{$DE_{g_{ss}} \neq \emptyset$}
\r
504 \ForAll{$de_{g_{ss}} \in DE_{g_{ss}}$}
\r
505 \State $\tuple{id_d,s_{d_{last}}} \gets GetSS(de_{g_{ss}})$
\r
506 \State $MS_g \gets \Call{UpdateLastSeqN}{id_d,s_{d_{last}},MS_g}$
\r
507 \State $SS_{live} \gets \Call{AddSSLivEnt}{SS_{live},de_{g_{ss}}}$
\r
510 \State $DE_{g_{cr}} \gets \Call{GetColRes}{DE_g}$\Comment{Handle cr}
\r
511 \If{$DE_{g_{cr}} \neq \emptyset$}
\r
512 \ForAll{$de_{g_{cr}} \in DE_{g_{cr}}$}
\r
513 \State $cr_g \gets GetCR(de_{g_{cr}})$
\r
514 \State $\Call{CheckCollision}{MS,SM,cr_g}$
\r
515 \State $CR_{live} \gets \Call{AddCRLivEnt}{CR_{live},cr_g}$
\r
518 \State $sl_{last} \gets \Call{StoreLastSlot}{MS,sl_{last},s_g,sv_g,id_g}$
\r
519 \State $DT \gets \Call{UpdateDT}{DT,DE_g,LV,s_g}$
\r
521 \If{$m + |SL_g| \leq max_g$}\Comment{Check actual size against $max_g$}
\r
522 \State $m \gets m + |SL_g|$
\r
524 \State \Call{Error}{'Actual $SL$ size on server exceeds $max_g$'}
\r
526 \State $\Call{CheckLastSeqN}{MS_g,MS,d}$
\r
527 \State $\Call{CheckSlotsRange}{|SL_g|}$
\r
528 \State $\Call{UpdateSSLivEnt}{SS_{live},MS}$
\r
529 \State $\Call{UpdateCRLivEnt}{CR_{live},MS}$
\r
530 \State $\Call{UpdateSM}{SM,CR_{live}}$
\r
534 \begin{algorithmic}[1]
\r
535 \Procedure{GetKVPairs}{}
\r
536 \State $s_g \gets GetLastSeqN(MS,id_{self}) + 1$
\r
537 \State $SL_c \gets \Call{GetSlot}{s_g}$
\r
538 \State $\Call{ProcessSL}{SL_c}$\Comment{Process slots and update DT}
\r
542 \begin{algorithmic}[1]
\r
543 \Function{Get}{$k_g$} \Comment{Interface function to get a value}
\r
544 \State $\tuple{k_s,v_s} \gets \tuple{k,v}$ \textit{such that} $\tuple{k,v}
\r
545 \in DT \land k = k_g$
\r
546 \State \Return{$v_s$}
\r
550 \subsubsection{Writing Slots}
\r
552 \textit{$cp$ = data entry $DE$ maximum size/capacity} \\
\r
553 \textit{$ck_p$ = counter of $kv \in KV$ for putting pairs (initially 0)} \\
\r
554 \textit{$ck_g$ = counter of $kv \in KV$ for getting pairs (initially 0)} \\
\r
555 \textit{$cs_p$ = counter of $ss \in SS$ for putting pairs (initially 0)} \\
\r
556 \textit{$cs_g$ = counter of $ss \in SS$ for getting pairs (initially 0)} \\
\r
557 \textit{$cc_p$ = counter of $cr \in CR$ for putting pairs (initially 0)} \\
\r
558 \textit{$cc_g$ = counter of $cr \in CR$ for getting pairs (initially 0)} \\
\r
559 \textit{$hmac_{c_p}$ = the HMAC value of the current slot} \\
\r
560 \textit{$hmac_{p_p}$ = the HMAC value of the previous slot
\r
561 ($hmac_{p_p} = \emptyset$ for the first slot)} \\
\r
562 \textit{$id_{self}$ = machine Id of this client} \\
\r
563 \textit{$sl_{last}$ = info of last slot in queue =
\r
564 $\tuple{s_{last},sv_{last},id_{last}}$ (initially $\emptyset$)} \\
\r
565 \textit{$th_p$ = threshold number of dead slots for a resize to happen} \\
\r
566 \textit{$m'_p$ = offset added to $max$ for resize} \\
\r
567 \textit{$reinsert_{qs}$ = boolean to decide $qs$($max_g$) reinsertion} \\
\r
568 \textit{$KV$ = set of $\tuple{ck, \tuple{k,v}}$ of kv entries on client} \\
\r
569 \textit{$SS$ = set of $\tuple{cs, \tuple{id,s_{last}}}$ of ss entries on client} \\
\r
570 \textit{$CR$ = set of $\tuple{cc, \tuple{s_{col},id_{col}}}$ of cr entries on client} \\
\r
571 \textit{$SL_p$ = set of returned slots on client} \\
\r
572 \textit{SK = Secret Key} \\ \\
\r
573 \textbf{Helper Functions} \\
\r
574 $CreateDat(s,id,hmac_p,DE,hmac_c)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\
\r
575 $CreateSS(id_s,s_{s_{last}})=\tuple{id_s,s_{s_{last}}} = ss_s$ \\
\r
576 $CreateQS(max'_s)=qs_s$ \\
\r
577 $CreateCR(s_s,id_s)=\tuple{s_s,id_s} = cr_s$ \\
\r
578 $Encrypt(Dat_s,SK_s)=sv_s$ \\
\r
579 $GetLastS(sl = \tuple{s,sv,id})=s$ \\
\r
580 $GetSV(sl = \tuple{s,sv,id})=sv$ \\
\r
581 $GetID(sl = \tuple{s,sv,id})=id$ \\
\r
582 $GetColSeqN(SL_s,s_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}
\r
583 \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s = s_s$ \\
\r
584 $GetKVPair(KV_s,k_s)= \tuple{ck,\tuple{k, v}}$ \textit{such that}
\r
585 $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
\r
586 \forall \tuple{ck_s,\tuple{k_s, v_s}} \in KV_s, k = k_s$ \\
\r
588 \begin{algorithmic}[1]
\r
589 \Function{Put}{$KV_s,\tuple{k_s,v_s}$} \Comment{Interface function to update a key-value pair}
\r
590 \State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKVPair(KV_s,k_s)$
\r
591 \If{$\tuple{ck_s,\tuple{k_s,v_t}} = \emptyset$}
\r
592 \State $KV_s \gets KV_s \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$
\r
593 \State $ck_p \gets ck_p + 1$
\r
595 \State $KV_s \gets (KV_s - \{\tuple{ck_s, \tuple{k_s,v_t}}\}) \cup
\r
596 \{\tuple{ck_s, \tuple{k_s,v_s}}\}$
\r
598 \State \Return{$KV_s$}
\r
602 \begin{algorithmic}[1]
\r
603 \Function{PutSSPair}{$SS_s,\tuple{id_s,s_{s_{last}}}$}\Comment{Insert a set of $ss$ entries}
\r
604 \State $SS_s \gets SS_s \cup \{\tuple{cs_p, \tuple{id_s,s_{s_{last}}}}\}$
\r
605 \State $cs_p \gets cs_p + 1$
\r
606 \State \Return{$SS_s$}
\r
610 \begin{algorithmic}[1]
\r
611 \Function{PutCRPair}{$CR_s,\tuple{s_s,id_s}$}\Comment{Insert a set of $cr$ entries}
\r
612 \State $CR_s \gets CR_s \cup \{\tuple{cc_p, \tuple{s_s,id_s}}\}$
\r
613 \State $cc_p \gets cc_p + 1$
\r
614 \State \Return{$CR_s$}
\r
618 \begin{algorithmic}[1]
\r
619 \Function{CheckResize}{$MS_s,th_s,max_t,m'_s$}
\r
620 \State $s_{last_{min}} \gets MinLastSeqN(MS_s)$
\r
621 \State $s_{last_{max}} \gets MaxLastSeqN(MS_s)$
\r
622 \State $n_{live} \gets s_{last_{max}} - s_{last_{min}} + 1$\Comment{Number of live slots}
\r
623 \State $n_{dead} \gets max_t - n_{live}$
\r
624 \If{$n_{dead} \leq th_s$}
\r
625 \State $max'_s \gets max_t + m'_s$
\r
627 \State $max'_s \gets \emptyset$
\r
629 \State \Return{$max'_s$}
\r
633 \begin{algorithmic}[1]
\r
634 \Function{CheckSLFull}{$MS_s,max_t$}\Comment{Check if $ss$ is needed}
\r
635 \State $s_{last_{min}} \gets MinLastSeqN(MS_s)$
\r
636 \State $s_{last_{max}} \gets MaxLastSeqN(MS_s)$
\r
637 \State $n_{live} \gets s_{last_{max}} - s_{last_{min}}$\Comment{Number of live slots}
\r
638 \State $n_{dead} \gets max_t - n_{live}$
\r
639 \State \Return {$n_{dead} = 0$}
\r
643 \begin{algorithmic}[1]
\r
644 \Function{HandleCollision}{$SL_s,s_s$}
\r
645 \If{$SL_s = \emptyset$}
\r
646 \State \Call{Error}{'No slots received from server'}
\r
648 \State $\tuple{s_{col},sv_{col}} \gets GetColSeqN(SL_s,s_s)$
\r
649 \State $Dat_{col} \gets Decrypt(SK,sv_{col})$
\r
650 \State $id_{col} \gets GetMacId(Dat_{col})$
\r
651 \State $cr_s \gets CreateCR(s_{col},id_{col})$
\r
652 \State $\Call{ProcessSL}{SL_s}$
\r
653 \State \Return{$cr_s$}
\r
657 \begin{algorithmic}[1]
\r
658 \Procedure{CheckLastSlot}{$sl_{s_{last}}$}
\r
659 \State $s_s \gets GetLastS(sl_{s_{last}})$
\r
660 \State $sv_s \gets GetSV(sl_{s_{last}})$
\r
661 \State $Dat_s \gets Decrypt(SK,sv_s)$
\r
662 \State $DE_s \gets GetDatEnt(Dat_s)$
\r
663 \ForAll{$de_s \in DE_s$}
\r
664 \State $live \gets \Call{CheckLiveness}{s_s,de_s}$
\r
667 \State $\tuple{k_s,v_s} \gets GetKV(de_s)$
\r
668 \State $KV \gets \Call{PutKVPair}{KV,\tuple{k_s,v_s}}$
\r
669 \ElsIf{$de_s = ss$}
\r
670 \State $\tuple{id_s,s_{s_{last}}} \gets GetSS(de_s)$
\r
671 \State $SS \gets \Call{PutSSPair}{SS,\tuple{id_s,s_{s_{last}}}}$
\r
672 \ElsIf{$de_s = cr$}
\r
673 \State $\tuple{s_s,id_s} \gets GetCR(de_s)$
\r
674 \State $CR \gets \Call{PutCRPair}{CR,\tuple{s_s,id_s}}$
\r
675 \ElsIf{$de_s = qs$}
\r
676 \State $reinsert_{qs} \gets true$
\r
683 \begin{algorithmic}[1]
\r
684 \Function{CheckLiveness}{$s_s,de_s$}
\r
685 \State $live \gets true$
\r
687 \State $s_l \gets GetLivEntLastS(LV,de_s)$
\r
688 \If{$s_l = \emptyset \lor s_s < s_l$}
\r
689 \State $live \gets false$
\r
691 \ElsIf{$de_s = ss$}
\r
692 \State $ss_s \gets GetSS(de_s)$
\r
693 \State $ss_l \gets GetLiveSS(SS_{live},ss_s)$
\r
694 \If{$ss_l = \emptyset$}
\r
695 \State $live \gets false$
\r
697 \ElsIf{$de_s = cr$}
\r
698 \State $cr_s \gets GetCR(de_s)$
\r
699 \State $cr_l \gets GetLiveCR(CR_{live},cr_s)$
\r
700 \If{$cr_l = \emptyset$}
\r
701 \State $live \gets false$
\r
703 \ElsIf{$de_s = qs$}
\r
704 \State $qs_s \gets GetQS(de_s)$
\r
705 \If{$qs_s \neq max_g$}
\r
706 \State $live \gets false$
\r
709 \State \Call{Error}{'Unrecognized $de$ type'}
\r
711 \State \Return{$live$}
\r
715 \begin{algorithmic}[1]
\r
716 \Function{CreateSlotSeq}{$sl_s$}
\r
717 \State $id_s \gets GetID(sl_s)$
\r
718 \State $s_{s_{last}} \gets GetLastS(sl_s)$
\r
719 \State $ss_s \gets CreateSS(id_s,s_{s_{last}})$
\r
720 \State \Return{$\tuple{ss_s}$}
\r
724 \begin{algorithmic}[1]
\r
725 \Function{AddQueSta}{$DE_s,max'_s,cp_s$}\Comment{Insert a $qs$}
\r
726 \State $DE_{ret} \gets \emptyset$
\r
727 \State $qs_s \gets max'_s$
\r
728 \State $DE_{ret} \gets DE_s \cup \{qs_s\}$
\r
729 \State $cp_s \gets cp_s - 1$
\r
730 \State \Return{$\tuple{DE_{ret},cp_s}$}
\r
734 \begin{algorithmic}[1]
\r
735 \Function{GetKVPairs}{$DE_s,KV_s,cp_s$}
\r
736 \State $DE_{ret} \gets \emptyset$
\r
737 \If{$|KV_s| \leq cp_s$}\Comment{$KV$ set can span multiple slots}
\r
738 \State $DE_{ret} \gets DE_s \cup
\r
739 \{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s\}$
\r
741 \State $DE_{ret} \gets DE_s \cup
\r
742 \{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s,
\r
743 ck_g \leq ck_s < ck_g + cp_s\}$
\r
745 \State \Return{$\tuple{DE_{ret}}$}
\r
749 \begin{algorithmic}[1]
\r
750 \Function{GetSSPairs}{$DE_s,SS_s,cp_s$}
\r
751 \State $DE_{ret} \gets \emptyset$
\r
752 \If{$|SS_s| \leq cp_s$}\Comment{$SS$ set can span multiple slots}
\r
753 \State $DE_{ret} \gets DE_s \cup
\r
754 \{\tuple{id_s,s_{s_{last}}} \mid \tuple{cs_s,\tuple{id_s,s_{s_{last}}}} \in SS_s\}$
\r
755 \State $cp_s \gets cp_s - |SS_s|$
\r
757 \State $DE_{ret} \gets DE_s \cup
\r
758 \{\tuple{id_s,s_{s_{last}}} \mid \tuple{cs_s,\tuple{id_s,s_{s_{last}}}} \in SS_s,
\r
759 cs_g \leq cs_s < cs_g + cp_s\}$
\r
760 \State $cp_s \gets 0$
\r
762 \State \Return{$\tuple{DE_{ret},cp_s}$}
\r
766 \begin{algorithmic}[1]
\r
767 \Function{GetCRPairs}{$DE_s,CR_s,cp_s$}
\r
768 \State $DE_{ret} \gets \emptyset$
\r
769 \If{$|CR_s| \leq cp_s$}\Comment{$CR$ set can span multiple slots}
\r
770 \State $DE_{ret} \gets DE_s \cup
\r
771 \{\tuple{s_s,id_s} \mid \tuple{cc_s,\tuple{s_s,id_s}} \in CR_s\}$
\r
772 \State $cp_s \gets cp_s - |CR_s|$
\r
774 \State $DE_{ret} \gets DE_s \cup
\r
775 \{\tuple{s_s,id_s} \mid \tuple{cc_s,\tuple{s_s,id_s}} \in CR_s,
\r
776 cc_g \leq cc_s < cc_g + cp_s\}$
\r
777 \State $cp_s \gets 0$
\r
779 \State \Return{$\tuple{DE_{ret},cp_s}$}
\r
783 \begin{algorithmic}[1]
\r
784 \Procedure{PutDataEntries}{$th_p,m'_p$}
\r
785 \State $success_p \gets false$
\r
786 \State $CR_p \gets \emptyset$
\r
787 \While{$\neg success_p$}
\r
788 \State $DE_p \gets \emptyset$
\r
789 \State $s_p \gets MaxLastSeqN(MS)$
\r
790 \State $cp_p \gets cp$
\r
791 \State $max'_p \gets \Call{CheckResize}{MS,th_p,max_g,m'_p}$
\r
792 \If{$max'_p \neq \emptyset$}\Comment{Add a qs entry}
\r
793 \State $\tuple{DE_p,cp_p} \gets \Call{AddQueSta}{DE_p,max'_p,cp_p}$
\r
794 \State $reinsert_{qs} \gets false$
\r
795 \Else\Comment{Check if there is $qs$ reinsertion}
\r
796 \If{$reinsert_{qs}$}
\r
797 \State $\tuple{DE_p,cp_p} \gets \Call{AddQueSta}{DE_p,max_g,cp_p}$
\r
798 \State $reinsert_{qs} \gets false$
\r
801 \If{$SS \neq \emptyset$}\Comment{Add $ss$ entries}
\r
802 \State $\tuple{DE_p,cp_p} \gets \Call{GetSSPairs}{DE_p,SS,cp_p}$
\r
804 \If{$CR \neq \emptyset$}\Comment{Add $cr$ entries}
\r
805 \State $\tuple{DE_p,cp_p} \gets \Call{GetCRPairs}{DE_p,CR,cp_p}$
\r
807 \State $\tuple{DE_p,cp_p} \gets \Call{GetKVPairs}{DE_p,KV,cp_p}$\Comment{Add $kv$ entries}
\r
808 \State $hmac_{c_p} \gets Hmac(DE_p,SK)$
\r
809 \State $Dat_p \gets CreateDat(s_p,id_{self},hmac_{p_p},DE_p,hmac_{c_p})$
\r
810 \State $hmac_{p_p} \gets hmac_{c_p}$
\r
811 \State $sv_p \gets Encrypt(Dat_p,SK)$
\r
812 \State $\tuple{success_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$
\r
813 \If{$\neg success_p$}
\r
814 \State $cr_p \gets \Call{HandleCollision}{SL_p,s_p}$
\r
815 \State $\tuple{s_{p_{col}},id_{p_{col}}} \gets GetCR(cr_p)$
\r
816 \State $CR \gets \Call{PutCRPair}{CR,\tuple{s_{p_{col}},id_{p_{col}}}}$
\r
819 \State $MS \gets \Call{UpdateLastSeqN}{id_{self},s_p,MS}$
\r
820 \If{$|DE_p| = cp$}\Comment{Update set counters}
\r
821 \State $ck_g \gets ck_g + cp_p$\Comment{Middle of set}
\r
822 \State $cs_g \gets cs_g + |SS|$
\r
823 \State $cc_g \gets cc_g + |CR|$
\r
824 \Else\Comment{End of set}
\r
825 \State $ck_g \gets 0$
\r
826 \State $cs_g \gets 0$
\r
827 \State $cc_g \gets 0$
\r
829 \State $need_p \gets \Call{CheckSLFull}{MS,max_g}$
\r
830 \If{$need_p$}\Comment{SL on server is full}
\r
831 \State $\Call{CheckLastSlot}{sl_{last}}$\Comment{Salvage entries from expunged slot}
\r
832 \State $ss_p \gets \Call{CreateSlotSeq}{sl_{last}}$
\r
833 \State $\tuple{id_p,s_{p_{last}}} \gets GetSS(ss_p)$
\r
834 \State $SS \gets \Call{PutSSPair}{SS,\tuple{id_p,s_{p_{last}}}}$\Comment{Add ss}
\r
839 %\note{Lots of problems with PutDataEntries: (1) What happens if lose network connectivity after adding the key value pair, but before reinserting the last slot? You probably need to create space first and then insert your data entry... (2) What if reinsertlastslot kicks something else important out? What if the server rejects our update because it is out of date? At the very least, any putdataentries function w/o a loop is wrong!}
\r
841 %\note{General comments... Work on structuring things to improve readability... This include names of functions/variables, how things are partitioned into functions, adding useful comments,...}
\r
843 %\note{Also Missing liveness state definition in algorithm...}
\r
846 \subsection{Formal Guarantees}
\r
847 \subsubsection{Definitions}
\r
849 \begin{defn}[Message]
\r
850 A message $\mathsf{t}$, is the tuple
\r
852 $\mathsf{t = \tuple{s, E(Dat_s)}}$ \\
\r
853 $\mathsf{Dat_t = \tuple{s,id,hmac_p, DE,hmac_c}}$
\r
855 containing $\mathsf{s}$ as sequence number and $\mathsf{Dat_t}$ as its
\r
856 encrypted contents. $\mathsf{Dat_t}$ consists of $\mathsf{s}$,
\r
857 $\mathsf{id}$ as machine ID of the sender, $\mathsf{hmac_p}$ as HMAC
\r
858 from a previous message, $\mathsf{DE}$ as set of data entries, and
\r
859 $\mathsf{hmac_c}$ as HMAC from message $\mathsf{t}$ respectively.
\r
862 \begin{defn}[Equality]
\r
863 Two messages $\mathsf{t}$ and $\mathsf{u}$ are equal if their $\mathsf{s}$,
\r
864 and $\mathsf{Dat_t}$ are exactly the same.
\r
867 \begin{defn}[Parent]
\r
868 A parent of a message $\mathsf{t}$ is the message $\mathsf{p_t}$,
\r
869 unique by the correctness of HMACs in $\mathsf{Dat_t}$, such that
\r
870 $\mathsf{hmac_p(t) = hmac_c(p_t)}$.
\r
873 \begin{defn}[Chain]
\r
874 A chain of messages with length $\mathsf{n \ge 1}$ is a message sequence
\r
875 $\mathsf{R = (r_s, r_{s+1}, ..., r_{s+n-1})}$ such that for every sequence
\r
876 number $\mathsf{s < k \le s+n-1}$, $\mathsf{r_k}$ has sequence number
\r
877 $\mathsf{k}$ and is the parent of $\mathsf{r_{k-1}}$.
\r
880 \begin{defn}[Partial sequence]
\r
881 A partial sequence $\mathsf{P}$ is a sequence of messages, no two
\r
882 with the same sequence number, that can be divided into disjoint chains.
\r
885 \begin{defn}[Total sequence]
\r
886 A total sequence $\mathsf{T =}$ $\mathsf{(t_1, t_2, ..., t_n)}$ with
\r
887 length $\mathsf{n}$ is a chain of messages that starts at $\mathsf{s = 1}$.
\r
891 The path of a message $\mathsf{t}$ is the chain that starts at $\mathsf{s = 1}$
\r
892 and whose last message is $\mathsf{t}$. The uniqueness of a path follows
\r
893 from the uniqueness of a parent.
\r
896 \begin{defn}[Consistency]
\r
897 A partial sequence $\mathsf{P}$ is consistent with a total sequence
\r
898 $\mathsf{T}$ of length $\mathsf{n}$ if for every message $\mathsf{p \in P}$
\r
899 with $\mathsf{s_p \leq n}$, $\mathsf{t_{s_p} = p}$. This implies that
\r
900 $\mathsf{\{p \in P | s_p \le n\}}$ is a partial sequence of $\mathsf{T}$.
\r
903 \begin{defn}[Transitive closure]
\r
904 Transitive closure set at sequence number $\mathsf{s_n}$ is a set
\r
905 $\mathsf{\mathscr{S}}$ of clients comprising a connected component of an
\r
906 undirected graph, where two clients are connected by an edge if they both
\r
907 received the same message $\mathsf{t}$ with sequence number $\mathsf{s_t > s_n}$.
\r
910 \subsubsection{Lemmas and Proofs}
\r
913 \label{prop:parentmessage}
\r
914 Every client $\mathsf{J}$ who sends a message $\mathsf{t}$
\r
915 has parent $\mathsf{p_t}$ as its latest stored message, and
\r
916 $\mathsf{s_t = s_{p_t} + 1}$.
\r
918 \begin{proof} True by definition, because $J$ sets
\r
919 $\mathsf{hmac_p(t) = hmac_c(p_t)}$ and
\r
920 $\mathsf{s_t = }$ $\mathsf{s_{p_t + 1}}$ when a message
\r
925 \label{prop:rejectedmessage}
\r
926 If a rejected message entry is added to the set $\mathsf{CR}$
\r
927 at sequence number $\mathsf{s}$, the message will remain in $\mathsf{CR}$
\r
928 until every client has seen it.
\r
930 \begin{proof} Every $\mathsf{CR}$ entry $\mathsf{cr}$ remains in the queue until it
\r
931 reaches the tail, and is refreshed by the next sender $\mathsf{J}$ at that time if
\r
932 $\mathsf{min(MS) > s_{cr}}$; that is, until every client has sent a message with
\r
933 sequence number greater than $\mathsf{s_{cr}}$. Because every client who sends a
\r
934 message with sequence number $\mathsf{s}$ has the state of the set $\mathsf{SL}$ at
\r
935 $\mathsf{s - 1}$, this client will have seen the message at $\mathsf{s_{cr}}$.
\r
940 \xymatrix{ & & L \\
\r
941 \dots \ar[r] & q \ar[dr]_{J} \ar[r]^{K} & l_1 \ar[r] & l_2 \ar[r] & \dots \ar[r] & m \ar[r] & \dots \ar[r] & l_n = u \\
\r
942 & & r_1 \ar[r] & r_2 \ar[r] & \dots \ar[r] & r_m = t \\
\r
944 \save "2,3"."2,8"*+\frm{^\}}
\r
945 \save "3,3"."3,6"*+\frm{_\}}
\r
949 \caption{By \textbf{Lemma \ref{lem:twomessages}}, receiving both $t$ and $u$ here is impossible.}
\r
953 \label{lem:twomessages}
\r
954 Two messages are received without errors by a client $\mathsf{C}$;
\r
955 call them $\mathsf{t}$ and $\mathsf{u}$ such that $\mathsf{s_t \le s_u}$.
\r
956 Then $\mathsf{t}$ is in the path of $\mathsf{u}$.
\r
959 Assume that there are some pairs of messages $\mathsf{(t,u)}$ that violate this lemma.
\r
960 Take a specific $\mathsf{(t,u)}$ such that $\mathsf{s_u}$ is minimized, and
\r
961 $\mathsf{s_t}$ is maximized for this choice of $\mathsf{s_u}$. We will show that $\mathsf{C}$
\r
962 cannot receive both $\mathsf{t}$ and $\mathsf{u}$ without throwing an error.
\r
964 Clearly $\mathsf{C}$ will throw an error if $\mathsf{s_t = s_u}$. So
\r
965 $\mathsf{s_t < s_u}$. Additionally, if $\mathsf{C}$ receives $\mathsf{u}$ before
\r
966 $\mathsf{t}$, this will cause it to throw an error, so $\mathsf{t}$ is received
\r
967 before $\mathsf{u}$. We will prove that an error occurs upon receipt of $\mathsf{u}$.
\r
969 Let $\mathsf{r_1}$ be the earliest member of the path of $\mathsf{t}$ that is
\r
970 not in the path of $\mathsf{u}$, and $\mathsf{q}$ be its parent. Message
\r
971 $\mathsf{q}$, the last common ancestor of $\mathsf{t}$ and $\mathsf{u}$, must exist,
\r
972 since all clients and the server were initialized with the same state. Let
\r
973 $\mathsf{l_1}$ be the successor of $\mathsf{q}$ that is in the path of $\mathsf{u}$;
\r
974 we know $\mathsf{l_1 \neq r_1}$. Let $\mathsf{R = (r_1, r_2, \dots, r_{|R|} = t)}$ be
\r
975 the distinct portion of the path of $\mathsf{t}$, and similarly let $\mathsf{L}$
\r
976 be the distinct portion of the path of $\mathsf{l_{|L|} = u}$.
\r
978 Let $\mathsf{J}$ be the client who sent $\mathsf{r_1}$; that is, such that
\r
979 $\mathsf{{id_{self}}_J = GetMacID(r_1)}$, and $\mathsf{K}$ be the client who
\r
980 sent $\mathsf{l_1}$. Because no client can send two messages with the same sequence number, and
\r
981 $\mathsf{s_{r_1} = s_{l_1} = s_q + 1}$, $\mathsf{J \neq K}$.
\r
983 We also know the following facts:
\r
986 \label{prop:bothmessages}
\r
987 No client sends both a message in $\mathsf{(r_2,...,t)}$ and a message in $\mathsf{(l_2,...,u)}$.
\r
991 To send a message $\mathsf{p}$ that is the parent of some other
\r
992 message, one must have received the parent of $\mathsf{p}$. Since
\r
993 $\mathsf{u}$ is the message with smallest sequence number received by any
\r
994 client that violates Lemma \ref{lem:twomessages}, no client receives both a message
\r
995 in $\mathsf{r}$ and a message in $\mathsf{l}$.
\r
999 \label{prop:seqnumb}
\r
1000 $\mathsf{C}$ does not receive any message with a
\r
1001 sequence number strictly between $\mathsf{s_t}$ and $\mathsf{s_u}$.
\r
1004 \begin{proof} If there were such a message with sequence number smaller than
\r
1005 $\mathsf{s_u}$, it would contradict the assumption that $\mathsf{u}$ is the
\r
1006 message with the least sequence number that violates Lemma \ref{lem:twomessages}.
\r
1009 There are two cases:
\r
1011 \item Case 1: $\mathsf{J}$ did not send a message in $\mathsf{L}$. Then, where $\mathsf{s_{t_J}}$
\r
1012 is the greatest sequence number of the messages that client $\mathsf{J}$ sent in
\r
1013 the path of message $\mathsf{t}$, $\mathsf{s_{t_J} > s_{q_J} = s_{u_J}}$.
\r
1015 \item Case 1.1: $\mathsf{C}$ never updates its slot sequence list $\mathsf{SS}$
\r
1016 between receiving $\mathsf{t}$ and receiving $\mathsf{u}$; this can only happen if
\r
1017 $\mathsf{s_t = s_u - 1}$. Since $\mathsf{t}$ is not the parent of $\mathsf{u}$,
\r
1018 $\mathsf{hmac_p(u) \neq hmac_c(t)}$, causing $\mathsf{C}$ to throw an error.
\r
1019 \item Case 1.2: Case 1.1 does not occur; therefore, $\mathsf{C}$ must update
\r
1020 its slot sequence list $\mathsf{SS}$ at some point between receiving $\mathsf{t}$
\r
1021 and $\mathsf{u}$.
\r
1022 The latest sequence number of $\mathsf{J}$ decreases during this time, which
\r
1023 means it must decrease when some message is received, which means $\mathsf{C}$
\r
1024 throws an error in the $\mathsf{CheckLastSeqN()}$ subroutine.
\r
1027 \item Case 2: $\mathsf{J}$ sent at least one message in $\mathsf{L}$. Call the
\r
1028 first one $\mathsf{m}$. We know that $\mathsf{s_m > s_{r_1}}$, since
\r
1029 $\mathsf{J \neq K}$ and $\mathsf{m \neq l_1}$. Message $\mathsf{r_1}$ must be sent
\r
1030 either before or after $\mathsf{m}$.
\r
1032 \item Case 2.1: Client $\mathsf{J}$ sends $\mathsf{m}$, and then $\mathsf{r_1}$.
\r
1033 Before sending $\mathsf{m}$, the greatest sequence number of a message that
\r
1034 $\mathsf{J}$ has received, $\mathsf{{s_{last}}_J}$, must be equal to
\r
1035 $\mathsf{s_m - 1 \ge s_{r_1}}$. Since $\mathsf{{s_{last}}_J}$ never decreases,
\r
1036 client $\mathsf{J}$ cannot then send a message with sequence number
\r
1037 $\mathsf{s_{r_1}}$, a contradiction.
\r
1038 \item Case 2.2: Client $\mathsf{J}$ sends $\mathsf{r_1}$, and then $\mathsf{m}$.
\r
1039 Let $\mathsf{X = (r_1 = x_1, \dots , x_n)}$ be the list of messages $\mathsf{J}$ sends
\r
1040 starting before $\mathsf{r_1}$ and ending before $m$; clearly these all have sequence
\r
1041 number $\mathsf{s_p = s_q + 1}$.
\r
1043 \item Case 2.2.1: Some message in $\mathsf{X}$ was accepted. Before sending $\mathsf{m}$,
\r
1044 $\mathsf{J}$'s value in $\mathsf{MS_J}$ for its own latest sequence number would
\r
1045 be strictly greater than $\mathsf{s_{q_J}}$. If there is a sequence of messages with
\r
1046 contiguous sequence numbers that $\mathsf{J}$ receives between $\mathsf{r_1}$ and
\r
1047 $\mathsf{m}$, $\mathsf{J}$ throws an error for a similar reason as Case 1.1. Otherwise,
\r
1048 when preparing to send $\mathsf{m}$, $\mathsf{J}$ would have received an update of its
\r
1049 own latest sequence number as at most $\mathsf{s_{q_J}}$. $J$ throws an error before
\r
1050 sending $\mathsf{p}$, because its own latest sequence number decreases.
\r
1051 \item Case 2.2.2: All messages in $\mathsf{X}$ were rejected, making $\mathsf{m}$
\r
1052 the first message of $\mathsf{J}$ that is accepted after $\mathsf{r_1}$.
\r
1054 We will show that $\mathsf{C}$ sees $\mathsf{r_1}$. Assume not. Then $\mathsf{(r_2, ..., u)}$
\r
1055 must have at least $\mathsf{{max_g}_C} \geq 2$ messages for $\mathsf{r_1}$ to fall off the
\r
1056 end of the queue. Consider the sender of $\mathsf{r_3}$ and call it $\mathsf{H}$.
\r
1057 $\mathsf{H \neq J}$ by Proposition \ref{prop:bothmessages} and the existence of $\mathsf{m}$.
\r
1058 Since $\mathsf{H \neq J}$, then by Proposition \ref{prop:bothmessages} it could not also
\r
1059 have sent a message in $\mathsf{(l_2,..., u)}$. Therefore, $\mathsf{s_{u_H} < s_q + 2 = s_{t_H}}$,
\r
1060 so upon receipt of $\mathsf{u}$, $\mathsf{C}$ will throw an error by the decrease in a
\r
1061 last sequence number similar to Case 1, a contradiction.
\r
1063 Now that we know that $\mathsf{C}$ sees $\mathsf{r_1}$, note that C receives $\mathsf{u}$
\r
1064 immediately after $\mathsf{t}$ by Proposition \ref{prop:seqnumb}. Therefore,
\r
1065 $\mathsf{C}$ could not have seen a message after $\mathsf{t}$ with sequence number less
\r
1066 than $\mathsf{s_m}$. In the $\mathsf{PutDataEntries()}$ subroutine, $\mathsf{J}$ adds every
\r
1067 $\mathsf{cr}$ entry that contains sequence number $\mathsf{s}$ and machine ID
\r
1068 $\mathsf{id}$ of the messsages that win in the collisions before $\mathsf{m}$ into
\r
1069 $\mathsf{CR}$; $\mathsf{CR}$ keeps the collection of live $\mathsf{cr}$ entries, namely
\r
1070 those which not all clients have seen. Hence, for every $\mathsf{i}$, $\mathsf{1 \leq i < |X|}$,
\r
1071 the collision winner that has collided with $\mathsf{x_i}$ will be recorded appropriately. Since all the $\mathsf{cr}$ entries that record the results of the collisions before $\mathsf{p}$ will also be seen when $\mathsf{u}$
\r
1072 is received, and $\mathsf{C}$ sees $\mathsf{r_1}$, ${l_1}$ will be recorded in a $\mathsf{cr}$ entry as the winner in the
\r
1073 collision against ${r_1}$.
\r
1075 When $\mathsf{C}$ receives $\mathsf{u}$, if $\mathsf{C}$
\r
1076 has seen the $\mathsf{cr}$ entry that records the collision at index $\mathsf{s_q + 1}$, it will throw
\r
1077 an error from the mismatch of $\mathsf{\tuple{s_q+1, id_J}}$ with
\r
1078 $\mathsf{\tuple{s_q+1, id_K}}$ in the corresponding $\mathsf{cr}$ entry.
\r
1087 \label{lem:pathmessages}
\r
1088 If there are two messages $\mathsf{t}$ and $\mathsf{u}$, with
\r
1089 $\mathsf{s_t \leq s_u}$, such that $\mathsf{t}$ is in the path of $\mathsf{u}$,
\r
1090 then for any message $\mathsf{p}$ with $\mathsf{s_p \leq s_t}$, iff $\mathsf{p}$ is in
\r
1091 the path of $\mathsf{t}$, it is in the path of $\mathsf{u}$.
\r
1095 If $\mathsf{s_t = s_u}$ or $\mathsf{s_p = s_t}$, then we are done, because the two
\r
1096 relevant messages are the same. If they are different messages, then:
\r
1098 \item Reverse direction: The definition of $\mathsf{t}$ being in the path of
\r
1099 $\mathsf{u}$ is the existence of a message sequence $\mathsf{(\dots, t, \dots, u)}$
\r
1100 such that each message except $\mathsf{u}$ is the parent of the succeeding message.
\r
1101 The path of $\mathsf{u}$ must contain some message with sequence number $\mathsf{s_p}$;
\r
1102 because $\mathsf{p}$ is in the path of $\mathsf{u}$, this message is $\mathsf{p}$
\r
1103 itself. The path of $\mathsf{t}$ is then the prefix of this path ending at $\mathsf{t}$,
\r
1104 which clearly contains $\mathsf{p}$.
\r
1106 \item Forward direction: The path of $\mathsf{t}$ is a substring of the path of
\r
1107 $\mathsf{u}$, so if the path of $\mathsf{t}$ contains $\mathsf{p}$, so does the path
\r
1113 Suppose that there is a transitive closure set $\mathsf{\mathscr{S}}$ of clients,
\r
1114 at sequence number $\mathsf{s_n}$. Then there is some total sequence $\mathsf{T}$ of
\r
1115 length $\mathsf{n}$ such that every client $\mathsf{C}$ in $\mathsf{\mathscr{S}}$
\r
1116 sees a partial sequence $\mathsf{P_C}$ consistent with $\mathsf{T}$.
\r
1121 The definition of consistency of $\mathsf{P_C}$ with $\mathsf{T}$ is that every message
\r
1122 $\mathsf{p \in P_C}$ with sequence number $\mathsf{s_p \le s_n}$ is equal to the message
\r
1123 in that slot in $\mathsf{T}$. Let $\mathsf{C_1}$ be some client in the transitive closure
\r
1124 set, with partial sequence $\mathsf{P_{C_1}}$, and let $\mathsf{u}$ be some message with
\r
1125 $\mathsf{s_u > s_n}$ that $\mathsf{C_1}$ shares with another client. Then let $\mathsf{T}$
\r
1126 be the portion of the path of $\mathsf{u}$ ending at sequence number $\mathsf{s_n}$ and
\r
1127 $\mathsf{t}$ be the message at that sequence number. Clearly, by Lemma \ref{lem:twomessages},
\r
1128 $\mathsf{P_{C_1}}$ is consistent with $\mathsf{T}$. We will show that, for every other client
\r
1129 $\mathsf{D}$ with partial sequence $\mathsf{P_D}$, $\mathsf{P_D}$ has some message whose path
\r
1130 includes $\mathsf{t}$. Because $\mathsf{D}$ is in the transitive closure, there is a sequence
\r
1131 of clients $\mathsf{\mathscr{C} = (C_1, C_2, ..., D)}$ from $\mathsf{C_1}$ to $\mathsf{D}$,
\r
1132 where each shares an edge with the next.
\r
1133 We prove by induction that $\mathsf{P_D}$ has a message whose path includes $\mathsf{t}$.
\r
1135 \item Base case: $\mathsf{P_{C_1}}$ includes $\mathsf{u}$, whose path includes $\mathsf{t}$.
\r
1137 \item Inductive step: Each client in $\mathsf{\mathscr{C}}$ has a partial sequence with a message
\r
1138 that includes $\mathsf{t}$ if the previous client does. Suppose $\mathsf{P_{C_k}}$ has
\r
1139 a message $\mathsf{w}$ with a path that includes $\mathsf{t}$, and shares message $\mathsf{x}$
\r
1140 with $\mathsf{P_{C_{k+1}}}$ such that $\mathsf{s_x > s_n}$. By Lemma \ref{lem:twomessages},
\r
1141 $\mathsf{w}$ or $\mathsf{x}$, whichever has the least sequence number, is in the path of the other,
\r
1142 and therefore by Lemma \ref{lem:pathmessages}, $\mathsf{t}$ is in the path of $\mathsf{x}$.
\r
1144 \item Let $\mathsf{z}$ be the message of $\mathsf{D}$ whose path includes $\mathsf{t}$.
\r
1145 By Lemma \ref{lem:twomessages}, every message in $\mathsf{P_D}$ with sequence number smaller
\r
1146 than $\mathsf{s_w}$ is in the path of $\mathsf{z}$. Since $\mathsf{t}$ is in the path of
\r
1147 $\mathsf{z}$, every message in $\mathsf{P_D}$ with smaller sequence number than
\r
1148 $\mathsf{s_t = s_n}$ is in $\mathsf{T}$.
\r
1149 Therefore, $\mathsf{P_D}$ is consistent with $\mathsf{T}$.
\r
1154 \subsection{Future Work}
\r
1155 \paragraph{Support Messages}
\r
1156 A message is dead once receiving machine sends an entry with a newer
\r
1157 sequence identifier
\r
1159 \paragraph{Persistent data structures}
\r
1160 Root object w/ fields
\r
1161 Other objects can be reachable from root
\r
1162 Each object has its own entries
\r
1163 Dead objects correspond to dead
\r
1165 \paragraph{Multiple App Sharing}
\r
1167 Idea is to separate subspace of entries... Shared with other cloud...
\r
projects / iotcloud.git / blob