--- a/provsec/paper.tex	Fri Apr 16 09:42:19 2010 +0200
+++ b/provsec/paper.tex	Fri Apr 16 09:54:38 2010 +0200
@@ -138,10 +138,10 @@
 
 In order to keep the prototype implementation simple, we leave out
 quite a lot of syntactic constructs from Python, including generators,
-with-constructs, elif, augmented assignments (assignments of the form
+with-constructs, \KWD{elif}, augmented assignments (assignments of the form
 \verb|x+=1|), delete statements, global statements, try/except and
 import statements. And focus on a small While-like language. Some of
-these are easily rewritten into PySMCL (for example \verb|elif| can be
+these are easily rewritten into PySMCL (for example \KWD|elif| can be
 written into a nested if) while others complicate the data flow, and
 are left out for that reason.
 
@@ -217,7 +217,7 @@
 commas should be present or not. It is presented in
 figure~\ref{fig:corepysmcl}. A Core PySMCL program consists of a
 sequence of function declarations. A certain function called
-\verb|main| is used as the entry point of the computation.
+\KWD|main| is used as the entry point of the computation.
 
 The set of statements and expressions is similar to a standard
 while-language augmented with domain-specific operations operating on
@@ -229,7 +229,7 @@
 
 \subsection{Semantics}
 The execution of the program is initiated by evaluating the
-\verb|main| function. The main function should not return anything,
+\KWD|main| function. The main function should not return anything,
 but rather print or otherwise communicate the result of the
 computation. The semantics are like those of Python. Local variables
 are introduced by assigning to them first time.
@@ -253,7 +253,7 @@
 A secret value can be revealed by the \KWD{output} function, that
 returns the hidden value of its argument. If the variant opening a
 value to a specific player is used, only for that player the function
-returns a value, for other players it will return \verb|None|.
+returns a value, for other players it will return \KWD{None}.
 
 \section{Implementation strategy}
 We embed PySMCL in Python by using ``decorators''.  These are higher
@@ -266,13 +266,13 @@
     return 1 - a
 \end{verbatim}
 
-Here the decorator called is \verb|ideal_functionality|, a higher
-order function receiving the function \verb|negate| and returning
-another function that is then also named \verb|negate|. While deciding
+Here the decorator called is \KWD{ideal_functionality}, a higher
+order function receiving the function \KWD{negate} and returning
+another function that is then also named \KWD{negate}. While deciding
 what output function to return, it may of course the values of its own
-arguments (here the values of \verb|secret| and \verb|range|).
+arguments (here the values of \KWD{secret} and \KWD{range}).
 
-We use the \verb|inspect| module from Python, so the decorator can get
+We use the \KWD{inspect} module from Python, so the decorator can get
 access to the source code and thereby the parse tree of the decorated
 function, and make analyses and changes before rewriting it.
 
@@ -322,11 +322,11 @@
     return result(output(max))
 \end{verbatim}
 
-The function \verb|f| above is marked as an ideal functionality, and
+The function \KWD{f} above is marked as an ideal functionality, and
 therefore subject to preprocessing and verification.
 
-The variables \verb|a| and \verb|b| are marked as secret by the
-\verb|secrets| argument to \verb|ideal_functionality|.
+The variables \KWD{a} and \KWD{b} are marked as secret by the
+\KWD{secrets} argument to \KWD{ideal_functionality}.
 
 % The variable \verb|c| is marked secret because it is the result of a
 % call to \verb|Secret|. Of course the value 42 is public, since it
@@ -338,7 +338,7 @@
 allowed, moreover calls to other verified functions with secret values
 in the right places are also allowed.
 
-\verb|bigger| is a secret value since it is derived from secret
+\KWD{bigger} is a secret value since it is derived from secret
 values. It can be inferred to contain a Boolean value because it is
 the result of a comparison.
 
@@ -356,10 +356,12 @@
 The second conditional is not rewritten because \verb|c| is not
 secret.
 
-\verb|open_a| is a possible security breach, leaking the value of
-\verb|a|, and therefore generating an error message from the analysis.
+\KWD{open(a)} is a possible security breach, leaking the value of
+\KWD{a}, and therefore causes the generation of a proof burden from
+the analysis that a can be derived from the public values and the
+result. (In this case the burden cannot be proven).
 
-Opening \verb|max| using the \verb|result| function is interpreted as
+Opening \KWD{max} using the \KWD{result} function is interpreted as
 if this is an intended result of the computation, it is therefore
 allowed to open it.
 
@@ -386,7 +388,7 @@
   %  variable $b$ in the above example).
 \item Range analysis, keeping track of the intervals which we can
   guarantee variables to be in. This is especially convenient for
-  Boolean values (such as the variable $bigger$ in the above example).
+  Boolean values (such as the variable \KWD{bigger} in the above example).
 \end{itemize}
 
 The feedback from the verifier to the programmer is used to alert the
@@ -412,7 +414,7 @@
   %   of random values is not implemented yet, as it is still unclear
   %   how the general rules should look.
 \item
-  The opening is done using the \verb|output| function.
+  The opening is done using the \KWD{output} function.
   % but the analysis cannot determine whether
   %the opening is harmless.
   The analysis interprets this to mean that the programmer claims the
@@ -516,9 +518,9 @@
 branch.
 
 This is done recursively, with the innermost statements first, to
-allow for nested \verb|if|-statements.
+allow nested \KWD{if}-state\-ments.
 
-As this rewrite often will make more variables depend on secret values
+As this rewrite often will make even more variables depend on secret values
 we afterwards repeat the analysis and possibly this operation until a
 fixpoint is reached.
 
@@ -560,7 +562,7 @@
 \end{verbatim}
 
 Notice that we need to take special care that the temporary variables
-\verb|a_then0|, \verb|cond0| etc.\ are \emph{not}\/ combined in the second step,
+\KWD{a_then0}, \KWD{cond0} etc.\ are \emph{not}\/ combined in the second step,
 as they will never by used outside the transformed if.
 
 Here follows a description of the algorithm used for the rewrite:
@@ -573,8 +575,8 @@
     invocation of the procedure we do not need it outside this branch,
     and nothing needs to be changes, so we leave it in place.
   \item Otherwise, if we have not assigned to this variable before; we
-    suffix the assigned variable name with a fresh \verb|_thenx| (or
-    \verb|_elsex|) and remember this renaming.
+    suffix the assigned variable name with a fresh \KWD{_thenx} (or
+    \KWD{_elsex}) and remember this renaming.
   \item If we have assigned to this variable before in the same branch
     we reuse the same name as last time.
   \item All variables on the right-hand side that have been renamed in
@@ -593,7 +595,7 @@
 
 Now we have computed in variables suffixed with \verb|_then| the value
 of variables as they would be if \verb|cond|=1, and in those suffixed
-\verb|_else| what they would be if \verb|cond|=0.
+\KWD{_else} what they would be if \verb|cond|=0.
 
 Finally we emit statements for obliviously combining the values of the
 variables of the two branches. These are one assignment for each
@@ -603,7 +605,7 @@
 
 \verb|a = a_else + (a_then - a_else) * cond|
 
-Because the range-analysis guarantees us that \verb|cond| is in $\{0,1\}$ this will give the right value of a.
+Because the range-analysis guarantees us that \KWD{cond} is in $\{0,1\}$ this will give the right value of a.
 
 One subtlety is that function calls are made no matter what the
 condition was, this might give counter-intuitive results, because
@@ -622,7 +624,7 @@
 
 When revealing a secret value in VIFF, we get back a deferred, but
 often we want to output the value, and write an if statement
-immediately after using the opened value to brach on. This cannot be
+immediately after using the opened value to branch on. This cannot be
 done in plain VIFF, because we do not know if the value to be opened is
 ready when we do the branching.  Therefore a common idiom when writing
 VIFF code is to put the code doing the branch in a callback-function,
@@ -667,7 +669,7 @@
 Now we define a functionality $F_P$, working just as $F$, but it has a
 new command $P$ that, when called, makes the functionality run the
 program $P$ --- taking inputs when $P$ would, outputting \emph{only}
-what is marked as \verb|result| in $P$. At all times $F_P$ will tell
+what is marked as \KWD{result} in $P$. At all times $F_P$ will tell
 the adversary where in the program execution it is.
 
 We now want to show that $pi_P$ with access to $F$ is implementing
@@ -895,6 +897,6 @@
 
 
 % Local Words (en_US): preprocessing multi preprocessor deferreds
-% Local Words (en_US): runtimes
+% Local Words (en_US): analyses runtimes
 % Local Words: MPC CACE PySMCL SMCL VIFF