Re: RSA has been proved correct

[solman@MIT.EDU]

Tim quoth:

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

Given the enormous difficulty of ensuring security in a world of
ubiquitous distributed computing, I'm as big a fan as any of formal
methods. But Tim's post hammers home the big fault of formal methods:
the possibility that people will come to rely upon them. I have
paranoid visions of people finally accepting formal methods in a decade
or so, and then becoming dependent on them... forgeting the enormous
potential for error that will always exist in such systems.

If somebody told me that intentionally letting a few violent criminals
free each year is a good idea because it would keep me on my toes, I
would think that person is an idiot. But I'm not entirely convinced that
it is a bad idea to avoid formal methods because they could breed
complacency.

Cheers,

JWS