# HG changeset patch
# User Sigurd Meldgaard
# Date 1271408633 -7200
# Node ID e461d9e51c40b5ec6afd2b9078beaad394b664a5
# Parent 307d262401dcf6e542a3684cadbf687dc3bf1ed8
open -> output
diff -r 307d262401dc -r e461d9e51c40 provsec/paper.tex
--- a/provsec/paper.tex Fri Apr 16 11:00:20 2010 +0200
+++ b/provsec/paper.tex Fri Apr 16 11:03:53 2010 +0200
@@ -105,10 +105,10 @@
only information that can be derived directly from this is ever
made available to an adversary in the real world protocol.
-A secure MPC protocol is often implemented by having
-players exchange values that are encrypted or by other means hidden,
-performing the computations on the hidden values, and opening or
-decrypting the final secret values to the appropriate players.
+A secure MPC protocol is often implemented by having players exchange
+values that are encrypted or by other means hidden, performing the
+computations on the hidden values, and opening or decrypting
+(outputting) the final secret values to the appropriate players.
VIFF is a framework implementing the primitives for doing MPC
implemented in Python, it is described in \cite{geisler10}. From our point of
@@ -271,7 +271,7 @@
obtaining their own value.
A secret value can be revealed by the \KWD{output} function, that
-returns the hidden value of its argument. If the variant opening a
+returns the hidden value of its argument. If the variant outputting a
value to a specific player is used, only for that player the function
returns a value, for other players it will return \KWD{None}.
@@ -376,14 +376,14 @@
The second conditional is not rewritten because \KWD{c} is not
secret.
-\KWD{open(a)} is a possible security breach, leaking the value of
+\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).
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.
+allowed to output it.
\section{The verifier}
@@ -419,7 +419,7 @@
possibilities:
\begin{itemize}
-\item The opening is marked as intentional, by making use of the
+\item The output is marked as intentional, by making use of the
construct \verb|result(output(e))|. This should be done when the
opened value is a part of the result that the programmer intends the
program to compute. Such openings are always considered OK.
@@ -438,17 +438,17 @@
% but the analysis cannot determine whether
%the opening is harmless.
The analysis interprets this to mean that the programmer claims the
- opening is harmless. In technical terms, this means the programmer
- claims that the opened value can be simulated with an
+ opening is harmless. This means the programmer
+ claims that the outputted value can be simulated with an
indistinguishable distribution, based only on the intended results
of the program. More concretely, this can be the case, for
- instance, if the opened value directly follows from the intended
+ instance, if the outputted value directly follows from the intended
results (but the programmer gets an efficiency improvement from
revealing the value at an earlier stage).
In such a case, the analysis will generate a warning, informing the
programmer about the proof burden that has to be carried in order
- for the opening to be proved secure, and providing as much help as
+ for the \KWD{output} to be proved secure, and providing as much help as
possible towards giving such a proof. This help can include an
overview of the intended results and a summary of the information
flow analysis. This part of the implementation is still sketchy in
@@ -524,7 +524,7 @@
``if-branching'' on a Boolean secret value into a program that
calculates both branches secretly.
\item
- Rewrite output statements,
+ Rewrite \KWD{output} calls,
so they block the computation until the opened value is ready.
\end{itemize}
We now give more details on these rewritings:
@@ -644,7 +644,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 branch on. This cannot be
+immediately after using the outputted 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,
@@ -695,11 +695,11 @@
We now want to show that $pi_P$ with access to $F$ is implementing
$F_P$.
-The main property we need to show, is that any \KWD{open} that $pi_P$
-will do, can only release information (do an \KWD{open}) when there is
+The main property we need to show, is that any \KWD{output} that $pi_P$
+will do, can only release information (do an \KWD{output}) when there is
a way to simulate this output from the information $F_P$ outputs from
the $result$ instructions, as of now the verifyer will print a proof
-burden for each \KWD{open} not directly within an \KWD{result} to show
+burden for each \KWD{output} not directly within an \KWD{result} to show
the consequences of the program.
A function marked \KWD{ideal\_functionality} should not be called from
@@ -709,7 +709,7 @@
harm.
-Also we need to show that the only parts of $pi_P$ that can \KWD{open}
+Also we need to show that the only parts of $pi_P$ that can \KWD{output}
information are the ones that are marked by
\KWD{@ideal\_functionality}: Secret information can only be created by
those functions, and they can only be called from other such
@@ -773,7 +773,7 @@
Because supply can be assumed to increase with increasing price, and demand will decrease,
we can assume the difference to be monotone, and hence we can find the
market clearing price
-by doing a binary search. This requires us to open the result of
+by doing a binary search. This requires us to output the result of
the intermediate comparisons, as arrays cannot be indexed by secret
values. This is however fine, because the result of the computation is
the intersection point, and a dishonest party getting access to the