From: Ray Cromwell <rjc@clark.net>
Date: Tue, 1 Aug 95 12:25:27 PDT
To: tcmay@sensemedia.net (Timothy C. May)
Subject: Re: Provably Correct Crypto?
In-Reply-To: <ac43be3d13021004ec3b@[205.199.118.202]>
Message-ID: <199508011915.PAA02085@clark.net>
MIME-Version: 1.0
Content-Type: text/plain



[Tim responds to my note on "provably correct implementation"}

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

  What I meant by my message is in some circumstances, an implementation
can be proven correct (i.e. to do what it says it does correctly) What
I mean by implementation is the source at the highest level, not the
module dependencies which are abstractly disconnected from the application.
(e.g. if a multiprecision math library that comes with the operating
system is used by PGP, the source to PGP could be said to be "trapdoor free"
even if the math library has an NSA monitoring function built into it)

 Each layer of course relies on the correctness of the layer beneath it, much
like a theorem proof relies on the proof of the statements that makes it
up. Thus, RSA-in-4-lines can be observed to be a correct implementation
of RSA without any trapdoors (like secretly storing or leaking private
key bits) at the level of its source code. Of course, the Perl interpreter
itself would have to be proven correct, but we assume that no RSA trap
doors have been put into perl because perl was available long before
PGP and RSA-in-4-lines perl and is widely distributed. The probability
of a trapdoor in perl is small.


The hierarchy looks like this:

RSA-in-4-lines :: DEPENDS_ON_CORRECTNESS_OF { Perl, DC, RSA_Algorithms }

Perl :: DEPENDS_ON_CORRECTNESS_OF { C, Unix, Perl_Algorithms }
DC :: DEPENDS_ON_CORRECTNESS_OF { C, Unix, DC_Algorithms }

C :: DEPENDS_ON_CORRECTNESS_OF { C_compiler } 
C_compiler :: DEPENDS_ON_CORRECTNESS_OF { Assembler }
Assembler :: DEPENDS_ON_CORRECTNESS_OF { instruction_set }
instruction_set :: DEPENDS_ON_CORRECTNESS_OF { hardware }

Now even if it were possible to prove the correctness of all those layers
(which I find doubtful. Some kind of Goedel/Turing limitation is going to turn
up somewhere), what if the 'hardware' isn't correct. (e.g. Pentium bug)
There could be a one-in-a-zillion bug that randomly leaks keybits. 

IMHO, there's no sense in worrying about stuff like this. If your data
is so valuable that you need absolute theoretical security, use a 
one-time-pad with a simple redundant provably secure device
(also shielded from TEMPEST attacks), and have the thing implanted
in your skull. ;-)


-Ray