changeset 278:8d5c7032e4cd

provsec: added ivans mail about the UC-framework
author Sigurd Meldgaard <stm@daimi.au.dk>
date Thu, 11 Mar 2010 12:43:28 +0100
parents 1295cec4a287
children 8876d40c68bd
files provsec/paper.tex
diffstat 1 files changed, 28 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/provsec/paper.tex	Thu Mar 11 11:15:51 2010 +0100
+++ b/provsec/paper.tex	Thu Mar 11 12:43:28 2010 +0100
@@ -526,7 +526,35 @@
 be output before execution can continue, then it pays off to collect
 them and wait for all of them at the same time. 
 How to approximate this (which cannot be done in the current version) is left for future work.
+\section{Security in the UC model}
 
+One way to think of the runtime is as an ideal functionality $F$ that can recieve inputs from the players, evaluate arithmetic circuits on its internal memory and output results. All of this when asked to do it by honest players.
+
+Running a pySMCL program $P$ corresponds to executing the protocol $\pi_P$ in a hybrid model where $F$ is available.
+
+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
+output når vi kommer til en output komando i P. Mht kontrolflow tror jeg vi skal antage
+at det der udføreres er programmet som det ser ud efter omskrivning (af if statements f.eks.).
+
+Dernæst definerer vi en ny  funktionalitet F_P som kan alt det F kan, men den har en ny
+kommando P man kan kalde. Når den udføres, kører funktionaliteten P, den forventer input
+der hvor P forventer det, *men* den sender kun det output ud der er defineret som result.
+Derudover holder den undervejs adversary orienteret om hvor den er henne i kontrol flowet.
+Dette skal modellere at vi i den virkelige verden ikke kan skjule for fjenden hvor vi er henne
+i programmet.
+
+Ideen skulle så være at vise en sætning der siger at under visse betingelser, så implementerer
+\pi_P (med adgang til F) funktionaliteten F_P.
+
+Betingelserne er vel så at P compiler, at der findes beviser for at alle åbninger der ikke er
+resultater er OK, og at alle dele af P der gør noget potentielt farligt faktisk er markeret med
+@ideal_functionality.
+
+Bemærkning; hvis vi siger at det F_P gør er at udføre P som det ser ud inden omskrivninger
+(af if's), så vil beviset automatisk skulle indeholde et bevis for at omskrivningen af if's på
+hemmelige værdier er OK.
 
 \section{Example: Binary Search in Auctions}
 A known example of secure multi-party computation used in practice is