Formatting and detailing definitions for formal guarantees

diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex
index e389472dfd6a8cadd94b24a7f88f5ad85ac98e2d..0e27bbfae43e551cbeec06925f382b70da52e86a 100644 (file)
--- a/doc/iotcloud.tex
+++ b/doc/iotcloud.tex
@@ -197,7 +197,7 @@ $id$ is a machine ID\\
 $hmac_p$ is the HMAC value of the previous slot \\\r
 $hmac_c$ is the HMAC value of the current slot \\\r
 $Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
 $hmac_p$ is the HMAC value of the previous slot \\\r
 $hmac_c$ is the HMAC value of the current slot \\\r
 $Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\\r

-$sv_s = \tuple{s, E(Dat_s)} = \r
+$slot_s = \tuple{s, E(Dat_s)} = \r

 \tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\\r
 \textbf{States} \\\r
 \textit{$id_{self}$ = machine Id of this client} \\\r
 \tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\\r
 \textbf{States} \\\r
 \textit{$id_{self}$ = machine Id of this client} \\\r


@@ -829,22 +829,83 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 %\note{Also Missing liveness state definition in algorithm...}\r
 \r
 \r
 %\note{Also Missing liveness state definition in algorithm...}\r
 \r
 \r

-\subsection{Definitions for Formal Guarantees}\r
-\r
-\begin{enumerate}\r
-\item Equality: Two messages $t$ and $u$ are equal if their sequence numbers, senders, and contents are exactly the same.\r
-\item Message: A message $t$, is the tuple $t = (i(t), s(t), contents(t))$ containing the sequence number, machine ID of the sender, and contents of $t$ respectively.\r
-\item Parent: A parent of a message $t$ is the message $A(t)$, unique by the correctness of HMACs, such that $HMAC_C(t) = HMAC_P(A(t))$.\r
-\item Chain: A chain of messages with length $n \ge 1$ is a message sequence $R = (R_i, R_{i+1}, ..., R_{i+n-1})$ such that for every index $i < k \le i+n-1$, $R_k$ has sequence number $k$ and is the parent of $R_{k-1}$.\r
-\item Partial message sequence: A partial message sequence is a sequence of messages, no two with the same sequence number, that can be divided into disjoint chains.\r
-\item Total message sequence: A total message sequence $T$ with length $n$ is a chain of messages that starts at $i = 1$.\r
-\item Path: The path of a message $t$ is the chain that starts at $i = 1$ and whose last message is $t$. The uniqueness of a path follows from the uniqueness of a parent.\r
-\item Consistency: A partial message sequence $P$ is consistent with a total message sequence $T$ of length $n$ if for every message $p \in P$ with $i(p) < n$, $T_{i(p)} = p$. This implies that $\{p \in P | i(p) \le n\}$ is a subsequence of T.\r
-\item Transitive closure set at index $n$: A set $\mathscr{S}$ of clients comprising a connected component of an undirected graph, where two clients are connected by an edge if they both received the same message $t$ with index $i(t) > n$.\r
-\r
-\end{enumerate}\r
-\r
-\subsection{Formal Guarantee}\r
+\subsection{Formal Guarantees}\r
+\subsubsection{Definitions}\r
+\r
+\begin{defn}[Message]\r
+A message $\mathsf{t}$, is the tuple \r
+\begin{center}\r
+$\mathsf{t = \tuple{s, E(Dat_s)}}$ \\\r
+$\mathsf{Dat_s = \tuple{s,id,hmac_p, DE,hmac_c}}$\r
+\end{center}\r
+containing $\mathsf{s}$ as sequence number and $\mathsf{Dat_s}$ as its \r
+encrypted contents. $\mathsf{Dat_s}$ consists of $\mathsf{s}$, \r
+$\mathsf{id}$ as machine ID of the sender, $\mathsf{hmac_p}$ as HMAC \r
+from a previous message, $\mathsf{DE}$ as set of data entries, and \r
+$\mathsf{hmac_c}$ as HMAC from message $\mathsf{t}$ respectively.\r
+\end{defn}\r
+\r
+\begin{defn}[Equality]\r
+Two messages $\mathsf{t}$ and $\mathsf{u}$ are equal if their $\mathsf{s}$, \r
+and $\mathsf{Dat_s}$ are exactly the same.\r
+\end{defn}\r
+\r
+\begin{defn}[Parent]\r
+A parent of a message $\mathsf{t}$ is the message $\mathsf{A(t)}$, unique \r
+by the correctness of HMACs in $\mathsf{Dat_s}$, such that \r
+$\mathsf{hmac_p(t) = hmac_c(A(t))}$.\r
+\end{defn}\r
+\r
+\begin{defn}[Chain]\r
+A chain of messages with length $\mathsf{n \ge 1}$ is a message sequence \r
+$\mathsf{R = (r_i, r_{i+1}, ..., r_{i+n-1})}$ such that for every index \r
+$\mathsf{i < k \le i+n-1}$, $\mathsf{r_k}$ has sequence number $\mathsf{k}$ \r
+and is the parent of $\mathsf{r_{k-1}}$.\r
+\end{defn}\r
+\r
+\begin{defn}[Partial sequence]\r
+A partial sequence $\mathsf{P}$ is a sequence of messages, no two \r
+with the same sequence number, that can be divided into disjoint chains.\r
+\end{defn}\r
+\r
+\begin{defn}[Total sequence]\r
+A total sequence $\mathsf{T =}$ $\mathsf{(t_1, t_2, ..., t_n)}$ with \r
+length $\mathsf{n}$ is a chain of messages that starts at $\mathsf{i = 1}$.\r
+\end{defn}\r
+\r
+\begin{defn}[Path]\r
+The path of a message $\mathsf{t}$ is the chain that starts at $\mathsf{i = 1}$ \r
+and whose last message is $\mathsf{t}$. The uniqueness of a path follows \r
+from the uniqueness of a parent.\r
+\end{defn}\r
+\r
+\begin{defn}[Consistency]\r
+A partial sequence $\mathsf{P}$ is consistent with a total sequence \r
+$\mathsf{T}$ of length $\mathsf{n}$ if for every message $\mathsf{p \in P}$ \r
+with $\mathsf{i(p) \leq n}$, $\mathsf{t_{i(p)} = p}$. This implies that \r
+$\mathsf{\{p \in P | i(p) \le n\}}$ is a partial sequence of $\mathsf{T}$.\r
+\end{defn}\r
+\r
+\begin{defn}[Transitive closure]\r
+Transitive closure set at index $\mathsf{n}$ is a set $\mathscr{S}$ of \r
+clients comprising a connected component of an undirected graph, where two \r
+clients are connected by an edge if they both received the same message \r
+$\mathsf{t}$ with index $\mathsf{i(t) > n}$.\r
+\end{defn}\r
+\r
+%\begin{enumerate}\r
+%\item Equality: Two messages $t$ and $u$ are equal if their sequence numbers, senders, and contents are exactly the same.\r
+%\item Message: A message $t$, is the tuple $t = (i(t), s(t), contents(t))$ containing the sequence number, machine ID of the sender, and contents of $t$ respectively.\r
+%\item Parent: A parent of a message $t$ is the message $A(t)$, unique by the correctness of HMACs, such that $HMAC_C(t) = HMAC_P(A(t))$.\r
+%\item Chain: A chain of messages with length $n \ge 1$ is a message sequence $R = (R_i, R_{i+1}, ..., R_{i+n-1})$ such that for every index $i < k \le i+n-1$, $R_k$ has sequence number $k$ and is the parent of $R_{k-1}$.\r
+%\item Partial message sequence: A partial message sequence is a sequence of messages, no two with the same sequence number, that can be divided into disjoint chains.\r
+%\item Total message sequence: A total message sequence $T$ with length $n$ is a chain of messages that starts at $i = 1$.\r
+%\item Path: The path of a message $t$ is the chain that starts at $i = 1$ and whose last message is $t$. The uniqueness of a path follows from the uniqueness of a parent.\r
+%\item Consistency: A partial message sequence $P$ is consistent with a total message sequence $T$ of length $n$ if for every message $p \in P$ with $i(p) < n$, $T_{i(p)} = p$. This implies that $\{p \in P | i(p) \le n\}$ is a subsequence of T.\r
+%\item Transitive closure set at index $n$: A set $\mathscr{S}$ of clients comprising a connected component of an undirected graph, where two clients are connected by an edge if they both received the same message $t$ with index $i(t) > n$.\r
+%\end{enumerate}\r
+\r
+\subsubsection{Lemmas and Proofs}\r

 \r
 \begin{prop} Every client $J$ who sends a message $t$ has $A(t)$ as its latest stored message, and $i(t) = i(A(t)) + 1$. \end{prop}\r
 \begin{proof} True by definition, because $J$ sets $HMAC_P(t) = HMAC_C(A(t))$ and $i(t) = i(A(t)) + 1$ when a message is sent. \end{proof}\r
 \r
 \begin{prop} Every client $J$ who sends a message $t$ has $A(t)$ as its latest stored message, and $i(t) = i(A(t)) + 1$. \end{prop}\r
 \begin{proof} True by definition, because $J$ sets $HMAC_P(t) = HMAC_C(A(t))$ and $i(t) = i(A(t)) + 1$ when a message is sent. \end{proof}\r


@@ -922,17 +983,17 @@ Forward direction: The path of $t$ is a substring of the path of $u$, so if the
 \end{proof}\r
 \r
 \begin{theorem}\r
 \end{proof}\r
 \r
 \begin{theorem}\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
+Suppose that there is a transitive closure set $\mathscr{S}$ of clients, at index $n$. Then there is some total 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
 \r
 \r
 \begin{proof}\r
 \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) > n$ that $C_1$ shares with another client. Then let $T$ be the portion of the path of $u$ ending at index $n$ 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 clients $\mathscr{C} = (C_1, C_2, ..., D)$ from $C_1$ to $D$, where each shares an edge with the next.\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 sequence $P_{C_1}$, and let $u$ be some message with $i(u) > n$ that $C_1$ shares with another client. Then let $T$ be the portion of the path of $u$ ending at index $n$ 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 clients $\mathscr{C} = (C_1, C_2, ..., D)$ from $C_1$ to $D$, where each shares an edge with the next.\r

 \r
 We prove by induction that $P_D$ has a message whose path includes $t$.\r
 \begin{itemize}\r
 \item Base case: $P_{C_1}$ includes $u$, whose path includes $t$.\r
 \r
 \r
 We prove by induction that $P_D$ has a message whose path includes $t$.\r
 \begin{itemize}\r
 \item Base case: $P_{C_1}$ includes $u$, whose path includes $t$.\r
 \r

-\item Inductive step: Each client in $\mathscr{C}$ has a partial message sequence with a message that includes $t$ if the previous client does. Suppose $P_{C_k}$ has a message $w$ with a path that includes $t$, and shares message $x$ with $P_{C_{k+1}}$ such that $i(x) > n$. By Lemma 1, $w$ or $x$, whichever has the least sequence number, is in the path of the other, and therefore by Lemma 2, $t$ is in the path of $x$.\r
+\item Inductive step: Each client in $\mathscr{C}$ has a partial sequence with a message that includes $t$ if the previous client does. Suppose $P_{C_k}$ has a message $w$ with a path that includes $t$, and shares message $x$ with $P_{C_{k+1}}$ such that $i(x) > n$. By Lemma 1, $w$ or $x$, whichever has the least sequence number, is in the path of the other, and therefore by Lemma 2, $t$ is in the path of $x$.\r

 \r
 \item Let $z$ be the message of $D$ whose path includes $t$. By Lemma 1, every message in $P_D$ with index smaller than $i(w)$ is in the path of $z$. Since $t$ is in the path of $z$, every message in $P_D$ with smaller index than $i(t)$ is in $T$. Therefore, $P_D$ is consistent with $T$.\r
 \r
 \r
 \item Let $z$ be the message of $D$ whose path includes $t$. By Lemma 1, every message in $P_D$ with index smaller than $i(w)$ is in the path of $z$. Since $t$ is in the path of $z$, every message in $P_D$ with smaller index than $i(t)$ is in $T$. Therefore, $P_D$ is consistent with $T$.\r
 \r