+\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
+$D = \{kv,ss,qs\}$ \\\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_c$ = set MS to save all $\tuple{id, s_{last}}$ pairs while\r
+traversing DT after a request to server (initially empty)} \\\r
+\textit{$max_c$ = maximum number of slots (initially $max_c > 0$)} \\\r
+\textit{m = number of slots on client (initially $m = 0 \mid m \leq n$)} \\\r
+\textit{$hmac_p$ = the HMAC value of the previous slot ($hmac_p = \emptyset$ \r
+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} \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
+$Decrypt(SK_s,sv_s)=Dat_s=\tuple{s,id,hmac_p,DE,hmac_c}$ \\\r
+$ComputeHash(bit_s)$ is a hash function that generates hash value on $bit_s$ \\\r
+$ComputeHmac(bit_s,SK_s)$ is a HMAC function that generates HMAC value on $bit_s$ \r
+based on key $SK_s$\\\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
+$GetQS(de_s \mid de_s \in D \land de_s = qs)=qs$ \\\r
+$GetSS(de_s \mid de_s \in D \land de_s = ss)=ss$ \\\r
+$GetKV(de_s \mid de_s \in D \land de_s = kv)=kv=\tuple{k,v}$ \\\r
+$GetLastSeqN(MS_s,id_s)= s_{last} \mid \tuple{id, s_{last}}\r
+\in MS_s \wedge \forall \tuple{id_s, s_{s_{last}}} \in MS_s, \r
+id = id_s$ \\\r
+$GetKey(\tuple{k, v})=k$ \\\r
+$GetVal(\tuple{k, v})=v$ \\\r
+$GetKeyVal(DT_s,k_s)= \tuple{k, v} \mid \tuple{k, v} \r
+\in DT_s \wedge \forall \tuple{k_s, v_s} \in DT_s, k = k_s$ \\\r
+\r