From: fc@all.net (Dr. Frederick B. Cohen)
Date: Mon, 7 Aug 95 05:54:43 PDT
To: cypherpunks@toad.com
Subject: Re: There's a hole in your crypto...
In-Reply-To: <9508070918.AA19988@cs.umass.edu>
Message-ID: <9508071253.AA10347@all.net>
MIME-Version: 1.0
Content-Type: text


> No crypto/privacy relevance, delete or flame now....
...
> Now, Rice's Theorem says that all non-trivial properties of TMs are undecidable.
> If I pick a "non-trivial" property, I can't conceivably build a TM ("write a
> program", if you like) that, upon input of the specification of an arbitrary TM,
> can tell whether or not that TM exhibits the property I picked. This does not
> mean that I can't decide whether some particular TMs have that property or not --
> I can. I just can't write down a procedure that handles the general case.
> 
> Also, this theorem clearly hinges on the meaning of "trivial". From what I've
> seen, a very strict interpretation is largely appropriate; nearly everything
> except the least exciting of trivial low-level properties of TMs seems to come
> out to be "non-trivial" in this regard. The proof of the theorem is more
> precise about this, naturally, but I've found this useful as a working
> colloquial definition.

Issue 1:

Undecidable for arbitrary programs does not mean undecidable for every
program.  For all finite programs with finite input sequences, all
properties are decidable.  Complexity may make proofs for large programs
infeasible at this time, but that is all.

Now back to the point of the discussion.  For certain classes of
programs, we can prove many things that are relevant to information
protection.  Furthermore, as we attempt these proofs, we may find and
fix the program anomolies (i.e., bugs) that would cause the program to
fail in an undesirable way.  Therefore, the proof techniques give us two
benefits - they help us fix the programs, and they help increase the
assurance that the programs do precisely what they are supposed to do
and nothing else.

Issue 2:

The notion that mathematics somehow excludes linguistic proofs
(forwarded I believe by a user with "may" in their email address) is
nonsense.  Mathematics at its core is based on linguistic notions that
are defined in plain language.  These notions develop a system of rules
which may be applied to decide the veracity of a proposition.  The
rules themselves form a language with syntax and semantics just as
the language that defines them has syntax and semantics.

The notion of separating language from mathematics is a fine and
interesting one, but it certainly does not apply to any mathematics
currently in widespread use.  A proof done without mathematical symbols
is no less a proof.

Issue 3:

Let's get back to the point of this discussion.  What can we really
prove about algorithms? I have made the assertion that an intersting
property for the purposes of assessing integrity, availability, and
confidentiality for servers like the W3 server and the gopher server is
the limitation of information flow.  I have backed up my assertion with
a demonstration in the form of programs that do this and English
demonstrations that that is of real value.

Does anyone disagree? Why? Is there a reason this same analytical
technique cannot be used on PGP or other cryptosystems to demonstrate
that there are no back doors (other than perhaps in the underlying
inadequacy of the overall technique)? How hard is it to do this for such
programs? What programming structures make this difficult? Will it
reveal many programming errors and therefor be a useful general purpose
tool for writing better programs?

Just thought I would stir things up a bit.

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