From 8744732c7a461b5a99bf961eaa329aabce91d0d2 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 5 Aug 2016 09:46:14 -0700 Subject: [PATCH] Formatting and detailing definitions for formal guarantees --- doc/iotcloud.tex | 101 +++++++++++++++++++++++++++++++++++++---------- 1 file changed, 81 insertions(+), 20 deletions(-) diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex index e389472..0e27bbf 100644 --- 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 \\ $hmac_c$ is the HMAC value of the current slot \\ $Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\ -$sv_s = \tuple{s, E(Dat_s)} = +$slot_s = \tuple{s, E(Dat_s)} = \tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\ \textbf{States} \\ \textit{$id_{self}$ = machine Id of this client} \\ @@ -829,22 +829,83 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge %\note{Also Missing liveness state definition in algorithm...} -\subsection{Definitions for Formal Guarantees} - -\begin{enumerate} -\item Equality: Two messages $t$ and $u$ are equal if their sequence numbers, senders, and contents are exactly the same. -\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. -\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))$. -\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}$. -\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. -\item Total message sequence: A total message sequence $T$ with length $n$ is a chain of messages that starts at $i = 1$. -\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. -\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. -\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$. - -\end{enumerate} - -\subsection{Formal Guarantee} +\subsection{Formal Guarantees} +\subsubsection{Definitions} + +\begin{defn}[Message] +A message $\mathsf{t}$, is the tuple +\begin{center} +$\mathsf{t = \tuple{s, E(Dat_s)}}$ \\ +$\mathsf{Dat_s = \tuple{s,id,hmac_p, DE,hmac_c}}$ +\end{center} +containing $\mathsf{s}$ as sequence number and $\mathsf{Dat_s}$ as its +encrypted contents. $\mathsf{Dat_s}$ consists of $\mathsf{s}$, +$\mathsf{id}$ as machine ID of the sender, $\mathsf{hmac_p}$ as HMAC +from a previous message, $\mathsf{DE}$ as set of data entries, and +$\mathsf{hmac_c}$ as HMAC from message $\mathsf{t}$ respectively. +\end{defn} + +\begin{defn}[Equality] +Two messages $\mathsf{t}$ and $\mathsf{u}$ are equal if their $\mathsf{s}$, +and $\mathsf{Dat_s}$ are exactly the same. +\end{defn} + +\begin{defn}[Parent] +A parent of a message $\mathsf{t}$ is the message $\mathsf{A(t)}$, unique +by the correctness of HMACs in $\mathsf{Dat_s}$, such that +$\mathsf{hmac_p(t) = hmac_c(A(t))}$. +\end{defn} + +\begin{defn}[Chain] +A chain of messages with length $\mathsf{n \ge 1}$ is a message sequence +$\mathsf{R = (r_i, r_{i+1}, ..., r_{i+n-1})}$ such that for every index +$\mathsf{i < k \le i+n-1}$, $\mathsf{r_k}$ has sequence number $\mathsf{k}$ +and is the parent of $\mathsf{r_{k-1}}$. +\end{defn} + +\begin{defn}[Partial sequence] +A partial sequence $\mathsf{P}$ is a sequence of messages, no two +with the same sequence number, that can be divided into disjoint chains. +\end{defn} + +\begin{defn}[Total sequence] +A total sequence $\mathsf{T =}$ $\mathsf{(t_1, t_2, ..., t_n)}$ with +length $\mathsf{n}$ is a chain of messages that starts at $\mathsf{i = 1}$. +\end{defn} + +\begin{defn}[Path] +The path of a message $\mathsf{t}$ is the chain that starts at $\mathsf{i = 1}$ +and whose last message is $\mathsf{t}$. The uniqueness of a path follows +from the uniqueness of a parent. +\end{defn} + +\begin{defn}[Consistency] +A partial sequence $\mathsf{P}$ is consistent with a total sequence +$\mathsf{T}$ of length $\mathsf{n}$ if for every message $\mathsf{p \in P}$ +with $\mathsf{i(p) \leq n}$, $\mathsf{t_{i(p)} = p}$. This implies that +$\mathsf{\{p \in P | i(p) \le n\}}$ is a partial sequence of $\mathsf{T}$. +\end{defn} + +\begin{defn}[Transitive closure] +Transitive closure set at index $\mathsf{n}$ is 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 +$\mathsf{t}$ with index $\mathsf{i(t) > n}$. +\end{defn} + +%\begin{enumerate} +%\item Equality: Two messages $t$ and $u$ are equal if their sequence numbers, senders, and contents are exactly the same. +%\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. +%\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))$. +%\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}$. +%\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. +%\item Total message sequence: A total message sequence $T$ with length $n$ is a chain of messages that starts at $i = 1$. +%\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. +%\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. +%\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$. +%\end{enumerate} + +\subsubsection{Lemmas and Proofs} \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} \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} @@ -922,17 +983,17 @@ Forward direction: The path of $t$ is a substring of the path of $u$, so if the \end{proof} \begin{theorem} -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} +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} \begin{proof} -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. +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. We prove by induction that $P_D$ has a message whose path includes $t$. \begin{itemize} \item Base case: $P_{C_1}$ includes $u$, whose path includes $t$. -\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$. +\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$. \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$. -- 2.34.1