changeset 321:aee28074a101

provsec: Improved description of UC-proof
author Sigurd Meldgaard <stm@daimi.au.dk>
date Mon, 03 May 2010 11:22:38 +0200
parents 402cfdaa8cf7
children 2951668602d3
files provsec/paper.tex
diffstat 1 files changed, 12 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/provsec/paper.tex	Thu Apr 29 10:46:19 2010 +0200
+++ b/provsec/paper.tex	Mon May 03 11:22:38 2010 +0200
@@ -723,6 +723,18 @@
 disclose no information at all, any composition of them will have the same
 property.
 
+
+Whenever $\pi_P$ outputs information, this information is coming from
+an \KWD{output} statement (because $\pi_P$ is composed of UC-secure
+primitives releasing no information at all).
+
+A simulator for $\pi_P$ with access to $F_P$ works as follows: it runs
+$F_P$, that will output only the information marked as \KWD{result} in
+the program $P$. The simulator records this, and to simulate the
+transcript of $\pi_P$ it uses the algorithm (that was proved to exist
+by the user as a fulfillment of the proof burden) for deriving a value
+indistinguishable from the \KWD{output} from the \KWD{result}.
+
 In VIFF there exists several different runtimes with different
 security and performance characteristics with respect to correctness,
 passive/active security, termination etc. The implemented protocol