$k$ is key of entry \\\r
$v$ is value of entry \\\r
$kv$ is a key-value entry $\tuple{k,v}$\\\r
- $DE$ is a set of data entries, possibly of different types \\\r
+ $D = \{kv,ss,qs,cr\}$ \\\r
+ $DE = \{de \mid de \in D\}$ \\\r
$Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
$sv_s = \tuple{s, E(Dat_s)} = \r
\tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\\r
\textbf{States} \\\r
- \textit{$capacity$ = data entry $DE$ maximum size/capacity} \\\r
+ \textit{$cp$ = data entry $DE$ maximum size/capacity} \\\r
\textit{$cr_p$ = saved cr entry $\tuple{s,id}$ on client if there is a collision\r
(sent in the following slot)} \\\r
\textit{$cr_{p_{last}}$ = saved cr entry $\tuple{s,id}$ on client if there is a \r
$\tuple{s_{last},sv_{last},id_{last}}$ (initially $\emptyset$)} \\\r
\textit{$th_p$ = threshold number of dead slots for a resize to happen} \\\r
\textit{$m'_p$ = offset added to $max$ for resize} \\\r
- \textit{$KV$ = associative array of $\tuple{ck, \tuple{k,v}}$ kv entries on client} \\\r
+ \textit{$KV$ = set of $\tuple{ck, \tuple{k,v}}$ of kv entries on client} \\\r
\textit{$SL_p$ = set of returned slots on client} \\\r
\textit{SK = Secret Key} \\ \\\r
\textbf{Helper Functions} \\\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
- \r
\Function{ReinsertLastSlot}{$MS_s,SK_s,sl_{s_{last}},max'_s,hmac_{p_s}$}\r
\State $s_s \gets MaxLastSeqN(MS_s)$\r
\State $sv_s \gets GetSV(sl_{s_{last}})$\r
\State $\tuple{stat_s,SL_s} \gets \Call{PutSlot}{s_s,sv_s,max'_s}$ \r
\State $cr_s \gets \Call{HandleCollision}{\tuple{stat_s,SL_s}}$\r
\State \Return{$\tuple{cr_s,hmac_{p_p}}$}\r
- \r
\EndFunction\r
\end{algorithmic}\r
\note{Shouldn't this function do something pretty sophisticated about seeing what data we actually need to keep from the last slot and not just insert the entire thing?}\r
\r
\note{Probably best to just not call this function if $need_s$ is false and not pass in such parameters. It makes it harder to read.}\r
\r
+ \r
\begin{algorithmic}[1]\r
\Function{GetDEPairs}{$KV_s,max'_s,need_s,sl_s$}\r
\State $DE_{ret} \gets \emptyset$\r
- \State $capacity_s \gets capacity$\r
+ \State $cp_s \gets cp$\r
\If{$cr_p \neq \emptyset$}\Comment{Check and insert a $cr$}\r
\State $DE_{ret} \gets DE_{ret} \cup cr_p$\r
- \State $capacity_s \gets capacity_s - 1$\r
- \EndIf\r
- \If{$cr_{p_{last}} \neq \emptyset$}\Comment{Check and insert a $cr$}\r
- \State $DE_{ret} \gets DE_{ret} \cup cr_{p_{last}}$\r
- \State $capacity_s \gets capacity_s - 1$\r
+ \State $cp_s \gets cp_s - 1$\r
\EndIf\r
+ %\If{$cr_{p_{last}} \neq \emptyset$}\Comment{Check and insert a $cr$}\r
+ % \State $DE_{ret} \gets DE_{ret} \cup cr_{p_{last}}$\r
+ % \State $cp_s \gets cp_s - 1$\r
+ %\EndIf\r
\If{$max'_s \neq \emptyset$}\Comment{Check and insert a $qs$}\r
\State $qs_s \gets max'_s$\r
\State $DE_{ret} \gets DE_{ret} \cup qs_s$\r
- \State $capacity_s \gets capacity_s - 1$\r
+ \State $cp_s \gets cp_s - 1$\r
\EndIf\r
- \If{$need_s$}\Comment{Check and insert a $ss$}\r
- \State $id_s \gets GetID(sl_s)$\r
- \State $s_{s_{last}} \gets GetLastS(sl_s)$\r
- \State $ss_s \gets CreateSS(id_s,s_{s_{last}})$\r
- \State $DE_{ret} \gets DE_{ret} \cup ss_s$\r
- \State $capacity_s \gets capacity_s - 1$\r
- \EndIf\r
- \If{$|KV_s| \leq capacity$}\Comment{$KV$ set can extend multiple slots}\r
+ %\If{$need_s$}\Comment{Check and insert a $ss$}\r
+ % \State $id_s \gets GetID(sl_s)$\r
+ % \State $s_{s_{last}} \gets GetLastS(sl_s)$\r
+ % \State $ss_s \gets CreateSS(id_s,s_{s_{last}})$\r
+ % \State $DE_{ret} \gets DE_{ret} \cup ss_s$\r
+ % \State $cp_s \gets cp_s - 1$\r
+ %\EndIf\r
+ \If{$|KV_s| \leq cp$}\Comment{$KV$ set can extend multiple slots}\r
\State $DE_{ret} \gets DE_{ret} \cup\r
\{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s\}$\r
\Else\r
\State $DE_{ret} \gets DE_{ret} \cup\r
\{\tuple{k_s,v_s} \mid \tuple{ck_s,\tuple{k_s,v_s}} \in KV_s,\r
- ck_g \leq ck_s < ck_g + capacity_s\}$\r
- \If{$|DE_{ret}| = capacity$}\r
- \State $ck_g \gets ck_g + capacity_s$\Comment{Middle of KV set}\r
+ ck_g \leq ck_s < ck_g + cp_s\}$\r
+ \If{$|DE_{ret}| = cp$}\r
+ \State $ck_g \gets ck_g + cp_s$\Comment{Middle of KV set}\r
\Else\r
\State $ck_g \gets 0$\Comment{End of KV set}\r
\EndIf\r
\r
\begin{algorithmic}[1]\r
\Procedure{PutDataEntries}{$th_p,m'_p$}\r
- \State $s_p \gets MaxLastSeqN(MS)$\r
- \State $max'_p \gets \Call{CheckResize}{MS,th_p,max'_g,m'_p}$\r
- \State $need_p \gets \Call{CheckNeedSS}{MS,max'_g}$\r
- \State $DE_p \gets \Call{GetDEPairs}{KV,max'_p,need_p,sl_{last}}$\r
- \State $hmac_{c_p} \gets Hmac(DE_p,SK)$\r
- \State $Dat_p \gets CreateDat(s_p,id_{self},hmac_{p_p},DE_p,hmac_{c_p})$\r
- \State $hmac_{p_p} \gets hmac_{c_p}$\r
- \State $sv_p \gets Encrypt(Dat_p,SK)$\r
- \State $\tuple{stat_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$\r
- \State $cr_p \gets \Call{HandleCollision}{\tuple{stat_p,SL_p}}$\r
- \If{$need_p$}\r
- \State $cr_{p_{last}} \gets \Call{ReinsertLastSlot}{sl_{last},max'_p}$\r
- \EndIf\r
+ \State $success \gets false$\r
+ \While{$\neg success$}\r
+ \State $s_p \gets MaxLastSeqN(MS)$\r
+ \State $max'_p \gets \Call{CheckResize}{MS,th_p,max'_g,m'_p}$\r
+ \State $need_p \gets \Call{CheckNeedSS}{MS,max'_g}$\r
+ \State $DE_p \gets \Call{GetDEPairs}{KV,max'_p,need_p,sl_{last}}$\r
+ \State $hmac_{c_p} \gets Hmac(DE_p,SK)$\r
+ \State $Dat_p \gets CreateDat(s_p,id_{self},hmac_{p_p},DE_p,hmac_{c_p})$\r
+ \State $hmac_{p_p} \gets hmac_{c_p}$\r
+ \State $sv_p \gets Encrypt(Dat_p,SK)$\r
+ \State $\tuple{stat_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$\r
+ \State $success \gets stat_p$\r
+ \If{$\neg success$}\r
+ \State $cr_p \gets \Call{HandleCollision}{\tuple{stat_p,SL_p}}$\r
+ \EndIf\r
+ %\If{$need_p$}\r
+ % \State $\tuple{cr_{p_{last}},hmac_{p_p}} \gets \r
+ % \Call{ReinsertLastSlot}{MS,SK,sl_{last},max'_p,hmac_{p_p}}$\r
+ %\EndIf\r
+ \EndWhile\r
+ \State $MS \gets \Call{UpdateLastSeqN}{id_{self},s_p,MS}$\r
\EndProcedure\r
\end{algorithmic}\r
\r
\note{General comments... Work on structuring things to improve\r
readability... This include names of functions/variables, how\r
things are partitioned into functions, adding useful comments,...}\r
+ \r
+ \note{Also Missing liveness state definition in algorithm...}\r
\r
\r
\subsection{Definitions for Formal Guarantees}\r
\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
\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
projects / iotcloud.git / commitdiff