From 8874bc9b4e54808cd19783e1bead5b4fbe78e9c7 Mon Sep 17 00:00:00 2001 From: tkwa Date: Tue, 2 Aug 2016 11:36:57 -0700 Subject: [PATCH] Improvements to diagram for Lemma 1 of the proof; added case to Lemma 1 --- doc/iotcloud.tex | 32 +++++++++++++++----------------- 1 file changed, 15 insertions(+), 17 deletions(-) diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex index 89c1c86..36de049 100644 --- a/doc/iotcloud.tex +++ b/doc/iotcloud.tex @@ -687,13 +687,19 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge \begin{figure}[h] \centering - \xymatrix{ -\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_1 \ar[r] & R_2 \ar[r] & \dots \ar[r] & R_m = t} + \xymatrix{ & & S \\ +\dots \ar[r] & q \ar[dr]_{J} \ar[r]^{K} & S_1 \ar[r] & S_2 \ar[r] & \dots \ar[r] & p \ar[r] & \dots \ar[r] & S_n = u \\ +& & R_1 \ar[r] & R_2 \ar[r] & \dots \ar[r] & R_m = t \\ +& & R +\save "2,3"."2,8"*+\frm{^\}} +\save "3,3"."3,6"*+\frm{_\}} +\restore +\restore +} \caption{By Lemma 1, receiving $u$ after $t$ is impossible.} \end{figure} -\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} +\begin{lem} Two packets are received without errors by a client $C$; call them $t$ and $u$ such that $i(t) \le i(u)$. Then $t$ is in the path of $u$. \end{lem} \begin{proof} 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$. @@ -708,28 +714,20 @@ There are two cases: \begin{itemize} \item Case 1: $J$ did not send a message in $S$. Then $v_J(t) > v_J(q) = v_J(u)$. \begin{itemize} -\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. -\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. - +\item Case 1.1: $C$ receives a sequence of messages between $t$ and $u$ with contiguous sequence numbers. In particular, there is some packet $w$ such that $i(w) = i(u) - 1$. If $w$ is the parent of $u$, messages $t$ and $w$ 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. +\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 during this time, which means it must decrease when some message is received, which means C throws an error in the $CheckLastSeqN$ subroutine. \end{itemize} - - -\item Case 2: $J$ sent at least one message in $S$. Call the first one $p$. We know that $i(p) > i(S_1)$, since $J \neq K$. $R_1$ must be sent either before or after $p$. +\item Case 2: $J$ sent at least one message in $S$. Call the first one $p$. We know that $i(p) > i(R_1)$, since $J \neq K$ and $p \neq S_1$. $R_1$ must be sent either before or after $p$. \begin{itemize} -\item Case 2.1: Client $J$ sends $p$, and then $R_1$. When $p$ was sent, whether it was accepted or rejected, $i(J, p) \geq i(p)$. Since $i(p) > i(S_1)$, $i(J, p) > q$. So $i(q) < i(J, p)$, which would cause $J$ to fail to send $R_1$, a contradiction. -\begin{itemize} -\item Case 2.2.1: - - - -\end{itemize} +\item Case 2.1: Client $J$ sends $p$, and then $R_1$. Before sending $p$, the greatest sequence number of a message that $J$ has received, ${s_{last}}_j$, must be equal to $i(p) - 1 \ge i(R_1)$. Since ${s_{last}}_j$ never decreases, Client $J$ cannot then send a message with sequence number $i(R_1)$, a contradiction. \item Case 2.2: Client $J$ sends $R_1$, and then $p$. Let $X = (R_1, \dots )$ be the list of messages $J$ sends starting before $R_1$ and ending before $p$. \begin{itemize} \item Case 2.2.1: Some message in $X$ was accepted. In this case, before sending $p$, $J$'s value for its own latest index would be strictly greater than $v_J(q)$. ($J$ could not have sent a message with index less than $i(q)$ after receiving $q$). When preparing to send $p$, $J$ would have received its own latest index as at most $v_J(q)$. $J$ throws an error before sending $p$, because its own latest index decreases. \item Case 2.2.2: All messages in $X$ were rejected. Client $J$ will always add the latest rejected message to the rejected-message list in the next update; so for every $i$, $1 \leq i < |X|$, the $i$th element of $X$ will be recorded in the RML of all further elements of $X$; and every element of $X$ will be recorded in $RML(p)$. Since every rejected message in $RML(p)$ will be in $RML(C, u)$, and $u$ is the first message that $C$ sees which does not have $t$ in its path, $R_1$ will be recorded in $RML(C, p)$. When $C$ receives $u$, $C$ will throw an error from the match $(J, iq+1)$ in $RML(C, p)$. \end{itemize} \end{itemize} + \end{itemize} \end{proof} -- 2.34.1