\documentclass{article}

\usepackage{fancyheadings}
\pagestyle{fancy}
\lhead{Free Haven Notation
\\David Molnar, Roger Dingledine}
\rhead{
The Free Haven Project
\\http://freehaven.net/}


\begin{document}

\section{Glossary of Notation}

\begin{description}
\item[``:''] Separator between ``who is sending" and %%@
``what is being sent."

\item[$A, B, C \dots$ :] Name of a servnet node, when on %%@
left hand side of separator ``:".

\item[$A_?$ :] Subscripts indicate a servnet node's %%@
status with respect to the presence or absence of a %%@
share. At this point, this reads as ``It is not known %%@
whether $A$ has the share." Which share is ``the" share %%@
is inferred from context.

\item[$A_{[ ]}$ : ] Servnet node $A$ does not have the %%@
share. 

\item[$A_{\Phi_i}$ : ] Servnet node $A$ has share $i$ of %%@
document $\Phi$. 

\item[$A_{[\Phi_i]}$ :] Servnet node $A$ does not have %%@
share $i$ of document $\Phi$, but it has a pointer to %%@
someone who might have the share.

\item[$A_{\Phi_i \cdot \Phi_j}$ :] Servnet node $A$ has share $i$ of
document $\Phi$, which is the buddy of share $j$ of the same document. 

\item[$ := $ ] Becomes known. Used in a protocol to %%@
indicate a servnet node's transition from one state %%@
regarding a share to another. For example, a node may %%@
begin in a state where it is not known if it has any %%@
shares. After being asked for a particular share, the %%@
node then either has the share or it does not. 

\item[$ | $ :] Used to indicate several possibilities; %%@
read as an ``Or." 

\item[$\rightarrow$:] ``Sends to," e.g. $A \rightarrow B$ %%@
reads as ``A sends to B."
\item[$\rightarrow^{\forall A}$ :] ``Sends to all members %%@
of $A$," where $A$ is some set of servnet nodes.

\item[``\{, \}''] Delimiters for payload of a message.

\item[$T$ :] In payload, read as holder for ``Transaction %%@
Type."
\item[$E$ :] In payload, read as holder for ``Method of %%@
Encryption." 
\item[$<\cdot>, <A>$ :] Reply block for whatever is %%@
inside. Read as ``reply block A"
\item[$\emptyset$ :] Nobody; message received from %%@
anonymous channel. 
\item[$\Phi$ :] Stands for a document.
\item[$\Phi$.key :] The public key associated with a %%@
document.
\item[$\Phi_i$ :] Share number $i$ of the document %%@
$\Phi$.

\item[$H(\cdot)$ :] Indicates a collision-resistant one-way hash function.
Used to send a description of an item without sending the entire item. 

\end{description}



\section{Document Request}

In a document request, an anonymous reader sends a %%@
message to every servnet node with a description of the %%@
document it wants and a reply block. Then every node %%@
which has shares of this document sends its shares to the reply block. 


$ \emptyset \rightarrow A_? : \{ T, \Phi.key, <B>, E \} $
$\forall A_{\Phi_i}  A_{\Phi_i} \rightarrow <B> : \{ E(\Phi_i) \} $


\section{Trading} 

Trading takes place in four steps. In the first two steps, shares are
exchanged. In the next two steps, receipts for the shares are exchanged.  
In a trade, we have node $A$ holding share $\Phi_i$ and node $B$ holding
share $\Lambda_j$ who wish to switch. 

$ A_{\Phi_i} \rightarrow B_{\Lambda_j} : \{ T_{T_1}, \Phi_i,
Description(\Lambda_j)
\}$

$ B_{\Lambda_j} \rightarrow A_{\Phi_i} : \{ T_{T_2} ,\Lambda_j, H(\Phi_i)
\}$

$A_{\Phi_i} \rightarrow B_{\Lambda_j} : \{ T_{T_3}, H(\Phi_i),
H(\Lambda_j), receipt \}$

$B_{\Phi_i} \rightarrow A_{\Lambda_j, \Phi_i} : \{ T_{T_4}, H(\Phi_i),
H(\Lambda_j), receipt \}$




\section{Buddy Update}

When a trade occurs, each share must tell its buddy about its new
location. 

\section{Buddy Check}

Now and then, a share will consult itself, realize that some time has
passed, and then attempt to verify that its buddy still exists. 


\end{document}

