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