\end{algorithmic}\r
\r
\subsection{Client Algorithm}\r
+\subsubsection{Reading Slots}\r
\textbf{Data Entry} \\\r
$de$ is a data entry \\\r
$k$ is key of entry \\\r
\textit{DT = set of $\tuple{k,v}$ on client} \\\r
\textit{MS = set of $\tuple{id, s_{last}}$ of all clients on client \r
(initially empty)} \\\r
-\textit{$MS_c$ = set MS to save all $\tuple{id, s_{last}}$ pairs while\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{$SM$ = set of $\tuple{s, id}$ of all slots in a previous read\r
(initially empty)} \\\r
-\textit{$max_c$ = maximum number of slots (initially $max_c > 0$)} \\\r
+\textit{$max_g$ = maximum number of slots (initially $max_c > 0$)} \\\r
\textit{m = number of slots on client (initially $m = 0 and m \leq n$)} \\\r
-\textit{$hmac_p$ = the HMAC value of the previous slot ($hmac_p = \emptyset$ \r
-for the first slot)} \\\r
+\textit{$hmac_{p_g}$ = the HMAC value of the previous slot \r
+($hmac_{p_g} = \emptyset$ for the first slot)} \\\r
\textit{$id_{self}$ = machine Id of this client} \\\r
\textit{SK = Secret Key} \\ \\\r
\textbf{Helper Functions} \\\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{ValidHmac}{$Dat_s,SK_s$}\r
-\State $hmac_{stored} \gets GetCurrHmac(Dat_s)$\r
-\State $hmac_{computed} \gets Hmac(Dat_s,SK_s)$\r
+\Function{ValidHmac}{$DE_s,SK_s,hmac_{stored}$}\r
+\State $hmac_{computed} \gets Hmac(DE_s,SK_s)$\r
\If{$hmac_{stored} = hmac_{computed}$}\r
\State $valid \gets true$\r
\Else\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{ValidPrevHmac}{$Dat_s,hmac_{p_s}$}\r
+\Function{ValidPrevHmac}{$DE_s,hmac_{p_s},hmac_{p_{sto}}$}\r
\If{$hmac_{p_s} = \emptyset$}\Comment{First slot - no previous HMAC}\r
\State $valid \gets true$\r
\Else\r
- \State $hmac_{stored} \gets GetPrevHmac(Dat_s)$\r
- \If{$hmac_{stored} = hmac_{p_s}$}\r
+ \If{$hmac_{p_{sto}} = hmac_{p_s}$}\r
\State $valid \gets true$\r
\Else\r
\State $valid \gets false$\r
\r
\begin{algorithmic}[1]\r
\Function{GetQueSta}{$Dat_s$}\r
-\State $DE_s \gets GetDatEnt(Dat_s)$\r
+\State $DE_s \gets GetDatEnt(DE_s)$\r
\State $de_{qs} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
de_s \in D \land de_s = qs$\r
\If{$de_{qs} \neq \emptyset$}\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
-\Function{GetKVPairs}{$s$}\r
-\State $SL_c \gets \Call{GetSlot}{s}$\r
-\State $MS_c \gets \emptyset$\r
+\Procedure{ProcessSL}{$SL_g$}\r
+\State $MS_g \gets \emptyset$\r
\State $SM_{curr} \gets \emptyset$\r
-\State $\tuple{s_{c_{max}},sv_{c_{max}}} \gets MaxSlot(SL_c)$\r
-\State $s_{c_{max}} \gets SeqN(\tuple{s_{c_{max}},sv_{c_{max}}})$\r
-\State $\tuple{s_{c_{min}},sv_{c_{min}}} \gets MinSlot(SL_c)$\r
-\State $s_{c_{min}} \gets SeqN(\tuple{s_{c_{min}},sv_{c_{min}}})$\r
-\For{$s_c \gets s_{c_{min}}$ \textbf{to} $s_{c_{max}}$}\Comment{Process slots \r
- in $SL_c$ in order}\r
- \State $\tuple{s_c,sv_c} \gets Slot(SL_c,s_c)$\r
- \State $SM_{curr} \gets SM_{curr} \cup \{\tuple{s_c,sv_c}\}$\r
- \State $s_c \gets SeqN(\tuple{s_c,sv_c})$\r
- \State $sv_c \gets SlotVal(\tuple{s_c,sv_c})$\r
- \State $Dat_c \gets Decrypt(SK,sv_c)$\r
- \State $s_{c_{in}} \gets GetSeqN(Dat_c)$\r
- \If{$s_c \neq s_{c_{in}}$}\r
+\State $\tuple{s_{g_{max}},sv_{g_{max}}} \gets MaxSlot(SL_g)$\r
+\State $s_{g_{max}} \gets SeqN(\tuple{s_{g_{max}},sv_{g_{max}}})$\r
+\State $\tuple{s_{g_{min}},sv_{g_{min}}} \gets MinSlot(SL_g)$\r
+\State $s_{g_{min}} \gets SeqN(\tuple{s_{g_{min}},sv_{g_{min}}})$\r
+\For{$s_g \gets s_{g_{min}}$ \textbf{to} $s_{g_{max}}$}\Comment{Process slots \r
+ in $SL_g$ in order}\r
+ \State $\tuple{s_g,sv_g} \gets Slot(SL_g,s_g)$\r
+ \State $SM_{curr} \gets SM_{curr} \cup \{\tuple{s_g,sv_g}\}$\r
+ \State $s_g \gets SeqN(\tuple{s_g,sv_g})$\r
+ \State $sv_g \gets SlotVal(\tuple{s_g,sv_g})$\r
+ \State $Dat_g \gets Decrypt(SK,sv_g)$\r
+ \State $s_{g_{in}} \gets GetSeqN(Dat_g)$\r
+ \If{$s_g \neq s_{g_{in}}$}\r
\State \Call{ReportError}{'Invalid sequence number'}\r
\EndIf\r
- \If{$\neg \Call{ValidPrevHmac}{Dat_c,hmac_p}$}\r
+ \State $DE_g \gets GetDatEnt(Dat_g)$\r
+ \State $hmac_{p_{stored}} \gets GetPrevHmac(Dat_g)$\r
+ \If{$\neg \Call{ValidPrevHmac}{DE_g,hmac_{p_g},hmac_{p_{stored}}}$}\r
\State \Call{ReportError}{'Invalid previous HMAC value'}\r
\EndIf\r
- \If{$\neg \Call{ValidHmac}{Dat_c,SK}$}\r
+ \State $hmac_{c_g} \gets GetCurrHmac(Dat_g)$\r
+ \If{$\neg \Call{ValidHmac}{DE_g,SK,hmac_{c_g}}$}\r
\State \Call{ReportError}{'Invalid current HMAC value'}\r
\EndIf\r
- \State $hmac_p \gets Hmac(Dat_c,SK)$\Comment{Update $hmac_p$ for next slot check}\r
- \State $qs_c \gets \Call{GetQueSta}{Dat_c}$\Comment{Handle qs}\r
- \If{$qs_c \neq \emptyset \land qs_c > max_c$}\r
- \State $max_c \gets qs_c$\r
+ \State $hmac_{p_g} \gets Hmac(Dat_g,SK)$\Comment{Update $hmac_{p_g}$ for next check}\r
+ \State $qs_g \gets \Call{GetQueSta}{Dat_g}$\Comment{Handle qs}\r
+ \If{$qs_g \neq \emptyset \land qs_g > max_g$}\r
+ \State $max_g \gets qs_g$\r
\EndIf\r
%Check for last s in Dat\r
- \State $id_c \gets GetMacId(Dat_c)$\Comment{Handle last s}\r
- \State $MS_c \gets \Call{UpdateLastSeqN}{id_c,s_c,MS_c}$\r
+ \State $id_g \gets GetMacId(Dat_g)$\Comment{Handle last s}\r
+ \State $MS_g \gets \Call{UpdateLastSeqN}{id_g,s_g,MS_g}$\r
%Check for last s in DE in Dat\r
- \State $\tuple{id_d,s_{d_{last}}} \gets \Call{GetSlotSeq}{Dat_c}$\Comment{Handle ss}\r
+ \State $\tuple{id_d,s_{d_{last}}} \gets \Call{GetSlotSeq}{Dat_g}$\Comment{Handle ss}\r
\If{$\tuple{id_d,s_{d_{last}}} \neq \emptyset$}\r
- \State $MS_c \gets \Call{UpdateLastSeqN}{id_d,s_{d_{last}},MS_c}$\r
+ \State $MS_g \gets \Call{UpdateLastSeqN}{id_d,s_{d_{last}},MS_g}$\r
\EndIf\r
\State $\tuple{s_e,id_e} \gets \r
- \Call{GetColRes}{Dat_c}$\Comment{Handle cr}\r
+ \Call{GetColRes}{Dat_g}$\Comment{Handle cr}\r
\If{$\tuple{s_e,id_e} \neq \emptyset$}\r
\State $s_e \gets GetS(\tuple{s_e,id_e})$\r
\State $id_e \gets GetId(\tuple{s_e,id_e})$\r
\State $\Call{CheckColRes}{SM,\tuple{s_e,id_e}}$\r
\EndIf\r
\EndIf\r
- \State $DT \gets \Call{UpdateDT}{DT,Dat_c}$\r
+ \State $DT \gets \Call{UpdateDT}{DT,Dat_g}$\r
\EndFor\r
\State $SM \gets SM_{curr}$\r
-\If{$m + |SL_c| \leq max_c$}\Comment{Check actual size against $max_c$}\r
- \State $m \gets m + |SL_c|$\r
+\If{$m + |SL_g| \leq max_g$}\Comment{Check actual size against $max_g$}\r
+ \State $m \gets m + |SL_g|$\r
\Else\r
- \State \Call{ReportError}{'Actual queue size exceeds $max_c$'}\r
+ \State \Call{ReportError}{'Actual queue size exceeds $max_g$'}\r
\EndIf\r
-\State $\Call{CheckLastSeqN}{MS_c,MS}$\r
-\State \Return{$DT$}\r
-\EndFunction\r
+\State $\Call{CheckLastSeqN}{MS_g,MS}$\r
+\EndProcedure\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Procedure{GetKVPairs}{}\r
+\State $s_g \gets GetLastSeqN(MS,id_{self}) + 1$\r
+\State $SL_c \gets \Call{GetSlot}{s_g}$\r
+\State $\Call{ProcessSL}{SL_c}$\Comment{Process slots and update DT}\r
+\EndProcedure\r
\end{algorithmic}\r
\r
\begin{algorithmic}[1]\r
\EndFunction\r
\end{algorithmic}\r
\r
+\subsubsection{Writing Slots}\r
+\textbf{Data Entry} \\\r
+$k$ is key of entry \\\r
+$v$ is value of entry \\\r
+$kv$ is a key-value entry $\tuple{k,v}$\\\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
+\r
+\textbf{States} \\\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{$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{$id_{self}$ = machine Id of this client} \\\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{$KV$ = set of $\tuple{ck, \tuple{k,v}}$ of kv entries on client} \\\r
+\textit{$ST$ = set of $DE$ objects on client} \\\r
+\textit{$SL_p$ = set of returned slots on client} \\\r
+\textit{SK = Secret Key} \\\r
+\r
+\textbf{Helper Functions} \\\r
+$CreateDat(s,id,hmac_p,DE,hmac_c)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
+$Encrypt(Dat_s,SK_s)=sv_s$ \\\r
+$GetStatus(\tuple{status,SL})=status$ \\\r
+$GetSL(\tuple{status,SL})=SL$ \\\r
+$GetColSeqN(SL_s,s_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 = s_s$ \\\r
+$CreateCR(s,id)=\tuple{s,id}$ \\\r
+$GetKV(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
+$MaxLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s \r
+\wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, s_{last} \geq s_{s_{last}}$ \\\r
+\r
+\begin{algorithmic}[1]\r
+\Function{PutKVPair}{$KV_s,\tuple{k_s,v_s}$}\r
+\State $k_s \gets GetKey(\tuple{k_s,v_s})$\r
+\State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKV(KV_s,k_s)$\r
+\If{$\tuple{ck_s,\tuple{k_s,v_t}} = \emptyset$}\r
+ \State $KV_s \gets KV_s \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$\r
+ \State $ck_p \gets ck_p + 1$\r
+\Else\r
+ \State $KV_s \gets (KV_s - \{\tuple{ck_s, \tuple{k_s,v_t}}\}) \cup \r
+ \{\tuple{ck_s, \tuple{k_s,v_s}}\}$\r
+\EndIf\r
+\State \Return{$KV_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{GetDEPairs}{$KV_s$}\r
+\State $DE_{ret} \gets \emptyset$\r
+\State $cp_s \gets cp$\r
+\If{$cr_p \neq \emptyset$}\r
+ \State $DE_{ret} \gets DE_{ret} \cup cr_p$\r
+ \State $cp_s \gets cp_s - 1$\r
+\EndIf\r
+\If{$|KV_s| \leq cp$}\Comment{KV set can extend multiple slots based on $cp$}\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 + 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
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{PutDataEntries}{$max'_p$}\r
+\State $s_p \gets MaxLastSeqN(MS)$\r
+\State $DE_p \gets GetDEPairs(KV)$\r
+\State $hmac_{c_p} \gets Hmac(DE_p,SK)$\r
+\State $Dat_p \gets CreateSlot(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 $stat_p \gets GetStatus(\tuple{stat_p,SL_p})$\r
+\State $SL_p \gets GetSL(\tuple{stat_p,SL_p})$\r
+\If{$\neg stat_p$}\Comment{Handle collision}\r
+ \State $\tuple{s_{col},sv_{col}} \gets GetColSeqN(SL_p,s_p)$\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_p \gets \tuple{s_{col},id_{col}}$\r
+\Else\r
+ \State $cr_p \gets \emptyset$\r
+\EndIf\r
+\State $\Call{ProcessSL}{SL_p}$\r
+\State \Return{$ST$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
\subsection{Formal Guarantees}\r
\r
\textit{To be completed ...}\r
projects / iotcloud.git / blobdiff