From 03d65f00156f48e01ec779a8610872976d2d1198 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Mon, 22 Aug 2016 12:13:22 -0700 Subject: [PATCH] Refactoring HMAC checks, replacing de type checks with IsKV, IsCR, IsSS, and IsQS --- doc/iotcloud.tex | 93 +++++++++++++++++++++++++++++++----------------- 1 file changed, 61 insertions(+), 32 deletions(-) diff --git a/doc/iotcloud.tex b/doc/iotcloud.tex index fd8a719..9d970c4 100644 --- a/doc/iotcloud.tex +++ b/doc/iotcloud.tex @@ -182,7 +182,6 @@ $SlotVal(slot_s = \tuple{s, sv})=sv$ \\ \subsection{Client Algorithm} \subsubsection{Reading Slots} \textbf{Data Entry} \\ -$de$ is a data entry \\ $k$ is key of entry \\ $v$ is value of entry \\ $kv$ is a key-value entry $\tuple{k,v}$, $kv \in DE$ \\ @@ -191,11 +190,14 @@ id + last s of a machine, $ss \in DE$ \\ $qs$ is a queue state entry (contains $max$ size of queue), $qs \in DE$ \\ $cr$ is a collision resolution entry $\tuple{s_{col},id_{col}}$, s + id of a machine that wins a collision, $cr \in DE$ \\ +$de$ is a data entry that can be a $kv$, $ss$, $qs$, or $cr$ \\ $DE$ is a set of all data entries, possibly of different types, in a single message \\ $s \in SN$ is a sequence number \\ $id$ is a machine ID\\ $hmac_p$ is the HMAC value of the previous slot \\ $hmac_c$ is the HMAC value of the current slot \\ +$hmac_{p_g}$ is the HMAC value of the previous slot in procedure $\Call{ProcessSL}{}$ \\ +$hmac_{c_g}$ is the HMAC value of the current slot in procedure $\Call{ProcessSL}{}$ \\ $Dat_s = \tuple{s,id,hmac_p,DE,hmac_c}$ \\ $slot_s = \tuple{s, E(Dat_s)} = \tuple{s, E(\tuple{s,id,hmac_p,DE,hmac_c})}$ \\ \\ @@ -242,14 +244,23 @@ $GetLivEntLastS(LV_s,kv_s)= s$ \textit{such that} $\tuple{kv, s} \in LV_s \wedge \forall \tuple{kv_s, s_s} \in LV_s, kv_s = kv$ \\ $GetKV($key-value data entry$)=\tuple{k_s,v_s} = kv_s$ \\ $GetSS($slot-sequence data entry$)=\tuple{id_s,s_{s_{last}}} = ss_s$ \\ -$GetQS($queue-state data entry$)=qs_s$ \\ -$GetCR($collision-resolution data entry$)=\tuple{s_s,id_s} = cr_s$ \\ -$GetKey(kv = \tuple{k, v})=k$ \\ -$GetVal(kv = \tuple{k, v})=v$ \\ -$GetId(ss = \tuple{id, s_{last}})=id$ \\ -$GetSLast(ss = \tuple{id, s_{last}})=s_{last}$ \\ -$GetS(cr = \tuple{s, id})=s$ \\ -$GetId(cr = \tuple{s, id})=id$ \\ +%$GetQS($queue-state data entry$)=qs_s$ \\ +$GetCR($de$)=\tuple{s_s,id_s} = cr_s$ \\ +$Hmac(Dat_s,SK) = hmac_c$ \textit{value computed from $s$, $id$, +$hmac_p$, and $DE$ taken from $Dat_s$} \\ +$IsKV(de) = true$ \textit{if $de$ is a $kv$, false otherwise} \\ +$IsSS(de) = true$ \textit{if $de$ is a $ss$, false otherwise} \\ +$IsQS(de) = true$ \textit{if $de$ is a $qs$, false otherwise} \\ +$IsCR(de) = true$ \textit{if $de$ is a $cr$, false otherwise} \\ +$GetKey(kv)=k$\Comment{$kv = \tuple{k, v}$} \\ +$GetVal(kv)=v$ \\ +$GetId(ss)=id$\Comment{$ss = \tuple{id, s_{last}}$} \\ +$GetSLast(ss)=s_{last}$ \\ +$GetS(cr)=s$\Comment{$cr = \tuple{s, id}$} \\ +$GetId(cr)=id$ \\ +$GetLastS(sl_{last})=s$\Comment{$sl_{last} = \tuple{s,sv,id}$} \\ +$GetSV(sl_{last})=sv$ \\ +$GetID(sl_{last})=id$ \\ $GetKeyVal(DT_s,k_s)= \tuple{k, v}$ \textit{such that} $\tuple{k, v} \in DT_s \wedge \forall \tuple{k_s, v_s} \in DT_s, k = k_s$ \\ $MaxLastSeqN(MS_s)= s_{last}$ \textit{such that} $\tuple{id, s_{last}} \in MS_s @@ -270,10 +281,10 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s \begin{algorithmic}[1] \Function{GetQueSta}{$DE_s$} -\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})$ +\State $qs_{de} \gets qs$ \textit{such that} $qs \in DE_s, + de_s \in D \land IsQS(de_s)$ +\If{$qs_{de} \neq \emptyset$} + \State $qs_{ret} \gets qs_{de})$ \Else \State $qs_{ret} \gets \emptyset$ \EndIf @@ -283,14 +294,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 | de \in DE_s \land type(de) = ``ss"\}$ +\State $DE_{ss} \gets \{de | de \in DE_s \land IsSS(de)\}$ \State \Return{$DE_{ss}$} \EndFunction \end{algorithmic} \begin{algorithmic}[1] \Function{GetColRes}{$DE_s$} -\State $DE_{cr} \gets \{de | de \in DE_s \land type(de) = ``cr"\}$ +\State $DE_{cr} \gets \{de | de \in DE_s \land IsCR(de)\}$ \State \Return{$DE_{cr}$} \EndFunction \end{algorithmic} @@ -446,10 +457,27 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s \EndFunction \end{algorithmic} +\begin{algorithmic}[1] +\Function{ValidateHmacChain}{$Dat_s,s_s,hmac_{p_s},sl_l$} + \State $hmac_{p_{stored}} \gets GetPrevHmac(Dat_s)$ + \If {$ \neg(s_s = 0 \land hmac_{p_s} = 0)$} + \State $s_l \gets GetLastS(sl_l)$ + \If {$(s_s > s_l + 1) \land (hmac_{p_{stored}} \neq hmac_{p_s})$} + \State \Call{Error}{'Invalid previous HMAC value'} + \EndIf + \EndIf + \If{$Hmac(Dat_s,SK) \neq GetCurrHmac(Dat_s)$ } + \State \Call{Error}{'Invalid current HMAC value'} + \EndIf + \State $hmac_{p_s} \gets Hmac(Dat_s,SK)$\Comment{Update $hmac_{p_s}$ for next check} +\State \Return{$hmac_{p_s}$} +\EndFunction +\end{algorithmic} + \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, type(de_s) = ``kv"\}$ -\ForAll{$de_s \in DE_s$} +\State $DE_{s_{kv}} \gets \{de_s | de_s \in DE_s \land IsKV(de_s)\}$ +\ForAll{$de_s \in DE_{s_{kv}}$} \State $kv_s \gets GetKV(de_s)$ \State $LV_s \gets \Call{UpdateKVLivEnt}{LV_s,kv_s,s_s}$ \State $k_s \gets GetKey(kv_s)$ @@ -481,22 +509,24 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s \If{$s_g \neq s_{g_{in}}$} \State \Call{Error}{'Invalid sequence number'} \EndIf + \State $hmac_{p_g} \gets \Call{ValidateHmacChain}{Dat_g,s_g,hmac_{p_g},sl_{last}}$ + +% \State $hmac_{p_{stored}} \gets GetPrevHmac(Dat_g)$ +% \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 +% \If{$Hmac(Dat_g,SK) \neq GetCurrHmac(Dat_g)$ } +% \State \Call{Error}{'Invalid current HMAC value'} +% \EndIf +% \State $hmac_{p_g} \gets Hmac(Dat_g,SK)$\Comment{Update $hmac_{p_g}$ for next check} + \State $DE_g \gets GetDatEnt(Dat_g)$ - \State $hmac_{p_{stored}} \gets GetPrevHmac(Dat_g)$ - \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 - \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} \State $qs_g \gets \Call{GetQueSta}{DE_g}$\Comment{Handle qs} \If{$qs_g \neq \emptyset \land qs_g > max_g$} \State $max_g \gets qs_g$ \EndIf %Check for last s in Dat - \State $id_g \gets GetMacId(Dat_g)$\Comment{Handle last s} - \State $MS_g \gets \Call{UpdateLastSeqN}{id_g,s_g,MS_g}$ + \State $MS_g \gets \Call{UpdateLastSeqN}{id_g,s_g,MS_g}$\Comment{Handle last s} %Check for last s in DE in Dat \State $DE_{g_{ss}} \gets \Call{GetSlotSeq}{DE_g}$\Comment{Handle ss} \If{$DE_{g_{ss}} \neq \emptyset$} @@ -555,9 +585,11 @@ $MaxSMSeqN(SM_s)= s$ \textit{such that} $\tuple{s, id} \in SM_s \textit{$cs_g$ = counter of $ss \in SS$ for getting pairs (initially 0)} \\ \textit{$cc_p$ = counter of $cr \in CR$ for putting pairs (initially 0)} \\ \textit{$cc_g$ = counter of $cr \in CR$ for getting pairs (initially 0)} \\ -\textit{$hmac_{c_p}$ = the HMAC value of the current slot} \\ +\textit{$hmac_{c_p}$ = the HMAC value of the current slot in procedure +$\Call{PutDataEntries}{}$} \\ \textit{$hmac_{p_p}$ = the HMAC value of the previous slot -($hmac_{p_p} = \emptyset$ for the first slot)} \\ +($hmac_{p_p} = \emptyset$ for the first slot) in procedure +$\Call{PutDataEntries}{}$} \\ \textit{$id_{self}$ = machine Id of this client} \\ \textit{$sl_{last}$ = info of last slot in queue = $\tuple{s_{last},sv_{last},id_{last}}$ (initially $\emptyset$)} \\ @@ -575,9 +607,6 @@ $CreateSS(id_s,s_{s_{last}})=\tuple{id_s,s_{s_{last}}} = ss_s$ \\ $CreateQS(max'_s)=qs_s$ \\ $CreateCR(s_s,id_s)=\tuple{s_s,id_s} = cr_s$ \\ $Encrypt(Dat_s,SK_s)=sv_s$ \\ -$GetLastS(sl = \tuple{s,sv,id})=s$ \\ -$GetSV(sl = \tuple{s,sv,id})=sv$ \\ -$GetID(sl = \tuple{s,sv,id})=id$ \\ $GetColSeqN(SL_s,s_s)= \tuple{s, sv}$ \textit{such that} $\tuple{s, sv} \in SL_s \wedge \forall \tuple{s_s, sv_s} \in SL_s, s = s_s$ \\ $GetKVPair(KV_s,k_s)= \tuple{ck,\tuple{k, v}}$ \textit{such that} -- 2.34.1