changeset 320:402cfdaa8cf7

provsec: rettelser
author Sigurd Meldgaard <stm@daimi.au.dk>
date Thu, 29 Apr 2010 10:46:19 +0200
parents 7c546cb11b58
children aee28074a101
files provsec/paper.tex provsec/refs.bib
diffstat 2 files changed, 22 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/provsec/paper.tex	Fri Apr 16 11:39:31 2010 +0200
+++ b/provsec/paper.tex	Thu Apr 29 10:46:19 2010 +0200
@@ -66,7 +66,7 @@
 SMCL\cite{damnielsen09}, and works on top of the VIFF
 framework\cite{geisler10}.
 
-First we informally describe the concept of multi-party computation,
+First we informally describe the concept of multiparty computation,
 and go through the different components of PySMCL, and give an example
 of how it works. Then follows a more detailed description of the tool
 and its implementation.
@@ -77,7 +77,7 @@
 a certain result from these data without revealing anything, except
 for the intended result. There are numerous examples of such
 scenarios. Examples include elections, auctions, procurements,
-benchmarkings, etc.  If a completely trusted party was available, the
+benchmarking, etc.  If a completely trusted party was available, the
 problem could easily be solved by sending all input to this party and
 let him compute the result. This is, however, usually an unrealistic
 assumption.  A secure MPC protocol allows the players to do the
@@ -908,7 +908,7 @@
 \begin{figure}
   \centering
   \includegraphics[width=1.0\textwidth]{screenshot}
-  \caption{A screenshot of the auction program edited with the Eclipse
+  \caption{A screen shot of the auction program edited with the Eclipse
     plug-in. Two boxes with output from the tool are shown.}
   \label{screenshot}
 \end{figure}
@@ -917,6 +917,6 @@
 
 
 % Local Words (en_US): preprocessing multi preprocessor deferreds
-% Local Words (en_US): analyses runtimes
+% Local Words (en_US): Composability analyses runtimes
 % Local Words: MPC CACE PySMCL SMCL VIFF
 
--- a/provsec/refs.bib	Fri Apr 16 11:39:31 2010 +0200
+++ b/provsec/refs.bib	Thu Apr 29 10:46:19 2010 +0200
@@ -32,3 +32,21 @@
   OPTannote =    {}
 }
 
+
+@Book{nipkow02,
+  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
+  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
+  publisher	= {Springer},
+  series	= {LNCS},
+  volume	= 2283,
+  year		= 2002
+}
+
+@PhdThesis{schirmer06,
+  author = 	 {Norbert Schirmer},
+  title = 	 {Verification of Sequential Imperative Programs in {I}sabelle/{HOL}},
+  school = 	 {Technische Universit\"at M\"unchen},
+  year = 	 {2006},
+}
+
+