# HG changeset patch # User Sigurd Meldgaard # Date 1271154271 -7200 # Node ID e426b4d5049bc7f87a4fc50cb76639871c112fe1 # Parent e1a9ebd21a0946a6d18640103c0b17a6b9e21e6d Minor correction diff -r e1a9ebd21a09 -r e426b4d5049b provsec/paper.tex --- a/provsec/paper.tex Mon Apr 12 15:19:01 2010 +0200 +++ b/provsec/paper.tex Tue Apr 13 12:24:31 2010 +0200 @@ -50,7 +50,7 @@ \section{Concepts} Secure multi-party computation (MPC) deals with scenarios where a -number of players each possess some private data, and we want to +number of players each possess some private data, and want to compute a certain result from these data without revealing anything except for the intended result. There are numerous examples of such scenarios. Examples include Elections, Auctions, Procurement, @@ -296,6 +296,11 @@ on the data computed on, via a text-string given as input to \KWD{precondition}. +A function marked \verb|ideal_functionality| cannot be called from +functions that are not themselves marked (this is implemented in +practice by renaming them, and updating every call inside a marked +function.) + \section{Example} In this section we give a toy example demonstrating some of the ideas @@ -668,17 +673,21 @@ what is marked as \verb|result| in $P$. At all times $F_P$ will tell the adversary where in the program execution it is. -We now want to show that $pi_P$ with acces to $F$ is implementing +We now want to show that $pi_P$ with access to $F$ is implementing $F_P$. -The main thing we need to show, is that any \verb|open| that $pi_P$ -will do, can only release information (do an \verb|open|) when there +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. Also we need to show that the only parts of $pi_P$ that can -\verb|open| information are the ones that are marked by -\verb|@ideal_functionality|. +\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. %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 @@ -705,6 +714,11 @@ %(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 for determining the so called market clearing price from the bids of