Mercurial > pysmcl
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