### changeset 310:d849315cd5b4

About calling secure functions
author Sigurd Meldgaard Fri, 16 Apr 2010 09:37:34 +0200 11a8086d6b0b 68683c9fe4f1 provsec/paper.tex 1 files changed, 7 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/provsec/paper.tex	Thu Apr 15 13:05:58 2010 +0200
+++ b/provsec/paper.tex	Fri Apr 16 09:37:34 2010 +0200
@@ -296,11 +296,6 @@
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
@@ -684,6 +679,13 @@
burden for each \KWD{open} not directly within an \KWD{result} to show
the consequences of the program.

+A function marked \verb|ideal_functionality| should not be called from
+functions that are not themselves marked (this is implemented in
+practice by giving them an extra parameter, the \emph{runtime}, without the
+runtime program cannot create or operate on secret values, and so cannot do
+harm.
+
+
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