\documentclass[11pt]{article}
\newcommand{\tuple}[1]{\ensuremath \langle #1 \rangle}
\usepackage{color}
\usepackage{amsthm}
\usepackage{amsmath}
\usepackage{algpseudocode}% http://ctan.org/pkg/algorithmicx
\newtheorem{theorem}{Theorem}
\newtheorem{defn}{Definition}
\newcommand{\note}[1]{{\color{red} \bf [[#1]]}}
\newcommand{\push}[1][1]{\hskip\dimexpr #1\algorithmicindent\relax}
\begin{document}
\section{Approach}

\subsection{Keys}

Each device has: user id + password

Server login is:
hash1(user id), hash1(password)

Symmetric Crypto keys is:
hash2(user id | password)

Server has finite length queue of entries + max\_entry\_identifier +
server login key

\subsection{Entry layout}
Each entry has:
\begin{enumerate}
\item Sequence identifier
\item Random IV (if needed by crypto algorithm)
\item Encrypted payload
\end{enumerate}

Payload has:
\begin{enumerate}
\item Sequence identifier
\item Machine id (most probably something like a 64-bit random number 
that is self-generated by client)
\item HMAC of previous slot
\item Data entries
\item HMAC of current slot
\end{enumerate}

A data entry can be one of these:
\begin{enumerate}
\item All or part of a Key-value entry
\item Slot sequence entry: Machine id + last message identifier 
\newline {The purpose of this is to keep the record of the last slot 
from a certain client if a client's update has to expunge that other 
client's last entry from the queue. This is kept in the slot until 
the entry owner inserts a newer update into the queue.}
\item Queue state entry: Includes queue size \newline {The purpose 
of this is for the client to tell if the server lies about the number 
of slots in the queue, e.g. if there are 2 queue state entry in the queue, 
e.g. 50 and 70, the client knows that when it sees 50, it should expect 
at most 50 slots in the queue and after it sees 70, it should expect 
50 slots before that queue state entry slot 50 and at most 70 slots. 
The queue state entry slot 70 is counted as slot number 51 in the queue.}
\end{enumerate}

\subsection{Live status}

Live status of entries:
\begin{enumerate}
\item Key-Value Entry is dead if either (a) there is a newer key-value pair or (b) it is incomplete.
	
\item Slot sequence number (of either a message version data
or user-level data) is dead if there is a newer slot from the same machine.

\item Queue state entry is dead if there is a newer queue state entry.
{In the case of queue state entries 50 and 70, this means that queue state 
entry 50 is dead and 70 is live. However, not until the number of slots reaches 
70 that queue state entry 50 will be expunged from the queue.}
\end{enumerate}

When data is at the end of the queue ready to expunge, if:
\begin{enumerate}
\item The key-value entry is not dead, it must be reinserted at the
beginning of the queue.

\item If the slot sequence number is not dead, then a message sequence
entry must be inserted.

\item If the queue state entry is not dead, it must be reinserted at the
beginning of the queue.
\end{enumerate}


\paragraph{Reads:}
Client sends a sequence number.  Server replies with either: all data
entries or all newer data entries.

\paragraph{Writes:}
Client sends slot, server verifies that sequence number is valid,
checks entry hash, and replies with an accept message if all checks
pass.  On success, client updates its sequence number.  On failure,
server sends updates slots to client and client validates those slots.

\paragraph{Local state on each client:}
A list of machines and the corresponding latest sequence numbers.

\paragraph{Validation procedure on client:}
\begin{enumerate}
\item Decrypt each new slot in order.
\item For each slot:
    (a) check its HMAC, and
    (b) check that the previous entry HMAC field matches the previous
    entry.
\item Check that the last message version for our machine matches our
last message sent.
\item For all other machines, check that the latest sequence number is
at least as large (never goes backwards).
\item That the queue has a current queue state entry.
\item That the number of entries received is consistent with the size
specified in the queue state entry.
\end{enumerate}

Key-value entries can span multiple slots.  They aren't valid until
they are complete.

\subsection{Resizing Queue}
Client can make a request to resize the queue. This is done as a write that combines:
  (a) a slot with the message, and
	(b) a request to the server

\subsection{Server Algorithm}
$s \in SN$ is a sequence number\\
$sv \in SV$ is a slot's value\\
$slot_s = \tuple{s, sv} \in SL \subseteq SN \times SV$ \\

\textbf{State} \\
\textit{SL = set of live slots on server} \\
\textit{max = maximum number of slots (input only for resize message)} \\
\textit{n = number of slots} \\

\begin{algorithmic}[1]
\Function{GetSlot}{$s_g$}
\State \Return{$\{\tuple{s, sv} \in SL \mid s \geq s_g\}$}
\EndFunction
\end{algorithmic}

\begin{algorithmic}[1]
\Function{PutSlot}{$s_p,sv_p,max'$}
\If{$(max' \neq \emptyset)$}\Comment{Resize}
\State $max \gets max'$
\EndIf
\State $s_n \gets \{\langle s,sv \rangle \in SL \mid 
    \forall \langle s_i,sv_i \rangle \in SL, s \geq s_i\}$\Comment{Last s}
\If{$(s_p = s_n + 1)$}
	\If{$n = max$}
		\State $SL \gets SL - \{\langle s,sv \rangle \in SL \mid 
    \forall \langle s_i,sv_i \rangle \in SL, s \leq s_i\}$\Comment{First s}
	\Else \Comment{$n < max$}
		\State $n \gets n + 1$
	\EndIf
    \State $SL \gets SL \cup \{\langle s_p,sv_p \rangle\}$
	\State \Return{$true$}
\Else
	\State \Return{$(false,\{\langle s,sv \rangle \in SL \mid 
    s \geq s_p\})$}
\EndIf
\EndFunction
\end{algorithmic}

\subsection{Client Algorithm}
\begin{algorithmic}[1]
\Function{CallClient}{$uid,pw,d,m,max,s,Data*,Result*$}
\textit{
\newline{// uid = user identification}
\newline{// pw = password}
\newline{// d = new data for write}
\newline{// m = client message (read/write/resize)}
\newline{// max = maximum number of slots (input only for resize message)}
\newline{// n = number of slots}
\newline{// s = sequence number for server request}
\newline{// t = sequence numbers of slots on server}
\newline{// mid = machine identification}
\newline{// seq = sequence number inside slot}
\newline{// newSlot = new slot}
\newline{// expSlot = expunged/expired slot}
\newline{// slotSeqE = slot sequence entry}
\newline{// M = list of all machines/devices with their respective latest s on client}
\newline{// Data = array of slots written/read (input only for write)}
\newline{// Result = array of decrypted and valid slots after a read}
\newline{// Slot = one data slot)}
\newline{// DSlot = one decrypted data slot)}
}
\State $SK = Hash(uid + pw)$
\If{$m = read$}
	\State $Data \gets CallServer(m,max,s,Data)$
	\If{$Data = \emptyset$}
		\State $ReportError(\emptyset,read)$
	\Else
		\If{$\neg HasCurrentQueueStateEntry(Data)$}
			\State $ReportError(DSlot_i,read)$
		\EndIf
		\ForAll{$Slot_i \in Data$}
			\State $DSlot_i \gets Decrypt(SK,Slot_i)$\Comment{Check s and HMAC}
			\If{$\neg (ValidSeqN(DSlot_i) \land ValidHmac(DSlot_i) \land $\\
				\push[1] $ValidPrevHmac(DSlot_i))$}
				\State $ReportError(DSlot_i,read)$
			\Else\Comment{Check only live entries}
				\If{$IsLiveSlotSequenceEntry(DSlot_i)$}
					\State $lastS \gets LastSeqN(DSlot_i)$
					\State $lastMid \gets LastMachineId(DSlot_i)$
					\If{$lastS \neq LastSeqN(lastMid,M)$}
						\State $ReportError(DSlot_i,read)$
					\EndIf
				\ElsIf{$IsLiveKeyValueEntry(DSlot_i)$}
					\State $mid \gets MachineId(DSlot_i)$
					\State $seq \gets SeqN(DSlot_i)$
					\If{$IsOwnMid(mid)$}
						\If{$IsLastS(mid,seq,Data) \land $\\
						\push[1] $(seq \neq LastSeqN(mid,M))$}
							\State $ReportError(DSlot_i,read)$
						\EndIf
					\Else\Comment{Check s for other machines}
						\If{$IsLastS(mid,seq,Data) \land $\\
						\push[1] $(seq < LastSeqN(mid,M))$}
							\State $ReportError(DSlot_i,read)$
						\EndIf
					\EndIf\Comment{Check queue state entry}
				\ElsIf{$IsLiveQueueStateEntry(DSlot_i)$}
					\If{$IsCurrentQueueState(DSlot_i)$}
						\If{$Length(Data) > QueueLength(DSlot_i)$}
							\State $ReportError(DSlot_i,read)$
						\EndIf
					\EndIf
				\Else
					\State $ReportError(DSlot_i,read)$
				\EndIf
			\EndIf
			\State $Result \gets Concat(Result, DSlot_i)$
		\EndFor
	\EndIf

\ElsIf{$m = write$}
	\State $newSlot \gets CreateSlot(d)$
	\State $Data[1] \gets Encrypt(SK,newSlot)$
	\State $Data \gets CallServer(m,max,s,Data)$
	\If{$Data = \emptyset$}
		\State $ReportError(\emptyset,write)$
	\Else\Comment Check for valid return value from server
		\If{$\neg ValidOldLastEntry(Data[1])$}
			\State $ReportError(Data[1],write)$
		\Else\Comment{Check if we need slot sequence entry}
			\If{$Length(Data) = 2$}
				\State $expSlot \gets Decrypt(SK,Data[2])$
				\State $mid \gets MachineId(expSlot)$
				\State $seq \gets SeqN(expSlot)$
				\If{$seq = LastSeqN(mid,M)$}\Comment{Liveness check}
					\State $slotSeqE \gets CreateSlotSeqE(mid,seq)$
					\State $Data[1] \gets Encrypt(SK,slotSeqE)$
					\State $Data \gets CallServer(m,max,s,Data)$
				\EndIf
			\Else
				\State $ReportError(Data,write)$
			\EndIf
		\EndIf
	\EndIf

\ElsIf{$m = resize$}
	\State $Data \gets CallServer(m,max,s,Data)$
	\If{$Data = \emptyset$}
		\State $ReportError(\emptyset,resize)$
	\EndIf
\EndIf
\State \Return{$Result$}
\EndFunction
\end{algorithmic}

\subsection{Formal Guarantees}

\textit{To be completed ...}

\begin{defn}[System Execution]
Let \\
\begin{center}
$Q = \{slot_{sn_1}, slot_{sn_2}, \dots, Slot_{sn_n}\}$, \\
$SN = \{sn_1, sn_2, \dots, sn_n\}$ \\
\end{center}
denote a queue $Q$ of $n$ slots, with each slot entry being denoted by a
valid sequence number $sn_i \in SN$. $Q$ represents a total order of all 
slot updates from all corresponding machines.
%\textit{Formalize a system execution as a sequence of slot updates...
%There is a total order of all slot updates.}
\end{defn}

\begin{defn}[Transitive Closure]
A transitive closure $\tau : \tau = \epsilon_{update(slot_i)} R $
$\epsilon_{receive(slot_i)}$ is a relation from slot update event
$\epsilon$ to a slot receive event $\epsilon$ for $slot_i$.
%Define transitive closure relation for slot updates...  There is an
%edge from a slot update to a slot receive event if the receive event
%reads from the update event.
\end{defn}

\begin{defn}[Suborder]
Let \\
\begin{center}
$q = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\}, 
sn_1 \leq i \leq j \leq sn_n \Longrightarrow q \subseteq Q$
\end{center}
denote a suborder of the total order. Set q is a sequence of contiguous
slot updates that is a subset of a total order of all slot updates in Q.
%Define suborder of total order.  It is a sequence of contiguous slots
%updates (as observed by a given device).
\end{defn}

\begin{defn}[Prefix of a suborder]
Given a suborder \\ 
\begin{center}
$q' = \{slot_{i}, slot_{i+1}, \dots, slot_{j}, \dots\}, 
sn_1 \leq i \leq j \leq sn_n \Longrightarrow 
q' \subseteq Q$
\end{center}
with $slot_{j}$ as a slot update in $q'$, the prefix of $q'$ is a sequence 
of all slot updates $\{slot_{i}, slot_{i+1}, \dots, slot_{j-1}\} \cup
slot_{j}$.
%Given a sub order $o=u_{i},u_{i+1},...,u_j, u_{j+i},..., u', ...$ and
%a slot update $u'$ in $o$, the prefix of $o$ is a sequence of all
%updates that occur before $u'$ and $u'$.
\end{defn}

\begin{defn}[Consistency between a suborder and a total order]
A suborder $q'$ is consistent with a total order $T$ of $Q$, if all
updates in $q'$ appear in $T$ and they appear in the same order, as 
the following:
\begin{center}
$q' = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\},$
$T = \{slot_{sn_1}, \dots, slot_{i}, slot_{i+1}, \dots, slot_{j}, \dots,
slot_{sn_n}\},$ \\ $sn_1 \leq i \leq j \leq sn_n \Longrightarrow
q' \subseteq T$
\end{center}
%A suborder $o$ is consistent with a total order $t$, if all updates in $o$ %appear in $t$ and they appear in the same order.
\end{defn}

\begin{defn}[Consistency between suborders]
Two suborders U and V are consistent if there exist a total order T 
such that both U and V are suborders of T.
\begin{center}
$U = \{slot_{i}, slot_{i+1}, \dots, slot_{j}\},$ \\
$V = \{slot_{k}, slot_{k+1}, \dots, slot_{l}\},$ \\
$sn_1 \leq i \leq j \leq k \leq l \leq sn_n,$ \\
$U \subset T \land V \subset T$ \\
$T = \{slot_{sn_1}, \dots, slot_{i}, slot_{i+1}, \dots, slot_{j}, $\\
$\dots, slot_{k}, slot_{k+1}, \dots, slot_{l}, \dots, slot_{sn_n}\}$
\end{center}
%Define notion of consistency between suborders...  Two suborders U,V
%are consistent if there exist a total order T such that both U and V
%are suborders of T.
\end{defn}

\begin{defn}[Error-free execution]
An error-free execution, for which the client does not flag any errors
is defined by the following criteria:
\begin{enumerate}
\item Item 1
\item Item 2
\end{enumerate}
%not flag any errors...
%Define error-free execution --- execution for which the client does
%not flag any errors...
\end{defn}

\begin{theorem} Error-free execution of algorithm ensures that the suborder
for node n is consistent with the prefix suborder for all other nodes
that are in the transitive closure.
\end{theorem}
\begin{proof}
\textit{TODO}
\end{proof}

\begin{defn}[State of Data Structure]
Define in terms of playing all updates sequentially onto local data
structure.
\end{defn}

\begin{theorem}
Algorithm gives consistent view of data structure.
\end{theorem}
\begin{proof}
\textit{TODO}
\end{proof}

\subsection{Future Work}
\paragraph{Support Messages}
  A message is dead once receiving machine sends an entry with a newer
  sequence identifier

\paragraph{Persistent data structures}
	Root object w/ fields
	Other objects can be reachable from root
	Each object has its own entries
	Dead objects correspond to dead 

\paragraph{Multiple App Sharing}

Idea is to separate subspace of entries...  Shared with other cloud...
\end{document}

