changeset 302:c1650bcfed98

Improved citations
author Sigurd Meldgaard <stm@daimi.au.dk>
date Tue, 13 Apr 2010 13:25:21 +0200
parents 72480b185ba0
children e00232852871
files provsec/paper.tex
diffstat 1 files changed, 7 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/provsec/paper.tex	Tue Apr 13 13:14:07 2010 +0200
+++ b/provsec/paper.tex	Tue Apr 13 13:25:21 2010 +0200
@@ -443,15 +443,13 @@
 an external proof engine. Ultimately we hope that this can allow for
 (semi)automatic proof that the entire program is secure. Work has
 started to incorporate the verifier with the proof assistant Isabelle
-(\url{http://www.cl.cam.ac.uk/research/hvg/Isabelle/}), to print out
-proof burdens that can be proved formally, and then mechanically
-checked. We are using the Simpl framework
-\url{http://afp.sourceforge.net/entries/Simpl.shtml} to model
-imperative programs, and the user has to proof the existence of a
-simulating function. Still it is not clear if this can also include
-proof that the simulator works in polynomial time, this will be
-necessary to show security, but may have to be left to be done ``by
-hand''.
+\cite{nipkow02} , to print out proof burdens that can be proved
+formally, and then mechanically checked. We are intending on using the
+Simpl framework \cite{schirmer06} to model the imperative programs,
+and the user has to proof the existence of a simulating
+function. Still it is not clear if this can also include proof that
+the simulator works in polynomial time, this will be necessary to show
+security, but may have to be left to be done ``by hand''.
 
 \subsection{Functions returning secret values}
 In some applications, the input to a computation is not generated