--- a/paper/pysmcl.tex	Mon Jul 05 12:45:16 2010 +0200
+++ b/paper/pysmcl.tex	Mon Jul 05 12:55:23 2010 +0200
@@ -64,7 +64,7 @@
 language for secure multiparty computation, embedded in Python. The
 implementation includes a static verifier working with an Eclipse
 plug-in and a preprocessor for the language, allowing automatic
-verification of various security properties for programs. This work
+verification of various security properties of programs. This work
 builds on the existing prototype language SMCL\cite{damnielsen09}, and
 works on top of the VIFF framework\cite{geisler10}.
 
@@ -75,9 +75,9 @@
 
 \section{Concepts}
 Secure multiparty computation (MPC) deals with scenarios where a
-number of players each possesses some private data, and want to compute
-a certain result from these data without revealing anything, except
-for the intended result. There are numerous examples of such
+number of players each possessing some private data, and wanting to
+compute a certain result from these data without revealing anything
+except for the intended result. There are numerous examples of such
 scenarios. Examples include elections, auctions, procurements,
 benchmarking, etc.  If a completely trusted party was available, the
 problem could easily be solved by sending all input to this party and
@@ -85,21 +85,21 @@
 assumption.  A secure MPC protocol allows the players to do the
 computation securely {\em without}\/ the help of trusted parties. In
 other words, a secure protocol creates a situation that is equivalent
-to having a trusted party do the computation, without assuming such a
-party is actually available.
+to having a trusted third party do the computation, without assuming
+such a party is actually available.
 
-To understand the analysis we plan to do of PySMCL programs, it is
-important to realize that the output of the intended computation of
-course may reveal information on the inputs supplied by the
-parties. But since this was the purpose of doing the computation in
-the first place, this is not a security breach. What we are concerned
-about is whether we reveal {\em more}\/ information than necessary. As
-an example, consider two parties $A,B$ who each have a private natural
-number as input $n_A, n_B$, respectively.  Suppose they want to
-compare $n_A$, $n_B$ securely. This means the output is one bit that
-is 1 if $n_A\geq n_B$ and 0 otherwise. Now, if the result is 1 and
-$n_A=1000$, say, then $A$ knows that $0< n_B\leq 1000$, but $A$ should
-learn nothing further about $n_B$.
+To understand the analysis we do of PySMCL programs, it is important
+to realize that the output of the intended computation of course may
+reveal information on the inputs supplied by the parties. But since
+this was the purpose of doing the computation in the first place, this
+is not a security breach. What we are concerned about is whether we
+reveal {\em more}\/ information than necessary. As an example,
+consider two parties $A,B$ who each have a private natural number as
+input $n_A, n_B$, respectively.  Suppose they want to compare $n_A$,
+$n_B$ securely. This means the output is one bit that is 1 if $n_A\geq
+n_B$ and 0 otherwise. Now, if the result is 1 and $n_A=1000$, say,
+then $A$ knows that $0< n_B\leq 1000$, but $A$ should learn nothing
+further about $n_B$.
 
 We model this using the Universal Composability (UC) framework of
 Canetti \cite{canetti00}. This means that we specify exactly what
@@ -118,7 +118,7 @@
 target language that PySMCL programs will be embedded in.
 
 The goal of PySMCL is to allow programmers who are not experts in
-Cryptography or MPC to specify a desired computation to be executed
+cryptography or MPC to specify a desired computation to be executed
 securely, and to specify what data should become known to certain
 players at given times. In a nutshell, one can say that a PySMCL
 program specifies the computation that the above mentioned trusted
@@ -136,21 +136,23 @@
 MPC primitives to be expressed directly, without considering low-level
 VIFF or MPC protocol details.
 
-The Eclipse plug-in will on each file-save run the PySMCL preprocessor,
-which performs static analysis of these special sections, tracking the
-flow of secret values.  If the analysis finds potential security
-problems, it will give feedback to the programmer, possibly with some
-help towards fixing the problem, and/or help towards proving that the
-issue in question is actually not a security problem.  The program can
-be run, upon loading of the program the preprocessing phase is run on
-each secret function. This is now still a syntactically valid Python
-program that can be executed using the VIFF framework.
+The Eclipse plug-in will run the PySMCL preprocessor every time the
+file is saved, which performs static analysis of these special
+sections, tracking the flow of secret values.  If the analysis finds
+potential security problems, it will give feedback to the programmer,
+possibly with some help towards fixing the problem, and/or help
+towards proving that the issue in question is actually not a security
+problem.  The program can be run, upon loading of the program the
+preprocessing phase is run on each secret function. This is now still
+a syntactically valid Python program that can be executed using the
+VIFF framework.
 
 In order to allow real execution of the program by all players
 concurrently, a configuration file must also be written and supplied
 to the VIFF runtime. This file specifies where the players will be
-located (e.g., their IP-numbers). A wrapper script is included that
-eases setting up the run-time and loading the configuration files.
+located (e.g., their IP-numbers). A wrapper script is included with
+PySMCL that eases setting up the run-time and loading the
+configuration files.
 
 \section{The language}
 The language is syntactically a restrictive subset of Python for which
@@ -189,7 +191,6 @@
       \nt{P} &::=& $\overline{\nt{d}}$ &\mbox{\rm program}\\ \\
 
       \nt{d} &::=& \KWD{def} \VAR{f}($\overline{\VAR{x}}$): \nt{S} &\mbox{\rm method definition}\\ \\
-      \\ \\
 
       \nt{S} &::=& pass & \mbox{\rm NOP}\\
       &$\mid$ & \VAR{x} = \nt{e} &\mbox{\rm assignment}\\
@@ -245,11 +246,11 @@
 detail.
 
 \subsection{Semantics}
-The execution of the program is initiated by evaluating the
-\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.
+The execution of the program is initiated by evaluating the \KWD{main}
+function. The main function should not return anything, but rather
+print or otherwise communicate the result of the computation to the
+player. The semantics are like those of Python. Local variables are
+introduced by assigning to them first time.
 
 Secret values can be introduced by \KWD{random}, \KWD{random\_bit} and
 \KWD{input}. Random values are unknown to all players.
@@ -376,7 +377,7 @@
 \KWD{output(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).
+result. (In this case the burden cannot be fulfilled).
 
 Opening \KWD{max} using the \KWD{result} function is interpreted as
 if this is an intended result of the computation, it is therefore
@@ -465,8 +466,8 @@
 \cite{schirmer06} to model the imperative programs, and the user has
 to prove the existence of a simulating function. Still it is not clear
 if this can also include proof that the simulator works in polynomial
-time, this will be necessary to show security, but may have to be left
-to be done ``by hand''.
+time, this would be necessary to formally show security, but may have
+to be left to be done ``by hand''.
 
 An important difference from the work on SMCL is the way we handle the
 information that is released from ``out'' statements. Where in SMCL an
@@ -647,7 +648,7 @@
 \subsection{Output and Timing of Operations}
 We compile PySMCL into VIFF programs. VIFF uses a system of
 ``deferreds'' to give the impression of programming a synchronous
-machine, but doing as much work in parallel as possible (see D4.3 for
+machine, but doing as much work in parallel as possible (see \cite{geisler10} for
 details). The result of any computation involving secret shared values
 is a deferred, that deferred can be used again in new computations
 giving new deferreds.
@@ -756,30 +757,14 @@
 perfect security based on the GMW87-protocol, and a cryptographic
 runtime with self-trust. %TODO cite properly
 
-%Givet semantikken af sproget burde det være indlysende hvad
-%protokollen gør: spillerne kører gennem P (i hovedet så et sige), de sender input til F når P indeholder
-%en input kommando, vi beder om de aritmetiske operationer der er i P, og beder F om
-%output når vi kommer til en output komando i P. Mht kontrolflow tror jeg vi skal antage
-%at det der udføreres er programmet som det ser ud efter omskrivning (af if statements f.eks.).
-
-%Dernæst definerer vi en ny funktionalitet F_P som kan alt det F kan,
-% men den har en ny kommando P man kan kalde. Når den udføres, kører
-% funktionaliteten P, den forventer input der hvor P forventer det,
-% *men* den sender kun det output ud der er defineret som result.
-% Derudover holder den undervejs adversary orienteret om hvor den er
-% henne i kontrol flowet.  Dette skal modellere at vi i den virkelige
-% verden ikke kan skjule for fjenden hvor vi er henne i programmet.
-% 
-%Ideen skulle så være at vise en sætning der siger at under visse betingelser, så implementerer
-%\pi_P (med adgang til F) funktionaliteten F_P.
-% 
-%Betingelserne er vel så at P compiler, at der findes beviser for at alle åbninger der ikke er
-%resultater er OK, og at alle dele af P der gør noget potentielt farligt faktisk er markeret med
-%@ideal_functionality.
-% 
-%Bemærkning; hvis vi siger at det F_P gør er at udføre P som det ser ud inden omskrivninger
-%(af if's), så vil beviset automatisk skulle indeholde et bevis for at omskrivningen af if's på
-%hemmelige værdier er OK.
+\begin{figure}[htbp]
+  \centering
+  \includegraphics[width=0.5\linewidth]{uc}
+  \caption{For the computation to be secure, no adversary must be able
+    to distinguish between communicating with the simulator and
+    communicating with the real protocol running on top of the ideal
+    runtime.}
+\end{figure}
 
 
 \section{Example: Binary Search in Auctions}