changeset 316:307d262401dc

More \verb|| -> \KWd{}
author Sigurd Meldgaard <stm@daimi.au.dk>
date Fri, 16 Apr 2010 11:00:20 +0200
parents b0dcca45efbc
children e461d9e51c40
files provsec/paper.tex
diffstat 1 files changed, 11 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/provsec/paper.tex	Fri Apr 16 10:55:36 2010 +0200
+++ b/provsec/paper.tex	Fri Apr 16 11:00:20 2010 +0200
@@ -161,7 +161,7 @@
 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 \KWD|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.
 
@@ -237,7 +237,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
-\KWD|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
@@ -249,7 +249,7 @@
 
 \subsection{Semantics}
 The execution of the program is initiated by evaluating the
-\KWD|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.
@@ -373,7 +373,7 @@
 partial information on the secret values could be inferred from the
 observed flow of the program.
 
-The second conditional is not rewritten because \verb|c| is not
+The second conditional is not rewritten because \KWD{c} is not
 secret.
 
 \KWD{open(a)} is a possible security breach, leaking the value of
@@ -607,13 +607,13 @@
   of straight-line assignments, we then continue the rewriting through
   these. But we only compute branch-specific values for those that are
   not synthesized.
-\item If the statement is a \verb|pass| we leave it.
+\item If the statement is a \KWD{pass} we leave it.
 \item Other statements trigger an error.
 \end{enumerate}
 The updated statements first from the \emph{then}\/ and then from the
 \emph{else}\/ branch are emitted in place of the if statement. 
 
-Now we have computed in variables suffixed with \verb|_then| the value
+Now we have computed in variables suffixed with \KWD{_then} the value
 of variables as they would be if \verb|cond|=1, and in those suffixed
 \KWD{_else} what they would be if \verb|cond|=0.
 
@@ -655,7 +655,7 @@
 to a programmer with no experience with deferred values.
 
 Therefore, in PySMCL, we rewrite the program, so a call to
-\verb|output| will block until the value is ready. This
+\KWD{output} will block until the value is ready. This
 way, the program can be written and will compute as a straight line
 program.
 
@@ -675,10 +675,10 @@
 $\pi_P$ in a hybrid model where $F$ is available.
 
 $\pi_P$ works as follows: The players follow the instructions of
-$P$. When $P$ contains an \verb|input| statement the designated player
+$P$. When $P$ contains an \KWD{input} statement the designated player
 sends input to the $F$, when the program contains computation on
 hidden values, the players ask $F$ to do it, and when $P$ contains
-\verb|output| statements the players ask $F$ to output the target
+\KWD{output} statements the players ask $F$ to output the target
 values.
 
 Any if-statement with a secret condition will be rewritten, and
@@ -716,8 +716,8 @@
 functions, and they cannot pass the information to non-analyzed
 functions (unless the user specifically asks for an
 exception). Therefore secret information can only be revealed by an
-analyzed function doing an \KWD|open|, and there will be created a
-proof burden to show the relationship between the \KWD{open}'ed value and
+analyzed function doing an \KWD{output}, and there will be created a
+proof burden to show the relationship between the \KWD{outputted}'ed value and
 the \KWD{result}.
 
 The security of the implemented protocol is now inherited from the