From 2b9f991bf3d413efd741b69006ce041a2e3cfb2e Mon Sep 17 00:00:00 2001 From: tkwa Date: Tue, 16 Aug 2016 15:34:08 -0700 Subject: [PATCH] Minor edits --- doc/iotcloud.tex | 45 ++++++++++++--------------------------------- 1 file changed, 12 insertions(+), 33 deletions(-) diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex index 52ec3f0..af1b1bb 100644 --- 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 \end{algorithmic} -\begin{algorithmic}[1] -\Function{ValidHmac}{$DE_s,SK_s,hmac_{stored}$} -\State $hmac_{computed} \gets Hmac(DE_s,SK_s)$ -\State \Return {$hmac_{stored} = hmac_{computed}$} -\EndFunction -\end{algorithmic} - -\begin{algorithmic}[1] -\Function{ValidPrevHmac}{$s_s,DE_s,hmac_{p_s},hmac_{p_{sto}}$} -\If{$s_s = 0 \land hmac_{p_s} = \emptyset$}\Comment{First slot - no previous HMAC} - \State \Return $true$ -\Else - \State \Return {$hmac_{p_{sto}} = hmac_{p_s}$} -\EndIf -\EndFunction -\end{algorithmic} - \begin{algorithmic}[1] \Function{GetQueSta}{$DE_s$} -\State $de_{qs} \gets de_s$ \textit{such that} $de_s \in DE_s, - de_s \in D \land de_s = qs$ +\State $de_{qs} \gets ss$ \textit{such that} $ss \in DE_s, + de_s \in D \land type(de_s) = "qs"$ \If{$de_{qs} \neq \emptyset$} \State $qs_{ret} \gets GetQS(de_{qs})$ \Else @@ -301,14 +284,14 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s \begin{algorithmic}[1] \Function{GetSlotSeq}{$DE_s$} -\State $DE_{ss} \gets \{de_s | de_s \in DE_s, de_s = ss\}$ +\State $DE_{ss} \gets \{de | de \in DE_s \land type(de) = "ss"\}$ \State \Return{$DE_{ss}$} \EndFunction \end{algorithmic} \begin{algorithmic}[1] \Function{GetColRes}{$DE_s$} -\State $DE_{cr} \gets \{de_s | de_s \in DE_s, de_s = cr\}$ +\State $DE_{cr} \gets \{de | de \in DE_s \land type(de) = "cr"\}$ \State \Return{$DE_{cr}$} \EndFunction \end{algorithmic} @@ -466,7 +449,7 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s \begin{algorithmic}[1] \Function{UpdateDT}{$DT_s,DE_s,LV_s,s_s$} -\State $DE_{s_{kv}} \gets \{de_s | de_s \in DE_s, de_s = kv\}$ +\State $DE_{s_{kv}} \gets \{de_s | de_s \in DE_s, type(de_s) = "kv"\}$ \ForAll{$de_s \in DE_s$} \State $kv_s \gets GetKV(de_s)$ \State $LV_s \gets \Call{UpdateKVLivEnt}{LV_s,kv_s,s_s}$ @@ -501,11 +484,10 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s \EndIf \State $DE_g \gets GetDatEnt(Dat_g)$ \State $hmac_{p_{stored}} \gets GetPrevHmac(Dat_g)$ - \If{$\neg \Call{ValidPrevHmac}{s_g,DE_g,hmac_{p_g},hmac_{p_{stored}}}$} + \If {$ \neg(s_g = 0 \land hmac_{p_g} = 0) \land hmac_{p_{stored}} \neq hmac_{p_g}$} \State \Call{Error}{'Invalid previous HMAC value'} \EndIf - \State $hmac_{c_g} \gets GetCurrHmac(Dat_g)$ - \If{$\neg \Call{ValidHmac}{DE_g,SK,hmac_{c_g}}$} + \If{$\Call{Hmac}{DE_g,SK} \neq GetCurrHmac(Dat_g)$ } \State \Call{Error}{'Invalid current HMAC value'} \EndIf \State $hmac_{p_g} \gets Hmac(DE_g,SK)$\Comment{Update $hmac_{p_g}$ for next check} @@ -558,7 +540,7 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s \end{algorithmic} \begin{algorithmic}[1] -\Function{GetValFromKey}{$k_g$} +\Function{Get}{$k_g$} \Comment{Interface function to get a value} \State $\tuple{k_s,v_s} \gets \tuple{k,v}$ \textit{such that} $\tuple{k,v} \in DT \land k = k_g$ \State \Return{$v_s$} @@ -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$ \\ \begin{algorithmic}[1] -\Function{PutKVPair}{$KV_s,\tuple{k_s,v_s}$} +\Function{Put}{$KV_s,\tuple{k_s,v_s}$} \Comment{Interface function to update a key-value pair} \State $\tuple{ck_s,\tuple{k_s,v_t}} \gets GetKVPair(KV,k_s)$ \If{$\tuple{ck_s,\tuple{k_s,v_t}} = \emptyset$} \State $KV_s \gets KV_s \cup \{\tuple{ck_p, \tuple{k_s,v_s}}\}$ @@ -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}$. \end{lem} \begin{proof} +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}$. + Clearly $\mathsf{C}$ will throw an error if $\mathsf{s_t = s_u}$. So $\mathsf{s_t < s_u}$. Additionally, if $\mathsf{C}$ receives $\mathsf{u}$ before $\mathsf{t}$, this will cause it to throw an error, so $\mathsf{t}$ is received -before $\mathsf{u}$. - -Assume that $\mathsf{t}$ is not in the path of $\mathsf{u}$. Take $\mathsf{u}$ -to be the packet of smallest sequence number for which this occurs, and -$\mathsf{t}$ be the packet with greatest sequence number for this $\mathsf{u}$. -We will prove that an error occurs upon receipt of $\mathsf{u}$. +before $\mathsf{u}$. We will prove that an error occurs upon receipt of $\mathsf{u}$. Let $\mathsf{r_1}$ be the earliest member of the path of $\mathsf{t}$ that is not in the path of $\mathsf{u}$, and $\mathsf{q}$ be its parent. Message -- 2.34.1