author tkwa Tue, 2 Aug 2016 18:36:57 +0000 (11:36 -0700) committer tkwa Tue, 2 Aug 2016 18:36:57 +0000 (11:36 -0700)
 doc/iotcloud.tex patch | blob | history

index 89c1c86..36de049 100644 (file)
@@ -687,13 +687,19 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge \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 + \xymatrix{ & & S \\\r +\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 +& & R_1 \ar[r] & R_2 \ar[r] & \dots \ar[r] & R_m = t \\\r +& & R\r +\save "2,3"."2,8"*+\frm{^\}}\r +\save "3,3"."3,6"*+\frm{_\}}\r +\restore\r +\restore\r +}\r \caption{By Lemma 1, receiving$u$after$t$is impossible.}\r \end{figure}\r \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{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}\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 @@ -708,28 +714,20 @@ There are two cases: \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.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 +\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.\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 during this time, which means it must decrease when some message is received, which means C throws an error in the$CheckLastSeqN$subroutine.\r \end{itemize}\r \r -\r -\r -\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$.\r +\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$.\r \begin{itemize}\r -\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.\r -\begin{itemize}\r -\item Case 2.2.1: \r -\r -\r -\r -\end{itemize}\r +\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.\r \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$.\r \begin{itemize}\r \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.\r \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)\$.\r
\end{itemize}\r
\end{itemize}\r
+\r
\end{itemize}\r
\end{proof}\r
\r