Re: 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 ...

[ lots of purely subjective arguments that frequent alt.security.pgp ]

Frederick can you please tell me why I should belive thttpd is secure.
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 on the
basis that it has no hard link what so ever to the source.  It was
also written by the authors of thttpd.

You should find this argument hauntingly familiar.

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'm sorry, the english prose your team writes holds no extra formal
credibility over trust.  It demonstrates more study - but has not
proven security.

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.

p.s X = thttpd

--
                                          <URL:http://www.comp.vuw.ac.nz/~matt>
                 |~    |~
             |~ o|    o|
       ('<  o| 
      ,',)   
     ''<<    
     ---""---