Further changes to Lemma 1; still not done

diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex
index 66881312697f6af727ef83cc724b4ae11df4b70e..6b812d3dc929a9fab023e9cd0d9b336a8e9e55cf 100644 (file)
--- a/doc/iotcloud.tex
+++ b/doc/iotcloud.tex
@@ -718,14 +718,26 @@ Assume that $t$ is not in the path of $u$. Take $u$ to be the packet of smallest
 \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
 \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
 \r

-Let $J = s(R_1)$, and $K = s(S_1)$. Because no client can send two messages with the same index, and $i(R_1) = i(S_1) = i(q) + 1$, we know that $J \neq K$.\r
+Let $J$ be the client who sent $R_1$; that is, such that ${id_self}_J = GetMacID(R_1)$, and $K$ be the client who sent $S_1$.\r
+\r
+We know the following three facts: \r
+\r
+\begin{enumerate}\r
+\r
+\item Because no client can send two messages with the same index, and $i(R_1) = i(S_1) = i(q) + 1$, $J \neq K$.\r
+\r
+\item To send a message $p$ that is the parent of some other message, one must have the received the parent of $p$. Since $u$ is the message with smallest sequence number received by any client that violate this lemma, no client receives both a message in $R$ and a message in $S$; therefore, no client sends both a message in $(R_2,...,t)$ and a message in $(S_2,...,u)$.\r
+\r
+\item Since $u$ are the greatest- and least- sequence number messages that violate this lemma, $C$ does not receive any message with sequence number strictly between $i(t)$ and $i(u)$. Because the $s_{last}$ that $C$ stores increases at every message receipt event, $C$ also does not receive any message after $t$ and before $u$ in real time.\r
+\r
+\end{enumerate}\r

 \r
 There are two cases:\r
 \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
 \r
 There are two cases:\r
 \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$ 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.1: $C$ never updates its slot sequence list between receiving $t$ and receiving $u$; this can only happen if $i(t) = i(u) - 1$. Since $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
 \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


@@ -735,7 +747,7 @@ There are two cases:
 \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. Let $v_J(w)$ be the greatest sequence number of the messages that client $J$ sent in the path of message $w$. In this case, before sending $p$, $J$'s value $SM_J[J]$ for its own latest index would be strictly greater than $v_J(q)$. If there is a sequence of messages with contiguous sequence numbers that $J$ receives between $R_1$ and $p$, J throws an error for a similar reason as Case 1.1. Otherwise, when preparing to send $p$, $J$ would have received an update of 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: 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. Let $v_J(w)$ be the greatest sequence number of the messages that client $J$ sent in the path of message $w$. In this case, before sending $p$, $J$'s value $SM_J[J]$ for its own latest index would be strictly greater than $v_J(q)$. If there is a sequence of messages with contiguous sequence numbers that $J$ receives between $R_1$ and $p$, J throws an error for a similar reason as Case 1.1. Otherwise, when preparing to send $p$, $J$ would have received an update of 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, making $p$ the first message of $J$ that is accepted after $R_1$. Note that $u$ is the message with least sequence number that violates this lemma, and therefore the first one that $C$ receives after $t$. Therefore, $C$ could not have seen a message after $t$ with index less than $i(p)$. In the $PutDataEntries$ subroutine, $J$ adds every rejected message to the ; 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 $CR_C(p)$. Since every rejected message in $CR(p)$ will be in $CR_C(u)$, $R_1$ will be recorded in $CR_C(p)$. When $C$ receives $u$, $C$ will throw an error from the match $(J, i(q)+1)$ in $CR_C(p)$.\r
+\item Case 2.2.2: All messages in $X$ were rejected, making $p$ the first message of $J$ that is accepted after $R_1$. Note that $u$ is the message with least sequence number that violates this lemma, and therefore the first one that $C$ receives after $t$. Therefore, $C$ could not have seen a message after $t$ with index less than $i(p)$. In the $PutDataEntries$ subroutine, $J$ adds every rejected message to $CR(P)$; 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 $CR_C(p)$. Since every rejected message in $CR(p)$ will be in $CR_C(u)$, $R_1$ will be recorded in $CR_C(p)$. When $C$ receives $u$, $C$ will throw an error from the match $(J, i(q)+1)$ in $CR_C(p)$.\r

 \item Case 2.2.2.1: \r
 \end{itemize}\r
 \end{itemize}\r
 \item Case 2.2.2.1: \r
 \end{itemize}\r
 \end{itemize}\r