### changeset 307:167f43b15439

Text text text
author Sigurd Meldgaard Thu, 15 Apr 2010 12:58:55 +0200 76417e62d6f4 77802c6967b7 provsec/paper.tex 1 files changed, 21 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/provsec/paper.tex	Thu Apr 15 12:45:34 2010 +0200
+++ b/provsec/paper.tex	Thu Apr 15 12:58:55 2010 +0200
@@ -468,7 +468,9 @@

Whatever is returned by this function is considered as secret by the
program verifier, and is assumed to be internally represented in
-whatever form the underlying protocol uses for secret data.
+whatever form the underlying protocol uses for secret data. This can
+be seen as a loophole in the system allowing for the creating of new
+primitives.

\subsection{Range analysis}

@@ -681,13 +683,16 @@
is a way to simulate this output from the information $F_P$ outputs
from the $result$ instructions.

-Also we need to show that the only parts of $pi_P$ that can
-\KWD{open} information are the ones that are marked by
-\KWD{@ideal\_functionality}: The secret information can only be
-created by those functions, and they cannot be called but from within
-themselves. And they cannot pass the information on to other
-functions, so we always have that secret information is only handled
-within these, and therefore they are the only ones that can \KWD{open} it.
+Also we need to show that the only parts of $pi_P$ that can \KWD{open}
+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
+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
+the \KWD{result}.

%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
@@ -861,8 +866,13 @@

%\input references.tex

-\bibliographystyle{plain}
-\bibliography{refs}
+\section{Conclusion}
+We have described an embedded domain specific language for describing
+secure multiparty computations, and the implementation on top of the
+VIFF runtime.
+
+
+\bibliographystyle{plain} \bibliography{refs}

\begin{figure}
\centering
@@ -876,5 +886,6 @@

% Local Words (en_US): preprocessing multi preprocessor deferreds
+% Local Words (en_US): runtimes
% Local Words: MPC CACE PySMCL SMCL VIFF