Minor edits

[iotcloud.git] / doc / iotcloud.tex

diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex
index 52ec3f098effc7dfa90b5d6c8d5c04f0985d5626..af1b1bb12a19e01e0d3332063a0dcaa7e86d9323 100644 (file)
--- a/doc/iotcloud.tex
+++ b/doc/iotcloud.tex
@@ -269,27 +269,10 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s
 \EndProcedure\r
 \end{algorithmic}\r
 \r
-\begin{algorithmic}[1]\r
-\Function{ValidHmac}{$DE_s,SK_s,hmac_{stored}$}\r
-\State $hmac_{computed} \gets Hmac(DE_s,SK_s)$\r
-\State \Return {$hmac_{stored} = hmac_{computed}$}\r
-\EndFunction\r
-\end{algorithmic}\r
-\r
-\begin{algorithmic}[1]\r
-\Function{ValidPrevHmac}{$s_s,DE_s,hmac_{p_s},hmac_{p_{sto}}$}\r
-\If{$s_s = 0 \land hmac_{p_s} = \emptyset$}\Comment{First slot - no previous HMAC}\r
-       \State \Return $true$\r
-\Else\r
-       \State \Return {$hmac_{p_{sto}} = hmac_{p_s}$}\r
-\EndIf\r
-\EndFunction\r
-\end{algorithmic}\r
-\r
 \begin{algorithmic}[1]\r
 \Function{GetQueSta}{$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
+\State $de_{qs} \gets ss$ \textit{such that} $ss \in DE_s, \r
+       de_s \in D \land type(de_s) = "qs"$\r
 \If{$de_{qs} \neq \emptyset$}\r
        \State $qs_{ret} \gets GetQS(de_{qs})$\r
 \Else\r
@@ -301,14 +284,14 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s
 \r
 \begin{algorithmic}[1]\r
 \Function{GetSlotSeq}{$DE_s$}\r
-\State $DE_{ss} \gets \{de_s | de_s \in DE_s, de_s = ss\}$\r
+\State $DE_{ss} \gets \{de | de \in DE_s \land type(de) = "ss"\}$\r
 \State \Return{$DE_{ss}$}\r
 \EndFunction\r
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
 \Function{GetColRes}{$DE_s$}\r
-\State $DE_{cr} \gets \{de_s | de_s \in DE_s, de_s = cr\}$\r
+\State $DE_{cr} \gets \{de | de \in DE_s \land type(de) = "cr"\}$\r
 \State \Return{$DE_{cr}$}\r
 \EndFunction\r
 \end{algorithmic}\r
@@ -466,7 +449,7 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s
 \r
 \begin{algorithmic}[1]\r
 \Function{UpdateDT}{$DT_s,DE_s,LV_s,s_s$}\r
-\State $DE_{s_{kv}} \gets \{de_s | de_s \in DE_s, de_s = kv\}$\r
+\State $DE_{s_{kv}} \gets \{de_s | de_s \in DE_s, type(de_s) = "kv"\}$\r
 \ForAll{$de_s \in DE_s$}\r
        \State $kv_s \gets GetKV(de_s)$\r
        \State $LV_s \gets \Call{UpdateKVLivEnt}{LV_s,kv_s,s_s}$\r
@@ -501,11 +484,10 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s
        \EndIf\r
        \State $DE_g \gets GetDatEnt(Dat_g)$\r
        \State $hmac_{p_{stored}} \gets GetPrevHmac(Dat_g)$\r
-       \If{$\neg \Call{ValidPrevHmac}{s_g,DE_g,hmac_{p_g},hmac_{p_{stored}}}$}\r
+       \If {$ \neg(s_g = 0 \land hmac_{p_g} = 0) \land hmac_{p_{stored}} \neq hmac_{p_g}$}\r
                \State \Call{Error}{'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
+       \If{$\Call{Hmac}{DE_g,SK} \neq GetCurrHmac(Dat_g)$ }\r
                \State \Call{Error}{'Invalid current HMAC value'}\r
        \EndIf\r
        \State $hmac_{p_g} \gets Hmac(DE_g,SK)$\Comment{Update $hmac_{p_g}$ for next check}\r
@@ -558,7 +540,7 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s
 \end{algorithmic}\r
 \r
 \begin{algorithmic}[1]\r
-\Function{GetValFromKey}{$k_g$}\r
+\Function{Get}{$k_g$}  \Comment{Interface function to get a value}\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 \Return{$v_s$}\r
@@ -604,7 +586,7 @@ $\tuple{ck,\tuple{k, v}} \in KV_s \wedge
 \forall \tuple{ck_s,\tuple{k_s, v_s}} \in KV_s, k = k_s$ \\\r
 \r
 \begin{algorithmic}[1]\r
-\Function{PutKVPair}{$KV_s,\tuple{k_s,v_s}$}\r
+\Function{Put}{$KV_s,\tuple{k_s,v_s}$}  \Comment{Interface function to update a key-value pair}\r
 \State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKVPair(KV,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
@@ -969,15 +951,12 @@ call them $\mathsf{t}$ and $\mathsf{u}$ such that $\mathsf{s_t \le s_u}$.
 Then $\mathsf{t}$ is in the path of $\mathsf{u}$. \r
 \end{lem}\r
 \begin{proof}\r
+Assume otherwise. Then there are some pairs $\mathsf{(t,u)}$ that violate this lemma. Take a specific $\mathsf{(t,u)}$ such that $\mathsf{s_u}$ is minimized and $\mathsf{s_t}$ is maximized for this choice of $\mathsf{s_u}$.\r
+\r
 Clearly $\mathsf{C}$ will throw an error if $\mathsf{s_t = s_u}$. So \r
 $\mathsf{s_t < s_u}$. Additionally, if $\mathsf{C}$ receives $\mathsf{u}$ before \r
 $\mathsf{t}$, this will cause it to throw an error, so $\mathsf{t}$ is received \r
-before $\mathsf{u}$.\r
-\r
-Assume that $\mathsf{t}$ is not in the path of $\mathsf{u}$. Take $\mathsf{u}$ \r
-to be the packet of smallest sequence number for which this occurs, and \r
-$\mathsf{t}$ be the packet with greatest sequence number for this $\mathsf{u}$. \r
-We will prove that an error occurs upon receipt of $\mathsf{u}$.\r
+before $\mathsf{u}$. We will prove that an error occurs upon receipt of $\mathsf{u}$.\r
 \r
 Let $\mathsf{r_1}$ be the earliest member of the path of $\mathsf{t}$ that is \r
 not in the path of $\mathsf{u}$, and $\mathsf{q}$ be its parent. Message \r