changeset 310:d849315cd5b4

About calling secure functions
author Sigurd Meldgaard <stm@daimi.au.dk>
date Fri, 16 Apr 2010 09:37:34 +0200
parents 11a8086d6b0b
children 68683c9fe4f1
files provsec/paper.tex
diffstat 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