From: fc@all.net (Dr. Frederick B. Cohen)
Date: Wed, 2 Aug 95 01:38:20 PDT
To: cypherpunks@toad.com
Subject: Re: Provably Correct Crypto?
Message-ID: <9508020832.AA25989@all.net>
MIME-Version: 1.0
Content-Type: text


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

The difference between my response to your question and your responses
to my questions is that I tried to answer your questions.

> > > 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."

I don't see wher I said anything about formal specification here or Z-specs.
It's true that proof of correctness for large systems is a hard problem, and
that is one of the reasons that the secure http daemon is designed to be small.
However, the same has not been shown (as far as I am aware) for many of the
other properties that may be interesting from a security standpoint.

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

Problems worthy of attack, prove their worth by fighting back - Alan Perlis

> > 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 never said it was and he is not my grad student.  He is a grad student
who made some comments on the daemons and decided he would be interested
in seeing if some of these properties could be proven.

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

And I told you that we are in the process of, but not finished with, doing
just that.  I never said that any such problems reside solely in PGP.

> > > 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"

If you are tired of hearing my responses to your comments, there is an
obvious solution.

-- 
-> See: Info-Sec Heaven at URL http://all.net
Management Analytics - 216-686-0090 - PO Box 1480, Hudson, OH 44236