### changeset 316:307d262401dc

More \verb|| -> \KWd{}
author Sigurd Meldgaard Fri, 16 Apr 2010 11:00:20 +0200 b0dcca45efbc e461d9e51c40 provsec/paper.tex 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