### changeset 324:a6ccd7e9cd68

Extra sentence about the correctness of if-rewriting and minor typos Note that the correctness of if-rewriting is important for the UC security.
author Sigurd Meldgaard Thu, 27 May 2010 16:10:15 +0200 d6ad5a70a4c0 cd2e7b42b05b provsec/paper.tex 1 files changed, 6 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/provsec/paper.tex	Fri May 21 13:44:20 2010 +0200
+++ b/provsec/paper.tex	Thu May 27 16:10:15 2010 +0200
@@ -595,7 +595,7 @@
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 \KWD{\_thenx} (or
-    \KWD{_elsex}) and remember this renaming.
+    \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
@@ -632,6 +632,8 @@
this up to the programmer, as we do not have the infrastructure for
forbidding side-effects, but function-calls are nice to be able to
make in the branches.
+
+
%TODO: Maybe it is better to emit an error, and suggest the function call is moved before the assignment?
\subsection{Output and Timing of Operations}
We compile PySMCL into VIFF programs. VIFF uses a system of
@@ -683,7 +685,9 @@
Any if-statement with a secret condition will be rewritten, and
looping is not allowed with a secret condition, so the programs will
never branch on secret values and the players will never have to
-disagree, or be uncertain on what to do next.
+disagree, or be uncertain on what to do next. The correctness of the
+protocol thus relies on the correctness of the if-rewriting, so the
+computation of $F_P$ is equivalent to that of $P$.

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