# HG changeset patch
# User Sigurd Meldgaard <stm@daimi.au.dk>
# Date 1271329479 -7200
# Node ID 77802c6967b744c6dcfdc77b29cb9541390821c6
# Parent  167f43b1543974524add49d9403e842fe186fb8e
Security

diff -r 167f43b15439 -r 77802c6967b7 provsec/paper.tex
--- a/provsec/paper.tex	Thu Apr 15 12:58:55 2010 +0200
+++ b/provsec/paper.tex	Thu Apr 15 13:04:39 2010 +0200
@@ -679,9 +679,11 @@
 $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 a way to simulate this output from the information $F_P$ outputs
-from the $result$ instructions.
+will do, can only release information (do an \KWD{open}) 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
+the consequences of the program.
 
 Also we need to show that the only parts of $pi_P$ that can \KWD{open}
 information are the ones that are marked by
@@ -694,6 +696,15 @@
 proof burden to show the relationship between the \KWD{open}'ed value and
 the \KWD{result}.
 
+The security of the implemented protocol is now inherited from the
+primitives of the runtime. Because they are proven to be UC-secure and
+release no data at all, any composition of them will have the same
+property.
+
+In VIFF there exists several different runtimes with different
+security and performance characteristics with respect to correctness,
+passive/active security, termination etc.
+
 %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
@@ -719,10 +730,6 @@
 %(af if's), så vil beviset automatisk skulle indeholde et bevis for at omskrivningen af if's på
 %hemmelige værdier er OK.
 
-The security of the implemented protocol is thus inherited from the
-primitives of the runtime. In VIFF there exists several different
-runtimes with different security characteristics with respect to
-correctness, passive/active security, termination etc.
 
 \section{Example: Binary Search in Auctions}
 A known example of secure multi-party computation used in practice is