From: tcmay@sensemedia.net (Timothy C. May)
Date: Tue, 1 Aug 95 11:23:03 PDT
To: Ray Cromwell <patl@lcs.mit.edu
Subject: Provably Correct Crypto?
Message-ID: <ac43be3d13021004ec3b@[205.199.118.202]>
MIME-Version: 1.0
Content-Type: text/plain


At 4:15 PM 8/1/95, Ray Cromwell wrote:

>  That's a neat metaphor, but it doesn't always apply. It shouldn't
>apply to algorithms which are primitive recursive. Elementary
>algorithms like multiprecision add, sub, multiply, divide, modmult,
>and modexp (the basis of public key encryption) are all provably
>correct and all terminate. (the basis is polynomial operators over a
>ring) It is possible to verify the implementation (assuming the
>correctness of the compiler). Now there could be a "factoring"
>trapdoor in RSA, but that's a trapdoor not in the implementation of
>PGP, but in the algorithm itself. RSA-in-4-lines-perl is probably
                                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
>provably correct.  To guard against trapdoors in PGP, you should
 ^^^^^^^^^^^^^^^^^
>verify the correctness of the PRNG, Key Generator, and that no private
>key bits or session key bits are leaked. I would suspect this could be
>difficult, but approximations could be determined to within a high
>degree of confidence.

This doesn't seem likely. I mean, doesn't "RSA-in-4-lines-of-Perl" *of
necessity* make use of external library/utility functions? Such as the "dc"
math routines for the PRNG? Part of its compactness is that it makes use of
available libraries.

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.

--Tim May

..........................................................................
Timothy C. May         | Crypto Anarchy: encryption, digital money,
tcmay@sensemedia.net   | anonymous networks, digital pseudonyms, zero
408-728-0152           | knowledge, reputations, information markets,
Corralitos, CA         | black markets, collapse of governments.
Higher Power: 2^756839 | Public Key: PGP and MailSafe available.
"National borders are just speed bumps on the information superhighway."