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