changeset 307:167f43b15439

Text text text
author Sigurd Meldgaard <stm@daimi.au.dk>
date Thu, 15 Apr 2010 12:58:55 +0200
parents 76417e62d6f4
children 77802c6967b7
files provsec/paper.tex
diffstat 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