From: tcmay@sensemedia.net (Timothy C. May)
Date: Thu, 3 Aug 95 23:40:51 PDT
To: cypherpunks@toad.com
Subject: RSA has been proved correct
Message-ID: <ac470d240502100447cc@[205.199.118.202]>
MIME-Version: 1.0
Content-Type: text/plain



Serendipity strikes.

I was reading the logic programming/theorem proving chapter of my new
Russell and Norvig book on AI, and came across something I once knew about
but had forgotten: the Boyer-Moore theorem prover was applied to the RSA
algorithm and the correctness of it was verified. Correctness in the sense
of showing that outputs match formal specs, for all inputs.

The paper is: Boyer, R.S and Moore, J.S. (1984). Proof checking the RSA
public key encryption algorithm, "American Mathematical Monthly,"
91(3):181-189.

Now this does not mean:

- that implementations cannot have flaws, backdoors, etc.

- that larger systems which use RSA cannot have flaws, backdoors, etc.

What it says is that there is hope that formal verification of critical
modules is possible.

I can't imagine too many areas of software engineering that are more
critical to modularize and verify than crypto and digital money sorts of
things.

Huge monolithic programs are vastly more difficult--probably
intractable--to verify.

The "crypto library" project(s)--I use the plural because there have been
several such projects--are good ideas. Small modules that do one thing and
one thing only are best for building larger modules robustly.

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