[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Provably Correct Crypto?
> 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
-> See: Info-Sec Heaven at URL http://all.net
Management Analytics - 216-686-0090 - PO Box 1480, Hudson, OH 44236