[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