Mercurial > pysmcl
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