Provably Correct Crypto?

[Nathan Zook]

On Tue, 1 Aug 1995, Dr. Frederick B. Cohen was alleged to have blathered:

> Tim May mused:

> > Anything that "reaches out" to external libraries or utilities would then
> > have the vulnerabilities of _those_ libraries and utilities, which may or
> > may not be provably correct themselves. (And the issue of any PRNG being
> > probably correct or not is of course an interesting, and deep, question.)
> > 
> > I do think the issues of modular design and provable correctness--or
> > approximations to it--are interesting ones.
> 
> 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 is pretty easy for one or two routines, but when you take
> the OS into account, the C compiler into account, the program itself
> into account, and the external environment into account, you run into
> some serious limitations.  For example, you may (in some cases) have to
> show that under all possible sequences of interrupt timings and stack
> conditions, the system operates correctly (which almost none currently
> do).  Unless you design with this sort of thing in mind, it's very hard
> to demonstrate these properties even for limited subproblems. 
> 

After all your griping over PGP, you spout this?  Have you ever heard of 
Godel's theorem?  I have a phrase for people who peddle their mark of 
approval that a given large program will work: "Snake oil salesman".  In 
the messages which you have scrawled between this and the last on my 
system when I caught up this evening, you have demonstrated the 
fraudulent nature of your business by first claiming that certain 
propositions were "demonstrated", then stating that a graduate student 
was working on "proving" them.

I repeat: Snake Oil Salesman

<PLONK>