\newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}\r
\usepackage{color}\r
\usepackage{amsthm}\r
-\usepackage{amsmath}\r
\usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx\r
\newtheorem{theorem}{Theorem}\r
\newtheorem{defn}{Definition}\r
the entry owner inserts a newer update into the queue.}\r
\item Queue state entry: Includes queue size \newline {The purpose \r
of this is for the client to tell if the server lies about the number \r
-of slots in the queue, e.g. if there are 2 queue state entries in the queue, \r
+of slots in the queue, e.g. if there are 2 queue state entry in the queue, \r
e.g. 50 and 70, the client knows that when it sees 50, it should expect \r
at most 50 slots in the queue and after it sees 70, it should expect \r
50 slots before that queue state entry slot 50 and at most 70 slots. \r
The queue state entry slot 70 is counted as slot number 51 in the queue.}\r
+\item Collision resolution entry: message identifier + machine id of a\r
+collision winner\r
+\newline {The purpose of this is to keep keep track of the winner of \r
+all the collisions until all clients have seen the particular entry.}\r
\end{enumerate}\r
\r
\subsection{Live status}\r
{In the case of queue state entries 50 and 70, this means that queue state \r
entry 50 is dead and 70 is live. However, not until the number of slots reaches \r
70 that queue state entry 50 will be expunged from the queue.}\r
+\r
+\item Collision resolution entry is dead if this entry has been seen\r
+by all clients after a collision happens.\r
\end{enumerate}\r
\r
When data is at the end of the queue ready to expunge, if:\r
(b) a request to the server\r
\r
\subsection{Server Algorithm}\r
-$s \in SN$ is a sequence number\\\r
+$s \in SN$ is a sequence number set\\\r
$sv \in SV$ is a slot's value\\\r
$slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\\r
\r
\textit{max = maximum number of slots (input only for resize message)} \\\r
\textit{n = number of slots} \\ \\\r
\textbf{Helper Function} \\\r
-$MaxSlot(SL')= \tuple{s, sv} \mid \tuple{s, sv}\r
-\in SL' \wedge \forall \tuple{s', sv'} \in SL', s \geq s'$ \\\r
-$MinSlot(SL')= \tuple{s, sv} \mid \tuple{s, sv} \r
-\in SL' \wedge \forall \tuple{s', sv'} \in SL', s \leq s'$ \\\r
+$MaxSlot(SL_s)= \tuple{s, sv} \mid \tuple{s, sv}\r
+\in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \geq s_s$ \\\r
+$MinSlot(SL_s)= \tuple{s, sv} \mid \tuple{s, sv} \r
+\in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s \leq s_s$ \\\r
$SeqN(\tuple{s, sv})=s$ \\\r
$SlotVal(\tuple{s, sv})=sv$ \\\r
\r
\State $n \gets n + 1$\r
\EndIf\r
\State $SL \gets SL \cup \{\tuple{s_p,sv_p}\}$\r
- \State \Return{$true$}\r
+ \State \Return{$(true,\emptyset)$}\r
\Else\r
\State \Return{$(false,\{\tuple{s,sv}\in SL \mid \r
s \geq s_p\})$}\r
\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
+$v$ is value of entry \\\r
+$kv$ is a key-value entry $\tuple{k,v}$, $kv \in D$ \\\r
+$ss$ is a slot sequence entry $\tuple{id,s_{last}}$, \r
+id + last s of a machine, $ss \in D$ \\\r
+$qs$ is a queue state entry, $qs \in D$ \\\r
+$cr$ is a collision resolution entry $\tuple{s_{col},id_{col}}$, \r
+s + id of a machine that wins a collision, $cr \in D$ \\\r
+$D = \{kv,ss,qs,cr\}$ \\\r
+$DE = \{de \mid de \in D\}$ \\ \\\r
+$s \in SN$ is a sequence number set\\\r
+$id$ is a machine ID\\\r
+$hmac_p$ is the HMAC value of the previous slot \\\r
+$hmac_c$ is the HMAC value of the current slot \\\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{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_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_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_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
+$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
+$MinSlot(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 \leq s_s$ \\\r
+$Slot(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
+$SeqN(\tuple{s, sv})=s$ \\\r
+$SlotVal(\tuple{s, sv})=sv$ \\\r
+$Decrypt(SK_s,sv_s)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
+$GetSeqN(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=s$ \\\r
+$GetMacId(Dat_s = \tuple{s,id,hmac_p,DE,hmac_c})=id$ \\\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
+$GetKV(de_s$ \textit{such that} $de_s \in D \land de_s = kv)=\tuple{k_s,v_s}$ \\\r
+$GetSS(de_s$ \textit{such that} $de_s \in D \land de_s = ss)=\tuple{id,s_{last}}$ \\\r
+$GetQS(de_s$ \textit{such that} $de_s \in D \land de_s = qs)=qs_s$ \\\r
+$GetCR(de_s$ \textit{such that} $de_s \in D \land de_s = cr)=\tuple{s_s,id_s}$ \\\r
+$GetLastSeqN(MS_s,id_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}}\r
+\in MS_s \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, id = id_s$ \\\r
+$GetMachineId(SM_s,s_s)= id$ \textit{such that} $\tuple{s, id}\r
+\in SM_s \wedge \forall \tuple{s_s, id_s} \in SM_s, s = s_s$ \\\r
+$GetS(\tuple{s, id})=s$ \\\r
+$GetId(\tuple{s, id})=id$ \\\r
+$GetKey(\tuple{k, v})=k$ \\\r
+$GetVal(\tuple{k, v})=v$ \\\r
+$GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v} \r
+\in DT_s \wedge \forall \tuple{k_s, v_s} \in DT_s, k = k_s$ \\\r
+\r
+\begin{algorithmic}[1]\r
+\Procedure{ReportError}{$msg$}\r
+\State $Print(msg)$\r
+\State $Halt()$\r
+\EndProcedure\r
+\end{algorithmic}\r
+\r
\begin{algorithmic}[1]\r
-\Function{CallClient}{$uid,pw,d,m,max,s,Data*,Result*$}\r
-\textit{\r
-\newline{// uid = user identification}\r
-\newline{// pw = password}\r
-\newline{// d = new data for write}\r
-\newline{// m = client message (read/write/resize)}\r
-\newline{// max = maximum number of slots (input only for resize message)}\r
-\newline{// n = number of slots}\r
-\newline{// s = sequence number for server request}\r
-\newline{// t = sequence numbers of slots on server}\r
-\newline{// mid = machine identification}\r
-\newline{// seq = sequence number inside slot}\r
-\newline{// newSlot = new slot}\r
-\newline{// expSlot = expunged/expired slot}\r
-\newline{// slotSeqE = slot sequence entry}\r
-\newline{// M = list of all machines/devices with their respective latest s on client}\r
-\newline{// Data = array of slots written/read (input only for write)}\r
-\newline{// Result = array of decrypted and valid slots after a read}\r
-\newline{// Slot = one data slot)}\r
-\newline{// DSlot = one decrypted data slot)}\r
-}\r
-\State $SK = Hash(uid + pw)$\r
-\If{$m = read$}\r
- \State $Data \gets CallServer(m,max,s,Data)$\r
- \If{$Data = \emptyset$}\r
- \State $ReportError(\emptyset,read)$\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
+ \State $valid \gets false$\r
+\EndIf\r
+\State \Return{$valid$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\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
+ \If{$hmac_{p_{sto}} = hmac_{p_s}$}\r
+ \State $valid \gets true$\r
\Else\r
- \If{$\neg HasCurrentQueueStateEntry(Data)$}\r
- \State $ReportError(DSlot_i,read)$\r
- \EndIf\r
- \ForAll{$Slot_i \in Data$}\r
- \State $DSlot_i \gets Decrypt(SK,Slot_i)$\Comment{Check s and HMAC}\r
- \If{$\neg (ValidSeqN(DSlot_i) \land ValidHmac(DSlot_i) \land $\\\r
- \push[1] $ValidPrevHmac(DSlot_i))$}\r
- \State $ReportError(DSlot_i,read)$\r
- \Else\Comment{Check only live entries}\r
- \If{$IsLiveSlotSequenceEntry(DSlot_i)$}\r
- \State $lastS \gets LastSeqN(DSlot_i)$\r
- \State $lastMid \gets LastMachineId(DSlot_i)$\r
- \If{$lastS \neq LastSeqN(lastMid,M)$}\r
- \State $ReportError(DSlot_i,read)$\r
- \EndIf\r
- \ElsIf{$IsLiveKeyValueEntry(DSlot_i)$}\r
- \State $mid \gets MachineId(DSlot_i)$\r
- \State $seq \gets SeqN(DSlot_i)$\r
- \If{$IsOwnMid(mid)$}\r
- \If{$IsLastS(mid,seq,Data) \land $\\\r
- \push[1] $(seq \neq LastSeqN(mid,M))$}\r
- \State $ReportError(DSlot_i,read)$\r
- \EndIf\r
- \Else\Comment{Check s for other machines}\r
- \If{$IsLastS(mid,seq,Data) \land $\\\r
- \push[1] $(seq < LastSeqN(mid,M))$}\r
- \State $ReportError(DSlot_i,read)$\r
- \EndIf\r
- \EndIf\Comment{Check queue state entry}\r
- \ElsIf{$IsLiveQueueStateEntry(DSlot_i)$}\r
- \If{$IsCurrentQueueState(DSlot_i)$}\r
- \If{$Length(Data) > QueueLength(DSlot_i)$}\r
- \State $ReportError(DSlot_i,read)$\r
- \EndIf\r
- \EndIf\r
- \Else\r
- \State $ReportError(DSlot_i,read)$\r
- \EndIf\r
- \EndIf\r
- \State $Result \gets Concat(Result, DSlot_i)$\r
- \EndFor\r
+ \State $valid \gets false$\r
\EndIf\r
+\EndIf\r
+\State \Return{$valid$}\r
+\EndFunction\r
+\end{algorithmic}\r
\r
-\ElsIf{$m = write$}\r
- \State $newSlot \gets CreateSlot(d)$\r
- \State $Data[1] \gets Encrypt(SK,newSlot)$\r
- \State $Data \gets CallServer(m,max,s,Data)$\r
- \If{$Data = \emptyset$}\r
- \State $ReportError(\emptyset,write)$\r
- \Else\Comment Check for valid return value from server\r
- \If{$\neg ValidOldLastEntry(Data[1])$}\r
- \State $ReportError(Data[1],write)$\r
- \Else\Comment{Check if we need slot sequence entry}\r
- \If{$Length(Data) = 2$}\r
- \State $expSlot \gets Decrypt(SK,Data[2])$\r
- \State $mid \gets MachineId(expSlot)$\r
- \State $seq \gets SeqN(expSlot)$\r
- \If{$seq = LastSeqN(mid,M)$}\Comment{Liveness check}\r
- \State $slotSeqE \gets CreateSlotSeqE(mid,seq)$\r
- \State $Data[1] \gets Encrypt(SK,slotSeqE)$\r
- \State $Data \gets CallServer(m,max,s,Data)$\r
- \EndIf\r
+\begin{algorithmic}[1]\r
+\Function{GetQueSta}{$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
+ \State $qs_{ret} \gets GetQS(de_{qs})$\r
+\Else\r
+ \State $qs_{ret} \gets \emptyset$\r
+\EndIf\r
+\State \Return{$qs_{ret}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{GetSlotSeq}{$Dat_s$}\r
+\State $DE_s \gets GetDatEnt(Dat_s)$\r
+\State $de_{ss} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
+ de_s \in D \land de_s = ss$\r
+\If{$de_{ss} \neq \emptyset$}\r
+ \State $\tuple{id_{ret},s_{last_{ret}}} \gets GetSS(de_{ss})$\r
+\Else\r
+ \State $\tuple{id_{ret},s_{last_{ret}}} \gets \emptyset$\r
+\EndIf\r
+\State \Return{$\tuple{id_{ret},s_{last_{ret}}}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{GetColRes}{$Dat_s$}\r
+\State $DE_s \gets GetDatEnt(Dat_s)$\r
+\State $de_{cr} \gets de_s$ \textit{such that} $de_s \in DE_s, \r
+ de_s \in D \land de_s = cr$\r
+\If{$de_{cr} \neq \emptyset$}\r
+ \State $\tuple{s_{ret},id_{ret}} \gets GetCR(de_{cr})$\r
+\Else\r
+ \State $\tuple{s_{ret},id_{ret}} \r
+ \gets \emptyset$\r
+\EndIf\r
+\State \Return{$\tuple{s_{ret},id_{ret}}$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{UpdateLastSeqN}{$id_s,s_s,MS_s$}\r
+\State $s_t \gets GetLastSeqN(MS_s,id_s)$\r
+\If{$s_t = \emptyset$}\r
+ \State $MS_s \gets MS_s \cup \{\tuple{id_s,s_s}\}$\Comment{First occurrence}\r
+\Else\r
+ \If{$s_s > s_t$}\Comment{Update entry with a later s}\r
+ \State $MS_s \gets (MS_s - \{\tuple{id_s,s_t}\}) \cup \r
+ \{\tuple{id_s,s_s}\}$\r
+ \EndIf\r
+\EndIf\r
+\State \Return{$MS_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Procedure{CheckLastSeqN}{$MS_s,MS_t$}\Comment{Check $MS_t$ based on $MS_s$}\r
+\ForAll{$\tuple{id_t,s_{t_{last}}} \in MS_t$}\r
+ \State $s_{s_{last}} \gets GetLastSeqN(MS_s,id_t)$\r
+ \If{$s_{s_{last}} \neq \emptyset$}\r
+ \If{$id_t = id_{self}$}\r
+ \If{$s_{s_{last}} \neq s_{t_{last}}$}\r
+ \State \Call{ReportError}{'Invalid last $s$ for this machine'}\r
+ \EndIf\r
+ \Else\r
+ \If{$s_{s_{last}} \geq s_{t_{last}}$}\r
+ \State $MS_s \gets (MS_s - \{\tuple{id_t,s_{t_{last}}}\}) \cup \r
+ \{\tuple{id_t,s_{s_{last}}}\}$\r
\Else\r
- \State $ReportError(Data,write)$\r
+ \State \Call{ReportError}{'Invalid last $s$ for machine $id_t$'}\r
\EndIf\r
\EndIf\r
\EndIf\r
+\EndFor\r
+\EndProcedure\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Procedure{CheckColRes}{$SM_s,\tuple{s_t,id_t}$}\Comment{Check $id_s$ in $SM_s$}\r
+\State $s_t \gets GetS(\tuple{s_t,id_t})$\r
+\State $id_t \gets GetId(\tuple{s_t,id_t})$\r
+\State $id_s \gets GetMachineId(SM_s,s_t)$\r
+\If{$id_s \neq id_t$}\r
+ \State \Call{ReportError}{'Invalid $id_s$ for this slot update'}\r
+\EndIf\r
+\EndProcedure\r
+\end{algorithmic}\r
+\r
+\begin{algorithmic}[1]\r
+\Function{UpdateDT}{$DT_s,Dat_s$}\r
+\State $DE_s \gets GetDatEnt(Dat_s)$\r
+\ForAll{$de_s \in DE_s$}\r
+ \If{$de_s$ \textit{such that} $de_s \in D \land de_s = kv$}\r
+ \State $\tuple{k_s,v_s} \gets GetKV(de_s)$\r
+ \State $k_s \gets GetKey(\tuple{k_s,v_s})$\r
+ \State $\tuple{k_s,v_t} \gets GetKeyVal(DT_s,k_s)$\r
+ \If{$\tuple{k_s,v_t} = \emptyset$}\r
+ \State $DT_s \gets DT_s \cup \{\tuple{k_s,v_s}\}$\r
+ \Else\r
+ \State $DT_s \gets (DT_s - \{\tuple{k_s,v_t}\}) \cup \r
+ \{\tuple{k_s,v_s}\}$\r
+ \EndIf\r
+ \EndIf\r
+\EndFor\r
+\State \Return{$DT_s$}\r
+\EndFunction\r
+\end{algorithmic}\r
\r
-\ElsIf{$m = resize$}\r
- \State $Data \gets CallServer(m,max,s,Data)$\r
- \If{$Data = \emptyset$}\r
- \State $ReportError(\emptyset,resize)$\r
+\begin{algorithmic}[1]\r
+\Procedure{ProcessSL}{$SL_g$}\r
+\State $MS_g \gets \emptyset$\r
+\State $SM_{curr} \gets \emptyset$\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
+ \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
+ \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_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_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_g}$\Comment{Handle ss}\r
+ \If{$\tuple{id_d,s_{d_{last}}} \neq \emptyset$}\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_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 $s_{c_{last}} \gets GetLastSeqN(MS,id_e)$\r
+ \If{$s_{c_{last}} < s_e$}\r
+ \State $\Call{CheckColRes}{SM,\tuple{s_e,id_e}}$\r
+ \EndIf\r
+ \EndIf\r
+ \State $DT \gets \Call{UpdateDT}{DT,Dat_g}$\r
+\EndFor\r
+\State $SM \gets SM_{curr}$\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_g$'}\r
+\EndIf\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
+\Function{GetValFromKey}{$k_g$}\r
+\State $\tuple{k_s,v_s} \gets \tuple{k,v}$ \textit{such that} $\tuple{k,v} \r
+ \in DT \land k = k_g$\r
+\State $v_s \gets GetVal(\tuple{k_s,v_s})$\r
+\State \Return{$v_s$}\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 \Return{$Result$}\r
+\State $\Call{ProcessSL}{SL_p}$\r
+\State \Return{$ST$}\r
\EndFunction\r
\end{algorithmic}\r
\r
projects / iotcloud.git / blobdiff