$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
-\r
\textbf{States} \\\r
\textit{$id_{self}$ = machine Id of this client} \\\r
\textit{$max_g$ = maximum number of slots (initially $max_g > 0$)} \\\r
\textit{DT = set of $\tuple{k,v}$ on client} \\\r
\textit{MS = associative array of $\tuple{id, s_{last}}$ of all clients on client \r
(initially empty)} \\\r
-\textit{$LV$ = live set of $de$ entries on client, contains \r
- $\tuple{de,s}$ entries} \\\r
+\textit{$LV$ = live set of $kv$ entries on client, contains \r
+ $\tuple{kv,s}$ entries} \\\r
+\textit{$SS_{live}$ = live set of $ss$ entries on client} \\\r
+\textit{$CR_{live}$ = live set of $cr$ entries on client} \\\r
\textit{$MS_g$ = set MS to save all $\tuple{id, s_{last}}$ pairs while\r
traversing DT after a request to server (initially empty)} \\\r
\textit{SK = Secret Key} \\\r
\textit{$SM$ = associative array of $\tuple{s, id}$ of all slots in a previous read\r
(initially empty)} \\ \\\r
-\r
\textbf{Helper Functions} \\\r
$MaxSlot(SL_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv}\r
\in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \geq s_s$ \\\r
$GetPrevHmac(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=hmac_p$ \\\r
$GetCurrHmac(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=hmac_c$ \\\r
$GetDatEnt(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=DE$ \\\r
+$GetLiveSS(SS_{live},ss_s)= ss$ \textit{such that} $ss \in SS_{live} \r
+\wedge \forall ss_s \in SS_{live}, ss = ss_s$ \\\r
+$GetLiveCR(CR_{live},cr_s)= cr$ \textit{such that} $cr \in CR_{live} \r
+\wedge \forall cr_s \in CR_{live}, cr = cr_s$ \\\r
$GetLivEntLastS(LV_s,de_s)= s$ \textit{such that} $\tuple{de, s} \in LV_s \r
\wedge \forall \tuple{de_s, s_s} \in LV_s, de_s = de$ \\\r
-$GetKV($key-value data entry$)=\tuple{k_s,v_s}$ \\\r
-$GetSS($slot-sequence data entry$)=\tuple{id,s_{last}}$ \\\r
+$GetKV($key-value data entry$)=\tuple{k_s,v_s} = kv_s$ \\\r
+$GetSS($slot-sequence data entry$)=\tuple{id_s,s_{s_{last}}} = ss_s$ \\\r
$GetQS($queue-state data entry$)=qs_s$ \\\r
-$GetCR($collision-resolution data entry$)=\tuple{s_s,id_s}$ \\\r
+$GetCR($collision-resolution data entry$)=\tuple{s_s,id_s} = cr_s$ \\\r
$GetS(\tuple{s, id})=s$ \\\r
$GetId(\tuple{s, id})=id$ \\\r
$GetKey(\tuple{k, v})=k$ \\\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{UpdateSSLivEnt}{$LV_s,MS_s,de_s$}\r
-\State $s_t \gets GetLivEntLastS(LV_s,de_s)$\r
-\If{$s_t = \emptyset$}\r
- \State $LV_s \gets LV_s \cup \{\tuple{de_s,s_s}\}$\Comment{First occurrence}\r
+\Function{AddSSLivEnt}{$SS_{s_{live}},de_s$}\r
+\State $ss_s \gets GetSS(de_s)$\r
+\State $ss_t \gets GetLiveSS(SS_{s_{live}},ss_s)$\r
+\If{$ss_t = \emptyset$}\r
+ \State $SS_{s_{live}} \gets SS_{s_{live}} \cup \{ss_s\}$\Comment{First occurrence}\r
\EndIf\r
-\State $\tuple{id_s,s_{s_{last}}} \gets GetSS(de_s)$\r
-\State $s_t \gets MS_s[id_s]$\r
-\If{$s_t > s_{s_{last}}$}\Comment{Remove if dead}\r
- \State $LV_s \gets LV_s - \{\tuple{de_s,s_{s_{last}}}\}$ \r
-\EndIf\r
-\State \Return{$LV_s$}\r
+\State \Return{$SS_{s_{live}}$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{UpdateCRLivEnt}{$LV_s,MS_s,de_s$}\r
-\State $s_t \gets GetLivEntLastS(LV_s,de_s)$\r
-\If{$s_t = \emptyset$}\r
- \State $LV_s \gets LV_s \cup \{\tuple{de_s,s_s}\}$\Comment{First occurrence}\r
+\Function{AddCRLivEnt}{$CR_{s_{live}},de_s$}\r
+\State $cr_s \gets GetCR(de_s)$\r
+\State $cr_t \gets GetLiveCR(CR_{s_{live}},cr_s)$\r
+\If{$cr_t = \emptyset$}\r
+ \State $CR_{s_{live}} \gets CR_{s_{live}} \cup \{cr_s\}$\Comment{First occurrence}\r
\EndIf\r
-\State $\tuple{s_s,id_s} \gets GetCR(de_s)$\r
-\State $s_t \gets MinLastSeqN(MS_s)$\r
-\If{$s_t > s_s$}\Comment{Remove if dead}\r
- \State $LV_s \gets LV_s - \{\tuple{de_s,s_s}\}$ \r
-\EndIf\r
-\State \Return{$LV_s$}\r
+\State \Return{$CR_{s_{live}}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{UpdateSSLivEnt}{$SS_{s_{live}},MS_s$}\r
+\State $s_{s_{min}} \gets MinLastSeqN(MS_s)$\r
+\ForAll{$ss_s \in SS_{s_{live}}$}\r
+ \State $\tuple{id_s,s_{s_{last}}} \gets GetSS(ss_s)$\r
+ \If{$s_{s_{min}} > s_{s_{last}}$}\Comment{Remove if dead}\r
+ \State $SS_{s_{live}} \gets SS_{s_{live}} - \{\tuple{id_s,s_{s_{last}}}\}$ \r
+ \EndIf\r
+\EndFor\r
+\State \Return{$SS_{s_{live}}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{UpdateCRLivEnt}{$CR_{s_{live}},MS_s$}\r
+\State $s_{s_{min}} \gets MinLastSeqN(MS_s)$\r
+\ForAll{$cr_s \in CR_{s_{live}}$}\r
+ \State $\tuple{s_s,id_s} \gets GetCR(cr_s)$\r
+ \If{$s_{s_{min}} > s_s$}\Comment{Remove if dead}\r
+ \State $SS_{s_{live}} \gets SS_{s_{live}} - \{\tuple{s_s,id_s}\}$ \r
+ \EndIf\r
+\EndFor\r
+\State \Return{$CR_{s_{live}}$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\ForAll{$de_{g_{ss}} \in DE_{g_{ss}}$}\r
\State $\tuple{id_d,s_{d_{last}}} \gets GetSS(de_{g_{ss}})$\r
\State $MS_g \gets \Call{UpdateLastSeqN}{id_d,s_{d_{last}},MS_g}$\r
- \State $LV \gets \Call{UpdateSSLivEnt}{LV,MS,de_{g_{ss}}}$\r
+ \State $SS_{live} \gets \Call{AddSSLivEnt}{SS_{live},de_{g_{ss}}}$\r
\EndFor\r
\EndIf\r
\State $DE_{g_{cr}} \gets \Call{GetColRes}{DE_g}$\Comment{Handle cr}\r
\ForAll{$de_{g_{cr}} \in DE_{g_{cr}}$}\r
\State $\tuple{s_e,id_e} \gets GetCR(de_{g_{cr}})$\r
\State $\Call{CheckCollision}{MS,SM,\tuple{s_e,id_e}}$\r
- \State $LV \gets \Call{UpdateCRLivEnt}{LV,MS,de_{g_{cr}}}$\r
+ \State $CR_{live} \gets \Call{AddCRLivEnt}{SS_{live},de_{g_{cr}}}$\r
\EndFor\r
\EndIf\r
\State $sl_{last} \gets \Call{StoreLastSlot}{MS,sl_{last},s_g,sv_g,id_g}$\r
\State \Call{Error}{'Actual queue size exceeds $max_g$'}\r
\EndIf\r
\State $\Call{CheckLastSeqN}{MS_g,MS}$\r
+\State $\Call{UpdateSSLivEnt}{SS_{live},MS}$\r
+\State $\Call{UpdateCRLivEnt}{CR_{live},MS}$\r
\EndProcedure\r
\end{algorithmic}\r
\r
collision in reinserting the last slot (sent in the following slot)} \\\r
\textit{$ck_p$ = counter of $kv \in KV$ for putting pairs (initially 0)} \\\r
\textit{$ck_g$ = counter of $kv \in KV$ for getting pairs (initially 0)} \\\r
+\textit{$cs_p$ = counter of $ss \in SS$ for putting pairs (initially 0)} \\\r
+\textit{$cs_g$ = counter of $ss \in SS$ for getting pairs (initially 0)} \\\r
+\textit{$cc_p$ = counter of $cr \in CR$ for putting pairs (initially 0)} \\\r
+\textit{$cc_g$ = counter of $cr \in CR$ for getting pairs (initially 0)} \\\r
\textit{$hmac_{c_p}$ = the HMAC value of the current slot} \\\r
\textit{$hmac_{p_p}$ = the HMAC value of the previous slot \r
($hmac_{p_p} = \emptyset$ for the first slot)} \\\r
\textit{$m'_p$ = offset added to $max$ for resize} \\\r
\textit{$reinsert_{qs}$ = boolean to decide $qs$($max_g$) reinsertion} \\\r
\textit{$KV$ = set of $\tuple{ck, \tuple{k,v}}$ of kv entries on client} \\\r
-%\textit{$LV_{kv}$ = live set of $kv$ entries on client, contains a few \r
-% $\tuple{kv,s_{last}}$ entries} \\\r
-%\textit{$LV_{ss}$ = live set of $ss$ entries on client, contains a few \r
-% $\tuple{ss,s_{last}}$ entries} \\\r
-%\textit{$LV_{cr}$ = live set of $cr$ entries on client, contains a few \r
-% $\tuple{cr,s_{last}}$ entries} \\\r
+\textit{$SS$ = set of $\tuple{cs, \tuple{id,s_{last}}}$ of ss entries on client} \\\r
+\textit{$CR$ = set of $\tuple{cc, \tuple{s_{col},id_{col}}}$ of cr entries on client} \\\r
\textit{$SL_p$ = set of returned slots on client} \\\r
-\textit{SK = Secret Key} \\\r
-\textit{$CR$ = set of $cr$ entries on client} \\ \\\r
-\textit{$SS$ = set of $ss$ entries on client} \\ \\\r
+\textit{SK = Secret Key} \\ \\\r
\textbf{Helper Functions} \\\r
$CreateDat(s,id,hmac_p,DE,hmac_c)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
-$CreateCR(s,id)=\tuple{s,id}$ \\\r
-$CreateQS(max')=qs$ \\\r
-$CreateSS(id,s_{last})=\tuple{id,s_{last}}$ \\\r
+$CreateSS(id_s,s_{s_{last}})=\tuple{id_s,s_{s_{last}}} = ss_s$ \\\r
+$CreateQS(max'_s)=qs_s$ \\\r
+$CreateCR(s_s,id_s)=\tuple{s_s,id_s} = cr_s$ \\\r
$Encrypt(Dat_s,SK_s)=sv_s$ \\\r
-$GetStatus(\tuple{status,SL})=status$ \\\r
-$GetSL(\tuple{status,SL})=SL$ \\\r
$GetLastS(sl = \tuple{s,sv,id})=s$ \\\r
$GetSV(sl = \tuple{s,sv,id})=sv$ \\\r
$GetID(sl = \tuple{s,sv,id})=id$ \\\r
$GetKVPair(KV_s,k_s)= \tuple{ck,\tuple{k, v}}$ \textit{such that} \r
$\tuple{ck,\tuple{k, v}} \in KV_s \wedge\r
\forall \tuple{ck_s,\tuple{k_s, v_s}} \in KV_s, k = k_s$ \\\r
-%$GetKVLastSeqN(LV_{kv},kv_s)= s_{last}$ \textit{such that} $\tuple{kv, s_{last}} \in LV_{kv} \r
-%\wedge \forall \tuple{kv_s, s_{s_{last}}} \in LV_{kv}, s_{last} \geq s_{s_{last}}$ \\\r
-%$GetSSLastSeqN(LV_{ss},ss_s)= s_{last}$ \textit{such that} $\tuple{ss, s_{last}} \in LV_{ss} \r
-%\wedge \forall \tuple{ss_s, s_{s_{last}}} \in LV_{ss}, s_{last} \geq s_{s_{last}}$ \\\r
-%$GetCRLastSeqN(LV_{cr},cr_s)= s_{last}$ \textit{such that} $\tuple{cr, s_{last}} \in LV_{cr} \r
-%\wedge \forall \tuple{cr_s, s_{s_{last}}} \in LV_{cr}, s_{last} \geq s_{s_{last}}$ \\\r
\r
\begin{algorithmic}[1]\r
\Function{PutKVPair}{$KV_s,\tuple{k_s,v_s}$}\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{HandleCollision}{$SL_s$}\r
+\Function{HandleCollision}{$SL_s,s_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 $cr_s \gets CreateCR(s_{col},id_{col})$\r
\State $\Call{ProcessSL}{SL_s}$\r
\State \Return{$cr_s$}\r
\EndFunction\r
\If{$de_s = kv$}\r
\State $\tuple{k_s,v_s} \gets GetKV(de_s)$\r
\State $KV \gets \Call{PutKVPair}{KV,\tuple{k_s,v_s}}$\r
- \EndIf\r
- \If{$de_s = ss$}\r
- \State $ss_s \gets GetSS(de_s)$\r
- \State $SS \gets SS \cup ss_s$\r
- \EndIf\r
- \If{$de_s = qs$}\r
+ \ElsIf{$de_s = ss$}\r
+ \State $\tuple{id_s,s_{s_{last}}} \gets GetSS(de_s)$\r
+ \State $SS \gets \Call{PutSSPair}{SS,\tuple{id_s,s_{s_{last}}}}$\r
+ \ElsIf{$de_s = cr$}\r
+ \State $\tuple{s_s,id_s} \gets GetCR(de_s)$\r
+ \State $CR \gets \Call{PutCRPair}{CR,\tuple{s_s,id_s}}$\r
+ \ElsIf{$de_s = qs$}\r
\State $reinsert_{qs} \gets true$\r
\EndIf\r
- \If{$de_s = cr$}\r
- \State $cr_s \gets GetCR(de_s)$\r
- \State $CR \gets CR \cup cr_s$\r
- \EndIf\r
\EndIf\r
\EndFor\r
\EndProcedure\r
\begin{algorithmic}[1]\r
\Function{CheckLiveness}{$s_s,de_s$}\r
\State $live \gets true$\r
-\If{$de_s = kv \lor de_s = ss \lor de_s = cr$}\r
+\If{$de_s = kv$}\r
\State $s_l \gets GetLivEntLastS(LV,de_s)$\r
\If{$s_l = \emptyset \lor s_s < s_l$}\r
\State $live \gets false$\r
\EndIf\r
+\ElsIf{$de_s = ss$}\r
+ \State $ss_s \gets GetSS(de_s)$\r
+ \State $ss_l \gets GetLiveSS(SS_{live},ss_s)$\r
+ \If{$ss_l = \emptyset$}\r
+ \State $live \gets false$\r
+ \EndIf\r
+\ElsIf{$de_s = cr$}\r
+ \State $cr_s \gets GetCR(de_s)$\r
+ \State $cr_l \gets GetLiveCR(CR_{live},cr_s)$\r
+ \If{$cr_l = \emptyset$}\r
+ \State $live \gets false$\r
+ \EndIf\r
\ElsIf{$de_s = qs$}\r
\State $qs_s \gets GetQS(de_s)$\r
\If{$qs_s \neq max_g$}\r
\EndFunction\r
\end{algorithmic}\r
\r
+%\begin{algorithmic}[1]\r
+%\Function{AddSlotSeq}{$DE_s,SS_s,cp_s$}\Comment{Insert a $ss$}\r
+%\State $DE_{ret} \gets DE_s \cup SS_s$\r
+%\State $cp_s \gets cp_s - |SS_s|$\r
+%\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+%\EndFunction\r
+%\end{algorithmic}\r
+\r
\begin{algorithmic}[1]\r
-\Function{AddSlotSeq}{$DE_s,SS_s,cp_s$}\Comment{Insert a $ss$}\r
-\State $DE_{ret} \gets DE_s \cup SS_s$\r
-\State $cp_s \gets cp_s - |SS_s|$\r
-\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+\Function{PutSSPair}{$SS_s,\tuple{id_s,s_{s_{last}}}$}\Comment{Insert a set of $ss$ entries}\r
+\State $SS_s \gets SS_s \cup \{\tuple{cs_p, \tuple{id_s,s_{s_{last}}}}\}$\r
+\State $cs_p \gets cs_p + 1$\r
+\State \Return{$SS_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{PutCRPair}{$CR_s,\tuple{s_s,id_s}$}\Comment{Insert a set of $cr$ entries}\r
+\State $CR_s \gets CR_s \cup \{\tuple{cc_p, \tuple{s_s,id_s}}\}$\r
+\State $cc_p \gets cc_p + 1$\r
+\State \Return{$CR_s$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\EndFunction\r
\end{algorithmic}\r
\r
+%\begin{algorithmic}[1]\r
+%\Function{AddColRes}{$DE_s,CR_s,cp_s$}\Comment{Insert a $cr$}\r
+%\State $DE_{ret} \gets \emptyset$\r
+%\State $DE_{ret} \gets DE_s \cup CR_s$\r
+%\State $cp_s \gets cp_s - |CR_s|$\r
+%\State \Return{$\tuple{DE_{ret},cp_s}$}\r
+%\EndFunction\r
+%\end{algorithmic}\r
+\r
\begin{algorithmic}[1]\r
-\Function{AddColRes}{$DE_s,CR_s,cp_s$}\Comment{Insert a $cr$}\r
+\Function{GetKVPairs}{$DE_s,KV_s,cp_s$}\r
\State $DE_{ret} \gets \emptyset$\r
-\State $DE_{ret} \gets DE_s \cup CR_s$\r
-\State $cp_s \gets cp_s - |CR_s|$\r
+\If{$|KV_s| \leq cp_s$}\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_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
+\EndIf\r
+\State \Return{$\tuple{DE_{ret}}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{GetSSPairs}{$DE_s,SS_s,cp_s$}\r
+\State $DE_{ret} \gets \emptyset$\r
+\If{$|SS_s| \leq cp_s$}\Comment{$SS$ set can span multiple slots}\r
+ \State $DE_{ret} \gets DE_s \cup\r
+ \{\tuple{id_s,s_{s_{last}}} \mid \tuple{cs_s,\tuple{id_s,s_{s_{last}}}} \in SS_s\}$\r
+\Else\r
+ \State $DE_{ret} \gets DE_s \cup\r
+ \{\tuple{id_s,s_{s_{last}}} \mid \tuple{cs_s,\tuple{id_s,s_{s_{last}}}} \in SS_s,\r
+ cs_g \leq cs_s < cs_g + cp_s\}$\r
+\EndIf\r
+\State $cp_s \gets cp_s - |SS_s|$\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
+\Function{GetCRPairs}{$DE_s,CR_s,cp_s$}\r
\State $DE_{ret} \gets \emptyset$\r
-\If{$|KV_s| \leq cp$}\Comment{$KV$ set can span multiple slots}\r
+\If{$|CR_s| \leq cp_s$}\Comment{$CR$ 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
+ \{\tuple{s_s,id_s} \mid \tuple{cc_s,\tuple{s_s,id_s}} \in CR_s\}$\r
\Else\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
+ \{\tuple{s_s,id_s} \mid \tuple{cc_s,\tuple{s_s,id_s}} \in CR_s,\r
+ cc_g \leq cc_s < cc_g + cp_s\}$\r
\EndIf\r
-\State \Return{$DE_{ret}$}\r
+\State $cp_s \gets cp_s - |CR_s|$\r
+\State \Return{$\tuple{DE_{ret},cp_s}$}\r
\EndFunction\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
\Procedure{PutDataEntries}{$th_p,m'_p$}\r
-\State $success \gets false$\r
+\State $success_p \gets false$\r
\State $CR_p \gets \emptyset$\r
-\While{$\neg success$}\r
+\While{$\neg success_p$}\r
\State $DE_p \gets \emptyset$\r
\State $s_p \gets MaxLastSeqN(MS)$\r
\State $cp_p \gets cp$\r
\State $reinsert_{qs} \gets false$\r
\EndIf\r
\EndIf\r
- \If{$SS \neq \emptyset$}\Comment{Reinsert $ss$ entries}\r
- %\State $\tuple{DE_p,cp_p} \gets \Call{ReinsertSS}{DE_p,SS,cp_p}$\r
- \State $\tuple{DE_p,cp_p} \gets \Call{AddSlotSeq}{DE_p,SS,cp_p}$\r
+ \If{$SS \neq \emptyset$}\Comment{Add $ss$ entries}\r
+ \State $\tuple{DE_p,cp_p} \gets \Call{GetSSPairs}{DE_p,SS,cp_p}$\r
\EndIf\r
\If{$CR \neq \emptyset$}\Comment{Add $cr$ entries}\r
- \State $\tuple{DE_p,cp_p} \gets \Call{AddColRes}{DE_p,CR,cp_p}$\r
+ \State $\tuple{DE_p,cp_p} \gets \Call{GetCRPairs}{DE_p,CR,cp_p}$\r
\EndIf\r
- %\State $need_p \gets \Call{CheckNeedSS}{MS,max_g}$\r
- %\If{$need_p$}\r
- % \State $\tuple{DE_p,cp_p} \gets \Call{AddSlotSeq}{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 $\tuple{DE_p,cp_p} \gets \Call{GetKVPairs}{DE_p,KV,cp_p}$\Comment{Add $kv$ entries}\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}{SL_p}$\r
- \State $CR_p \gets CR_p \cup cr_p$\r
+ \State $\tuple{success_p,SL_p} \gets \Call{PutSlot}{s_p,sv_p,max'_p}$\r
+ \If{$\neg success_p$}\r
+ \State $cr_p \gets \Call{HandleCollision}{SL_p,s_p}$\r
+ \State $\tuple{s_{p_{col}},id_{p_{col}}} \gets GetCR(cr_p)$\r
+ \State $CR \gets \Call{PutCRPair}{CR,\tuple{s_{p_{col}},id_{p_{col}}}}$\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
+\If{$|DE_p| = cp$}\Comment{Middle of set}\r
+ \State $ck_g \gets ck_g + cp_s$\r
+ \State $cs_g \gets cs_g + |SS|$\r
+ \State $cc_g \gets cc_g + |CR|$\r
+\Else\Comment{End of set}\r
+ \State $ck_g \gets 0$\r
+ \State $cs_g \gets 0$\r
+ \State $cc_g \gets 0$\r
\EndIf\r
\State $MS \gets \Call{UpdateLastSeqN}{id_{self},s_p,MS}$\r
-\State $SS \gets \emptyset$\r
-\State $CR \gets CR_p$\r
\State $need_p \gets \Call{CheckNeedSS}{MS,max_g}$\r
\If{$need_p$}\r
+ \State $\Call{CheckLastSlot}{sl_{last}}$\Comment{Get ready to expunge first slot}\r
\State $ss_p \gets \Call{CreateSlotSeq}{sl_{last}}$\r
- \State $SS \gets SS \cup ss_p$\Comment{Add ss}\r
- \State $\Call{CheckLastSlot}{sl_{last}}$\Comment{SL on server is full}\r
+ \State $\tuple{id_p,s_{p_{last}}} \gets GetSS(ss_p)$\r
+ \State $SS \gets \Call{PutSSPair}{SS,\tuple{id_p,s_{p_{last}}}}$\Comment{Add ss}\r
\EndIf\r
\EndProcedure\r
\end{algorithmic}\r
\r
-\note{Lots of problems with PutDataEntries: (1) What happens if lose network connectivity after adding the key value pair, but before reinserting the last slot? You probably need to create space first and then insert your data entry... (2) What if reinsertlastslot kicks something else important out? What if the server rejects our update because it is out of date? At the very least, any putdataentries function w/o a loop is wrong!}\r
+%\note{Lots of problems with PutDataEntries: (1) What happens if lose network connectivity after adding the key value pair, but before reinserting the last slot? You probably need to create space first and then insert your data entry... (2) What if reinsertlastslot kicks something else important out? What if the server rejects our update because it is out of date? At the very least, any putdataentries function w/o a loop is wrong!}\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
+%\note{General comments... Work on structuring things to improve readability... This include names of functions/variables, how things are partitioned into functions, adding useful comments,...}\r
\r
-\note{Also Missing liveness state definition in algorithm...}\r
+%\note{Also Missing liveness state definition in algorithm...}\r
\r
\r
\subsection{Definitions for Formal Guarantees}\r
\item Equality: Two messages $t$ and $u$ are equal if their sequence numbers, senders, and contents are exactly the same.\r
\item Message: A message $t$, is the tuple $t = (i(t), s(t), contents(t))$ containing the sequence number, machine ID of the sender, and contents of $t$ respectively.\r
\item Parent: A parent of a message $t$ is the message $A(t)$, unique by the correctness of HMACs, such that $HMAC_C(t) = HMAC_P(A(t))$.\r
- \item Partial message sequence: A partial message sequence is a sequence of messages, no two with the same sequence number, that can be divided into disjoint chains, where a chain of messages with length $n \ge 1$ is a message sequence $(t_i, t_{i+1}, ..., t_{i+n-1})$ such that for every index $i < k \le i+n-1$, $t_k$ has sequence number $k$ and is the parent of $t_{k-1}$.\r
+ \item Chain: A chain of messages with length $n \ge 1$ is a message sequence $R = (R_i, R_{i+1}, ..., R_{i+n-1})$ such that for every index $i < k \le i+n-1$, $R_k$ has sequence number $k$ and is the parent of $R_{k-1}$.\r
+ \item Partial message sequence: A partial message sequence is a sequence of messages, no two with the same sequence number, that can be divided into disjoint chains.\r
\item Total message sequence: A total message sequence $T$ with length $n$ is a chain of messages that starts at $i = 1$.\r
- \item Path: The path of a message $t$ is the total message sequence whose last message is $t$.\r
+ \item Path: The path of a message $t$ is the chain that starts at $i = 1$ and whose last message is $t$. The uniqueness of a path follows from the uniqueness of a parent.\r
\item Consistency: A partial message sequence $P$ is consistent with a total message sequence $T$ of length $n$ if for every message $p \in P$ with $i(p) < n$, $T_{i(p)} = p$. This implies that $\{p \in P | i(p) \le n\}$ is a subsequence of T.\r
\item Transitive closure set at index $n$: A set $\mathscr{S}$ of clients comprising a connected component of an undirected graph, where two clients are connected by an edge if they both received the same message $t$ with index $i(t) > n$.\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$; 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 messages 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
- Assume that $t$ is not in the path of $u$. Take $u$ to be the packet of smallest index for which this occurs, and $t$ be the packet with largest index for this $u$. We will prove that an error occurs upon receipt of $u$.\r
+ Assume that $t$ is not in the path of $u$. Take $u$ to be the packet of smallest index for which this occurs, and $t$ be the packet with greatest index for this $u$. We will prove that an error occurs upon receipt of $u$.\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
- \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 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
+ \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 $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
\r
\end{itemize}\r
\end{proof}\r
\r
+ \begin{lem} If there are two packets $t$ and $u$, with $i(t) <= i(u)$, such that $t$ is in the path of $u$, then for any message $p$ with $i(p) <= i(t)$, iff $p$ is in the path of $t$, it is in the path of $u$. \end{lem}\r
+ \r
+ \begin{proof}\r
+ If $i(t) = i(u)$ or $i(p) = i(t)$, then we are done, because the two relevant messages are the same.\r
+ \r
+ Reverse direction: The definition of $t$ being in the path of $u$ is the existence of a message sequence $(..., t, ..., u)$ such that each message except $u$ is the parent of the succeeding message. The path of $u$ must contain some message with index $i(p)$; because $p$ is in the path of $u$, this message is $p$ itself. The path of $t$ is then the prefix of this path ending at $t$, which clearly contains $p$.\r
+ \r
+ Forward direction: The path of $t$ is a substring of the path of $u$, so if the path of $t$ contains $p$, so does the path of $u$.\r
+ \end{proof}\r
+ \r
\begin{theorem}\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)$. \r
\r
- We subsequently 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) > n$ that $C_1$ shares with another client. Then let $T$ be the portion of the path of $u$ ending at index $n$ 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 clients $\mathscr{C} = (C_1, C_2, ..., D)$ from $C_1$ to $D$, where each shares an edge with the next.\r
+ \r
+ We prove by induction that $P_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
+ \item Base case: $P_{C_1}$ includes $u$, whose path includes $t$.\r
+ \r
+ \item Inductive step: Each client in $\mathscr{C}$ has a partial message sequence with a message that includes $t$ if the previous client does. 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) > n$. By Lemma 1, $w$ or $x$, whichever has the least sequence number, is in the path of the other, and therefore by Lemma 2, $t$ is in the path of $x$.\r
+ \r
+ \item Let $z$ be 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 $z$. Since $t$ is in the path of $z$, every message in $P_D$ with smaller index than $i(t)$ is in $T$. Therefore, $P_D$ is consistent with $T$.\r
+ \r
\end{itemize}\r
\end{proof}\r
\r
projects / iotcloud.git / commitdiff