1995-08-01 - Re: Provably Correct Crypto?

Header Data

From: Matthew James Sheppard <Matthew.Sheppard@Comp.VUW.AC.NZ>
To: fc@all.net (Dr. Frederick B. Cohen)
Message Hash: 3700c5b9d177f204133d9f39217d572ad44612c018e6e977d405555e1631b6d8
Message ID: <199508012259.KAA16027@bats.comp.vuw.ac.nz>
Reply To: <9508011911.AA11465@all.net>
UTC Datetime: 1995-08-01 22:59:57 UTC
Raw Date: Tue, 1 Aug 95 15:59:57 PDT

Raw message

From: Matthew James Sheppard <Matthew.Sheppard@Comp.VUW.AC.NZ>
Date: Tue, 1 Aug 95 15:59:57 PDT
To: fc@all.net (Dr. Frederick B. Cohen)
Subject: Re: Provably Correct Crypto?
In-Reply-To: <9508011911.AA11465@all.net>
Message-ID: <199508012259.KAA16027@bats.comp.vuw.ac.nz>
MIME-Version: 1.0
Content-Type: text/plain

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

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

                 |~    |~
             |~ o|    o|
       ('<  o|