Provably Correct Crypto?

[Matthew James Sheppard <Matthew.Sheppard@Comp.VUW.AC.NZ>]

The shadowy figure took form and announced "I am Dr. Frederick B. Cohen and I s
ay ...
> > I don't accept the ability to compile it myself as evidence and I
> > don't accept a summary of that source written in english prose
> 
> The reason to believe that thttpd fulfills the claims it makes is
> provided in some detail in the white paper on our server (see what's new
> under http://XXX.XXX).  A slightly more detailed version has been
> submitted for a journal article, and hopefully will appear in a year or
> two.
> 
>    [ A ton of crap which was exactly what I said I didn't want ]

I stipulated I didn't want any such garbage, I specifically said
english summaries are not acceptable and you bombard me with them.
Yet you wont accept others opinion of PGP's security, which verbal or
other wise, can only be an abstract summary.

> > You state that crypto should be poved correct and suggest a technique
> > otherwise known as formal specification.  I agree, pgp should have
> > been written in Z-specs.  If you take a course in formal specification
> > you will soon see the intractability of the technique wrt large
> > systems.
> 
> I didn't say that.  Perhaps you should review what I said before
> characterizing it.

piffle! Your words:
	"I think that this issue can generally be addressed by a divide
	and conquer strategy.  Prove that the called routines are
	correct and confined under all possible parameters, do the
	same for the calling routines, do the same for the interaction
	between them, and I think you have it."

This sounds like performing a formal analsis to me.  And you didn't
address the intractability anyway.

> I have shown (not yet proven) certain things.  A graduate student is now
> working on trying to prove the various properties I believe to be of
> interest in an automatic theorum prover he is working on.

The work in automatic theorum proving is ongoing and not limited to
your grad student or your work.

> I believe that these things are worth showing (and proving), but you
> may certainly feel free to disagree with these contentions.

I said showing by english isn't good enough, proving would be
fantastic.  I don't believe these issues reside solely with pgp and as
such you should question computability as a whole before using
"incomplete specification" in accusing one system to be flawed.
 
> > If you want prople on this list to repeat after you "I cannot be
> > certain there is no compromising bugs or backdoors in X" Then I will
> > go out on a limb and say everyone here will agree if system X is
> > sufficiently large.
> 
> I don't believe I ever asked anyone on this list to repeat anything. 
> All I did was ask questions and respond to responses to my questions.

Your tiresome repetitive question was "Why do you belive X is secure"
I herby answer exactly as above "I cannot be certain there is no
compromising bugs or backdoors in X"

--
                                          <URL:http://www.comp.vuw.ac.nz/~matt>
         __________
       .- __   / -- -\  __   .  .  .           0
      / <___> ___  |  =8'                    //\/  
    .^| _---_ /   \ =   / \                 \/\
    |o |  =  / o | |   ||  |              ... /
    =0=======0==|  |----|  |=    Another drive by shooting on
     \_\_/    \_\_/   \_\_/         the information super highway.