\usepackage{graphicx}\r
\usepackage{mathrsfs}\r
\usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx\r
+\usepackage[all]{xy}\r
\newtheorem{theorem}{Theorem}\r
\newtheorem{prop}{Proposition}\r
\newtheorem{lem}{Lemma}\r
(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
\r
\subsection{Server Algorithm}\r
-$s \in SN$ is a sequence number set\\\r
+$s \in SN$ is a sequence number\\\r
$sv \in SV$ is a slot's value\\\r
$slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\ \\\r
\textbf{State} \\\r
$cr$ is a collision resolution entry $\tuple{s_{col},id_{col}}$, \r
s + id of a machine that wins a collision, $cr \in DE$ \\\r
$DE$ is a set of all data entries, possibly of different types, in a single message \\\r
-$s \in SN$ is a sequence number set \\\r
+$s \in SN$ is a sequence number \\\r
$id$ is a machine ID\\\r
$hmac_p$ is the HMAC value of the previous slot \\\r
$hmac_c$ is the HMAC value of the current slot \\\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{ValidPrevHmac}{$DE_s,hmac_{p_s},hmac_{p_{sto}}$}\r
-\If{$hmac_{p_s} = \emptyset$}\Comment{First slot - no previous HMAC}\r
+\Function{ValidPrevHmac}{$s_s,DE_s,hmac_{p_s},hmac_{p_{sto}}$}\r
+\If{$s_s = 0 \land hmac_{p_s} = \emptyset$}\Comment{First slot - no previous HMAC}\r
\State \Return $true$\r
\Else\r
\State \Return {$hmac_{p_{sto}} = hmac_{p_s}$}\r
\EndFunction\r
\end{algorithmic}\r
\r
-\note{So if a slot has a null previous hmac, everything is fine? What if it isn't the first slot?}\r
-\r
\begin{algorithmic}[1]\r
\Function{GetQueSta}{$Dat_s$}\r
\State $DE_s \gets GetDatEnt(DE_s)$\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{GetColRes}{$Dat_s$}\Comment{At most 2 $cr$ entries in a slot}\r
+\Function{GetColRes}{$Dat_s$} %\Comment{At most 2 $cr$ entries in a slot}\r
\State $DE_s \gets GetDatEnt(Dat_s)$\r
\State $de_{cr} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
de_s \in D \land de_s = cr$\r
\State $\tuple{s_{ret},id_{ret}} \r
\gets \emptyset$\r
\EndIf\r
-\State $de_{r_{cr}} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
- de_s \in D \land de_s = cr \land de_s \neq de_{cr}$\r
-\If{$de_{r_{cr}} \neq \emptyset$}\r
- \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \gets GetCR(de_{r_{cr}})$\r
-\Else\r
- \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \r
- \gets \emptyset$\r
-\EndIf\r
-\State \Return{$\{\tuple{s_{ret},id_{ret}},\tuple{s_{r_{ret}},id_{r_{ret}}}\}$}\r
+%\State $de_{r_{cr}} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
+% de_s \in D \land de_s = cr \land de_s \neq de_{cr}$\r
+%\If{$de_{r_{cr}} \neq \emptyset$}\r
+% \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \gets GetCR(de_{r_{cr}})$\r
+%\Else\r
+% \State $\tuple{s_{r_{ret}},id_{r_{ret}}} \r
+% \gets \emptyset$\r
+%\EndIf\r
+%\State \Return{$\{\tuple{s_{ret},id_{ret}},\tuple{s_{r_{ret}},id_{r_{ret}}}\}$}\r
+\State \Return{$\{\tuple{s_{ret},id_{ret}}\}$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\State $MS_g \gets \emptyset$\r
\State $SM_{curr} \gets \emptyset$\r
\State $\tuple{s_{g_{max}},sv_{g_{max}}} \gets MaxSlot(SL_g)$\r
-\State $s_{g_{max}} \gets SeqN(\tuple{s_{g_{max}},sv_{g_{max}}})$\r
\State $\tuple{s_{g_{min}},sv_{g_{min}}} \gets MinSlot(SL_g)$\r
-\State $s_{g_{min}} \gets SeqN(\tuple{s_{g_{min}},sv_{g_{min}}})$\r
\For{$s_g \gets s_{g_{min}}$ \textbf{to} $s_{g_{max}}$}\Comment{Process slots \r
in $SL_g$ in order}\r
\State $\tuple{s_g,sv_g} \gets Slot(SL_g,s_g)$\r
\EndIf\r
\State $DE_g \gets GetDatEnt(Dat_g)$\r
\State $hmac_{p_{stored}} \gets GetPrevHmac(Dat_g)$\r
- \If{$\neg \Call{ValidPrevHmac}{DE_g,hmac_{p_g},hmac_{p_{stored}}}$}\r
- \State \Call{Error}{'Invalid previous HMAC value'}\r
+ \If{$\neg \Call{ValidPrevHmac}{s_g,DE_g,hmac_{p_g},hmac_{p_{stored}}}$}\r
+ \State \Call{ReportError}{'Invalid previous HMAC value'}\r
\EndIf\r
\State $hmac_{c_g} \gets GetCurrHmac(Dat_g)$\r
\If{$\neg \Call{ValidHmac}{DE_g,SK,hmac_{c_g}}$}\r
\If{$\tuple{id_d,s_{d_{last}}} \neq \emptyset$}\r
\State $MS_g \gets \Call{UpdateLastSeqN}{id_d,s_{d_{last}},MS_g}$\r
\EndIf\r
- \State $\{\tuple{s_e,id_e},\tuple{s_f,id_f}\} \gets \r
- \Call{GetColRes}{Dat_g}$\Comment{Handle cr}\r
+ %\State $\{\tuple{s_e,id_e},\tuple{s_f,id_f}\} \gets \r
+ % \Call{GetColRes}{Dat_g}$\Comment{Handle cr}\r
+ \State $\{\tuple{s_e,id_e}\} \gets \Call{GetColRes}{Dat_g}$\Comment{Handle cr}\r
\State $\Call{CheckCollision}{MS,SM,\tuple{s_e,id_e}}$\Comment{From normal slot}\r
- \State $\Call{CheckCollision}{MS,SM,\tuple{s_f,id_f}}$\Comment{From reinsertion}\r
+ %\State $\Call{CheckCollision}{MS,SM,\tuple{s_f,id_f}}$\Comment{From reinsertion}\r
\State $sl_{last} \gets \Call{StoreLastSlot}{MS,sl_{last},s_g,sv_g,id_g}$\r
\State $DT \gets \Call{UpdateDT}{DT,Dat_g}$\r
\EndFor\r
$k$ is key of entry \\\r
$v$ is value of entry \\\r
$kv$ is a key-value entry $\tuple{k,v}$\\\r
-$D = \{kv,ss,qs,cr\}$ \\\r
-$DE = \{de \mid de \in D\}$ \\\r
+$DE$ is a set of data entries, possibly of different types \\\r
$Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
$sv_s = \tuple{s, E(Dat_s)} = \r
\tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\\r
\textbf{States} \\\r
-\textit{$cp$ = data entry $DE$ maximum size/capacity} \\\r
+\textit{$capacity$ = data entry $DE$ maximum size/capacity} \\\r
\textit{$cr_p$ = saved cr entry $\tuple{s,id}$ on client if there is a collision\r
(sent in the following slot)} \\\r
\textit{$cr_{p_{last}}$ = saved cr entry $\tuple{s,id}$ on client if there is a \r
$\tuple{s_{last},sv_{last},id_{last}}$ (initially $\emptyset$)} \\\r
\textit{$th_p$ = threshold number of dead slots for a resize to happen} \\\r
\textit{$m'_p$ = offset added to $max$ for resize} \\\r
-\textit{$KV$ = set of $\tuple{ck, \tuple{k,v}}$ of kv entries on client} \\\r
+\textit{$KV$ = associative array of $\tuple{ck, \tuple{k,v}}$ kv entries on client} \\\r
\textit{$SL_p$ = set of returned slots on client} \\\r
\textit{SK = Secret Key} \\ \\\r
\textbf{Helper Functions} \\\r
\forall \tuple{ck_s,\tuple{k_s, v_s}} \in KV_s, k = k_s$ \\\r
\r
\begin{algorithmic}[1]\r
-\Function{PutKVPair}{$KV_s,\tuple{k_s,v_s}$}\r
-\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKV(KV_s,k_s)$\r
+\Function{PutKVPair}{$\tuple{k_s,v_s}$}\r
+\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKV(KV,k_s)$\r
\If{$\tuple{ck_s,\tuple{k_s,v_t}} = \emptyset$}\r
- \State $KV_s \gets KV_s \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$\r
+ \State $KV \gets KV \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$\r
\State $ck_p \gets ck_p + 1$\r
\Else\r
- \State $KV_s \gets (KV_s - \{\tuple{ck_s, \tuple{k_s,v_t}}\}) \cup \r
+ \State $KV \gets (KV - \{\tuple{ck_s, \tuple{k_s,v_t}}\}) \cup \r
\{\tuple{ck_s, \tuple{k_s,v_s}}\}$\r
\EndIf\r
\State \Return{$KV_s$}\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{ReinsertLastSlot}{$need_s,sl_{s_{last}},max'_s$}\r
-\If{$need_s$}\r
- \State $s_s \gets GetLastS(sl_{s_{last}})$\r
- \State $sv_s \gets GetSV(sl_{s_{last}})$\r
- \State $\tuple{stat_s,SL_s} \gets \Call{PutSlot}{s_s,sv_s,max'_s}$\r
- \State $cr_s \gets \Call{HandleCollision}{\tuple{stat_s,SL_s}}$\r
-\EndIf\r
-\State \Return{$cr_s$}\r
+\r
+\Function{ReinsertLastSlot}{$MS_s,SK_s,sl_{s_{last}},max'_s,hmac_{p_s}$}\r
+\State $s_s \gets MaxLastSeqN(MS_s)$\r
+\State $sv_s \gets GetSV(sl_{s_{last}})$\r
+\State $Dat_s \gets Decrypt(SK,sv_s)$\r
+\State $DE_s \gets GetDatEnt(Dat_s)$\r
+\State $hmac_{c_s} \gets Hmac(DE_s,SK_s)$\r
+\State $Dat_s \gets CreateDat(s_s,id_{self},hmac_{p_s},DE_p,hmac_{c_s})$\r
+\State $hmac_{p_s} \gets hmac_{c_s}$\r
+\State $\tuple{stat_s,SL_s} \gets \Call{PutSlot}{s_s,sv_s,max'_s}$ \r
+\State $cr_s \gets \Call{HandleCollision}{\tuple{stat_s,SL_s}}$\r
+\State \Return{$\tuple{cr_s,hmac_{p_p}}$}\r
+\r
\EndFunction\r
\end{algorithmic}\r
\note{Shouldn't this function do something pretty sophisticated about seeing what data we actually need to keep from the last slot and not just insert the entire thing?}\r
\r
-\note{Probably best to just not call this function is $need_s$ is false and not pass in such parameters. It makes it harder to read.}\r
-\r
+\note{Probably best to just not call this function if $need_s$ is false and not pass in such parameters. It makes it harder to read.}\r
\r
\begin{algorithmic}[1]\r
\Function{GetDEPairs}{$KV_s,max'_s,need_s,sl_s$}\r
\State $DE_{ret} \gets \emptyset$\r
-\State $cp_s \gets cp$\r
+\State $capacity_s \gets capacity$\r
\If{$cr_p \neq \emptyset$}\Comment{Check and insert a $cr$}\r
\State $DE_{ret} \gets DE_{ret} \cup cr_p$\r
- \State $cp_s \gets cp_s - 1$\r
+ \State $capacity_s \gets capacity_s - 1$\r
\EndIf\r
\If{$cr_{p_{last}} \neq \emptyset$}\Comment{Check and insert a $cr$}\r
\State $DE_{ret} \gets DE_{ret} \cup cr_{p_{last}}$\r
- \State $cp_s \gets cp_s - 1$\r
+ \State $capacity_s \gets capacity_s - 1$\r
\EndIf\r
\If{$max'_s \neq \emptyset$}\Comment{Check and insert a $qs$}\r
\State $qs_s \gets max'_s$\r
\State $DE_{ret} \gets DE_{ret} \cup qs_s$\r
- \State $cp_s \gets cp_s - 1$\r
+ \State $capacity_s \gets capacity_s - 1$\r
\EndIf\r
\If{$need_s$}\Comment{Check and insert a $ss$}\r
\State $id_s \gets GetID(sl_s)$\r
\State $s_{s_{last}} \gets GetLastS(sl_s)$\r
\State $ss_s \gets CreateSS(id_s,s_{s_{last}})$\r
\State $DE_{ret} \gets DE_{ret} \cup ss_s$\r
- \State $cp_s \gets cp_s - 1$\r
+ \State $capacity_s \gets capacity_s - 1$\r
\EndIf\r
-\If{$|KV_s| \leq cp$}\Comment{$KV$ set can extend multiple slots}\r
+\If{$|KV_s| \leq capacity$}\Comment{$KV$ set can extend multiple slots}\r
\State $DE_{ret} \gets DE_{ret} \cup\r
\{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s\}$\r
\Else\r
\State $DE_{ret} \gets DE_{ret} \cup\r
\{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s,\r
- ck_g \leq ck_s < ck_g + cp_s\}$\r
- \If{$|DE_{ret}| = cp$}\r
- \State $ck_g \gets ck_g + cp_s$\Comment{Middle of KV set}\r
+ ck_g \leq ck_s < ck_g + capacity_s\}$\r
+ \If{$|DE_{ret}| = capacity$}\r
+ \State $ck_g \gets ck_g + capacity_s$\Comment{Middle of KV set}\r
\Else\r
\State $ck_g \gets 0$\Comment{End of KV set}\r
\EndIf\r
\State $sv_p \gets Encrypt(Dat_p,SK)$\r
\State $\tuple{stat_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$\r
\State $cr_p \gets \Call{HandleCollision}{\tuple{stat_p,SL_p}}$\r
-\State $cr_{p_{last}} \gets \Call{ReinsertLastSlot}{need_p,sl_{last},max'_p}$\r
+\If{$need_p$}\r
+ \State $cr_{p_{last}} \gets \Call{ReinsertLastSlot}{sl_{last},max'_p}$\r
+\EndIf\r
\EndProcedure\r
\end{algorithmic}\r
\r
\begin{prop} If a rejected message entry is added to the RML at index $i$, the message will remain in the RML until every client has seen it. \end{prop}\r
\begin{proof} Every RML entry $e$ remains in the queue until it reaches the tail, and is refreshed by the next sender $J$ at that time if $min(MS) > i(e)$; that is, until every client has sent a message with sequence number greater than $i(e)$. Because every client who sends a message with index $i$ has the state of the queue at $i - 1$, this client will have seen the message at $i(e)$. \end{proof}\r
\r
-\begin{lem} \r
-\r
-\end{lem}\r
+\begin{figure}[h]\r
+ \centering\r
+ \xymatrix{\r
+\dots \ar[r] & q \ar[dr]_{J} \ar[r]^{K} & S_1 \ar[r] & S_2 \ar[rr] & & \dots \ar[r] & S_n = u \\\r
+& & R_1 \ar[r] & R_2 \ar[r] & \dots \ar[r] & R_m = t}\r
+\caption{By Lemma 1, receiving $u$ after $t$ is impossible.}\r
+\end{figure}\r
\r
-\begin{lem} If two packets $t$ and $u$, with $i(t) \le i(u)$, are received without errors by a client $C$, then $t$ is in the path of $u$. \end{lem}\r
+\begin{lem} Two packets are received without errors by a client $C$; we can call them $t$ and $u$ such that $i(t) \le i(u)$. Then $t$ is in the path of $u$. \end{lem}\r
\begin{proof}\r
+Clearly $C$ will throw an error if $i(t) = i(u)$. So $i(t) < i(u)$. Additionally, if $C$ receives $u$ before $t$, this will cause it to throw an error, so $t$ is received before $u$.\r
+\r
Assume that $t$ is not in the path of $u$. Take $u$ to be the packet of smallest index for which this occurs, and $t$ be the packet with largest index for this $u$. We will prove that an error occurs upon receipt of $u$.\r
\r
Let $R_1$ be the earliest member of the path of $t$ that is not in the path of $u$, and $q$ be its parent. $q$, the last common ancestor of $t$ and $u$, must exist, since all clients and the server were initialized with the same state. Let $S_1$ be the successor of $q$ that is in the path of $u$; we know $S_1 \neq R_1$. Let $R = (R_1, R_2, \dots, R_m = t)$ be the distinct portion of the path of $t$, and similarly let $S$ be the distinct portion of the path of $S_n = u$.\r
\begin{itemize}\r
\item Case 1: $J$ did not send a message in $S$. Then $v_J(t) > v_J(q) = v_J(u)$.\r
\begin{itemize}\r
-\item Case 1.1: $C$ will throw an error, because the latest index of $J$ changes in the opposite direction of the sequence number: $v_J(u) < v_J(t)$ but $i(u) > i(t)$.\r
-\r
-\r
+\item Case 1.2: $C$ receives a sequence of messages between $t$ and $u$ with contiguous sequence numbers. In particular, there is some packet $p$ such that $i(p) = i(u) + 1$. If $p$ is the parent of $u$, messages $t$ and $p$ are a violation of this lemma such that $p$ has a smaller sequence number than $u$; but this contradicts our assumption that $u$ had the smallest sequence number. If $t$ is not the parent of $u$, $HMAC_p(u) \neq HMAC_c(t)$, causing $C$ to error.\r
+\item Case 1.2: Case 1.1 does not occur; therefore, $C$ must update its slot sequence list at some point between receiving $t$ and $u$. The latest index of $J$ decreases overall during this time, which means it must decrease when some message is received, which means C throws an error in the $CheckLastSeqN$ subroutine.\r
\r
\end{itemize}\r
\r
Suppose that there is a transitive closure set $\mathscr{S}$ of clients, at index $n$. Then there is some total message sequence $T$ of length $n$ such that every client $C$ in $\mathscr{S}$ sees a partial sequence $P_C$ consistent with $T$. \end{theorem}\r
\r
\begin{proof}\r
-The definition of consistency of $P_C$ with $T$ is that every message $p \in P_C$ with index $i(p) \le n$ is equal to the message in that slot in $T$. Let $C_1$ be some client in the transitive closure set, with partial message sequence $P_{C_1}$, and let $u$ be some message with $i(u) > i$ that $C_1$ shares with another client. Then let $T$ be the portion of the path of $u$ ending at index $i$ and $t$ be the message at that index. Clearly, by Lemma 1, $P_{C_1}$ is consistent with $T$, and furthermore. We will show that, for every other client $D$ with partial sequence $P_D$, $P_D$ has some message whose path includes $t$. Because $D$ is in the transitive closure, there is a sequence of edges from $C_1$ to $D$. Call this $\mathscr{C} = (C_1, C_2, ..., D)$. I will prove by induction that $D$ has a message whose path includes $t$.\r
+The definition of consistency of $P_C$ with $T$ is that every message $p \in P_C$ with index $i(p) \le n$ is equal to the message in that slot in $T$. Let $C_1$ be some client in the transitive closure set, with partial message sequence $P_{C_1}$, and let $u$ be some message with $i(u) > i$ that $C_1$ shares with another client. Then let $T$ be the portion of the path of $u$ ending at index $i$ and $t$ be the message at that index. Clearly, by Lemma 1, $P_{C_1}$ is consistent with $T$. We will show that, for every other client $D$ with partial sequence $P_D$, $P_D$ has some message whose path includes $t$. Because $D$ is in the transitive closure, there is a sequence of edges from $C_1$ to $D$. Call this $\mathscr{C} = (C_1, C_2, ..., D)$. I will prove by induction that $D$ has a message whose path includes $t$.\r
\r
For the base case, $P_{C_1}$ includes $u$, whose path includes $t$. For the inductive step, suppose $P_{C_k}$ has an message $w$ with a path that includes $t$, and shares message $x$ with $P_{C_{k+1}}$ such that $i(x) > i$. If $i(w) = i(x)$, then $w = x$. If $i(w) < i(x)$, then, by Lemma 1, $w$ is in the path of $x$. If $i(w) > i(x)$, $x$ is in the path of $w$; note again that its index is greater than $i$. In any case, $t$ is in the path of $u_k+1$.\r
\r
projects / iotcloud.git / blobdiff