\newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}\r
\usepackage{color}\r
\usepackage{amsthm}\r
-\usepackage{algpseudocode}\r
+\usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx\r
\newtheorem{theorem}{Theorem}\r
\newtheorem{defn}{Definition}\r
\newcommand{\note}[1]{{\color{red} \bf [[#1]]}}\r
-\r
+\newcommand{\pushcode}[1][1]{\hskip\dimexpr #1\algorithmicindent\relax}\r
\begin{document}\r
\section{Approach}\r
\r
\r
\item Queue state entry is dead if there is a newer queue state entry.\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 slotes reaches \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
\end{enumerate}\r
\r
\r
\subsection{Server Algorithm}\r
\begin{algorithmic}[1]\r
-\Function{Server}{$m$,$max$,$s$,$Data*$}\r
+%\Function{CallServer}{$m$,$max$,$s$,$Data*$}\r
+\Function{CallServer}{$m,max,s,Data*$}\r
\textit{\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}\r
-\newline{// t = latest sequence number on server}\r
+\newline{// t = sequence numbers of slots on server}\r
\newline{// d = sequence number difference (1 by default)}\r
\newline{// Data = array of slots written/read (input only for write)}\r
\newline{// Q = queue of slots on server}\r
+\newline{// Slot = one data slot)}\r
\newline{// Resize() returns the old last slot in the queue}\r
\newline{// Append() updates Q and latest s after appending the new slot}\r
\newline{// Append() returns the latest Slot written with its correct s}\r
}\r
\If{$m = read$}\r
-\If{$s \in T = \{t_1, t_2, \dots, t_n\}$}\r
-\State $Data := \{Slot_{s}, Slot_{s+1}, \dots, Slot_{t_n}\} \forall Slot_i \in Q$\r
-\Else\r
-\State $Data := \emptyset$\r
-\EndIf\r
+ \If{$s \in T = \{t_1, t_2, \dots, t_n\}$}\r
+ \State $Data \gets \{Slot_{s}, Slot_{s+1}, \dots, Slot_{t_n}\} \forall Slot_i \in Q$\r
+ \Else\r
+ \State $Data \gets \emptyset$\r
+ \EndIf\r
\ElsIf{$m = write$}\r
-\If{$s = t_n + d$ \textbf{and} $n \leq max$ \textbf{and} $Data.length = 1$}\r
-\State $newSlot := Data[1]$\r
-\If{$n = max$}\r
-\State $DeleteFirst(Q)$\r
-\Else\r
-\State // $n < max$\r
-\State $n := n + 1$\r
-\EndIf\r
-\State $Data := Append(newSlot,Q)$\r
-\Else\r
-\State $Data := \emptyset$\r
-\EndIf\r
+ \If{$(s = t_n + d) \land (n \leq max) \land (Length(Data) = 1$)}\r
+ \State $newSlot \gets Data[1]$\r
+ \If{$n = max$}\r
+ \State $Data[2] \gets RemoveFirst(Q)$\r
+ \State $Data[1] \gets Append(newSlot,Q)$\r
+ \Else \Comment{$n < max$}\r
+ \State $n \gets n + 1$\r
+ \State $Data[1] \gets Append(newSlot,Q)$\r
+ \EndIf\r
+ \Else\r
+ \State $Data \gets \emptyset$\r
+ \EndIf\r
\ElsIf{$m = resize$}\r
-\State $Data := Resize(max)$\r
+ \State $Data \gets Resize(max)$\r
\EndIf\r
\State \Return{$Data$}\r
\EndFunction\r
\end{algorithmic}\r
\r
+\subsection{Client Algorithm}\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
+ \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
+ \pushcode[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
+ \pushcode[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
+ \pushcode[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
+ \EndIf\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
+ \Else\r
+ \State $ReportError(Data,write)$\r
+ \EndIf\r
+ \EndIf\r
+ \EndIf\r
+\r
+\ElsIf{$m = resize$}\r
+ \State $Data \gets CallServer(m,max,s,Data)$\r
+ \If{$Data = \emptyset$}\r
+ \State $ReportError(\emptyset,resize)$\r
+ \EndIf\r
+\EndIf\r
+\State \Return{$Result$}\r
+\EndFunction\r
+\end{algorithmic}\r
+\r
\subsection{Formal Guarantees}\r
\r
\textit{To be completed ...}\r
projects / iotcloud.git / commitdiff