\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{HandleCollision}{$\tuple{stat_s,SL_s}$}\r
-\State $stat_s \gets GetStatus(\tuple{stat_s,SL_s})$\r
-\State $SL_s \gets GetSL(\tuple{stat_s,SL_s})$\r
-\If{$\neg stat_s$}\Comment{Handle collision}\r
- \State $\tuple{s_{col},sv_{col}} \gets GetColSeqN(SL_s,s_s)$\r
- \State $s_{col} \gets SeqN(\tuple{s_{col},sv_{col}})$\r
- \State $sv_{col} \gets SlotVal(\tuple{s_{col},sv_{col}})$\r
- \State $Dat_{col} \gets Decrypt(SK,sv_{col})$\r
- \State $id_{col} \gets GetMacId(Dat_{col})$\r
- \State $\tuple{s_{col},id_{col}} \gets CreateCR(s_{col},id_{col})$\r
- \State $cr_s \gets \tuple{s_{col},id_{col}}$\r
-\Else\r
- \State $cr_s \gets \emptyset$\r
-\EndIf\r
+\Function{HandleCollision}{$SL_s$}\r
+\State $\tuple{s_{col},sv_{col}} \gets GetColSeqN(SL_s,s_s)$\r
+\State $Dat_{col} \gets Decrypt(SK,sv_{col})$\r
+\State $id_{col} \gets GetMacId(Dat_{col})$\r
+\State $\tuple{s_{col},id_{col}} \gets CreateCR(s_{col},id_{col})$\r
+\State $cr_s \gets \tuple{s_{col},id_{col}}$\r
\State $\Call{ProcessSL}{SL_s}$\r
\State \Return{$cr_s$}\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
+\begin{algorithmic}[1]\r
+\Function{AddSlotSeq}{$DE_s,sl_s,cp_s$}\Comment{Insert a $ss$}\r
+\State $DE_{ret} \gets \emptyset$\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_s \cup ss_s$\r
+\State $cp_s \gets cp_s - 1$\r
+\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+\EndFunction\r
+\end{algorithmic}\r
\r
+\begin{algorithmic}[1]\r
+\Function{AddQueSta}{$DE_s,max'_s,cp_s$}\Comment{Insert a $qs$}\r
+\State $DE_{ret} \gets \emptyset$\r
+\State $qs_s \gets max'_s$\r
+\State $DE_{ret} \gets DE_s \cup qs_s$\r
+\State $cp_s \gets cp_s - 1$\r
+\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+\EndFunction\r
+\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{GetDEPairs}{$KV_s,max'_s,need_s,sl_s$}\r
+\Function{AddCollRes}{$DE_s,cr_p,cp_s$}\Comment{Insert a $cr$}\r
\State $DE_{ret} \gets \emptyset$\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 $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 $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 $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
+\State $DE_{ret} \gets DE_s \cup cr_p$\r
+\State $cp_s \gets cp_s - 1$\r
+\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{GetKVPairs}{$DE_s,KV_s,cp_s$}\r
+\State $DE_{ret} \gets \emptyset$\r
+\If{$|KV_s| \leq cp$}\Comment{$KV$ set can span multiple slots}\r
+ \State $DE_{ret} \gets DE_s \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
+ \State $DE_{ret} \gets DE_s \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 + 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
\EndIf\r
\State \Return{$DE_{ret}$}\r
\EndFunction\r
\Procedure{PutDataEntries}{$th_p,m'_p$}\r
\State $success \gets false$\r
\While{$\neg success$}\r
+ \State $DE_p \gets \emptyset$\r
\State $s_p \gets MaxLastSeqN(MS)$\r
+ \State $cp_p \gets cp$\r
\State $max'_p \gets \Call{CheckResize}{MS,th_p,max'_g,m'_p}$\r
+ \If{$max'_p \neq \emptyset$}\r
+ \State $\tuple{DE_p,cp_p} \gets \Call{AddQueueState}{DE_p,max'_p,cp_p}$\Comment{Add qs}\r
+ \EndIf\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
+ \If{$need_p$}\r
+ \State $\tuple{DE_p,cp_p} \gets \Call{AddSlotSequence}{DE_p,sl_{last},cp_p}$\Comment{Add ss}\r
+ \EndIf\r
+ \State $DE_p \gets \Call{GetKVPairs}{DE_p,KV,cp_p}$\Comment{Add kv pairs}\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 $\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
+ \State $cr_p \gets \Call{HandleCollision}{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
+\If{$|DE_p| = cp$}\Comment{Check and advance $ck_g$}\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
\State $MS \gets \Call{UpdateLastSeqN}{id_{self},s_p,MS}$\r
\EndProcedure\r
\end{algorithmic}\r
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}\r
\r
\begin{proof}\r
-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) > i$ that $C_1$ shares with another client. Then let $T$ be the portion of the path of $u$ ending at index $i$ 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 edges from $C_1$ to $D$. Call this $\mathscr{C} = (C_1, C_2, ..., D)$. I will prove by induction that $D$ has a message whose path includes $t$.\r
+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) > i$ that $C_1$ shares with another client. Then let $T$ be the portion of the path of $u$ ending at index $i$ 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 edges from $C_1$ to $D$. Call this $\mathscr{C} = (C_1, C_2, ..., D)$. \r
\r
-For the base case, $P_{C_1}$ includes $u$, whose path includes $t$. For the inductive step, suppose $P_{C_k}$ has an message $w$ with a path that includes $t$, and shares message $x$ with $P_{C_{k+1}}$ such that $i(x) > i$. If $i(w) = i(x)$, then $w = x$. If $i(w) < i(x)$, then, by Lemma 1, $w$ is in the path of $x$. If $i(w) > i(x)$, $x$ is in the path of $w$; note again that its index is greater than $i$. In any case, $t$ is in the path of $u_k+1$.\r
-\r
-Let $w$ 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 $w$. Since $t$ is in the path of $w$, every message in $P_D$ with smaller index than $i(t)$ is in $T$. Therefore, $P_D$ is consistent with $T$.\r
+We subsequently prove by induction that $D$ has a message whose path includes $t$.\r
+\begin{itemize}\r
+\item For the base case, $P_{C_1}$ includes $u$, whose path includes $t$. \r
+\item For the inductive step, 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) > i$. If $i(w) = i(x)$, then $w = x$. If $i(w) < i(x)$, then, by Lemma 1, $w$ is in the path of $x$. If $i(w) > i(x)$, $x$ is in the path of $w$; note again that its index is greater than $i$. In any case, $t$ is in the path of $u_k+1$.\r
+\item Let $w$ 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 $w$. Since $t$ is in the path of $w$, every message in $P_D$ with smaller index than $i(t)$ is in $T$. Therefore, $P_D$ is consistent with $T$.\r
+\end{itemize}\r
\end{proof}\r
\r
\subsection{Future Work}\r
projects / iotcloud.git / commitdiff