[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: RSA has been proved correct
On Sat, 5 Aug 1995 [email protected] wrote:
> 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
The problem is that these "formal methods" are themselves unproved and,
in the general sense, unprovable. Using a computer program to verify RSA
is like using number theory to verify some proof in set theory--you may
succede, but so what? The RSA algorithm works because of some basic (and
not quite so basic) facts of number theory. Number theory is assumed in
the design of computers, of processors, of operating systems, and of
To put the question succinctly, would you trust a theorem "prover" to
verify its own accuracy?
The RSA algorithm:
Select primes p and q and an exponenet e, such that gcd(e,p-1) =
gcd(e,q-1) = 1. (In practice, we would want log_2(q) << e >> log_2(p).
Publish e and pq. Find d_1, d_2 such that d_1 and d_2 are inverses of e
in Z_p-1 and Z_q-1 respectively. A message Y (from 0 to pq-1) is
transformed into X = Y^e mod qp. When you recieve a message X, let X_1 =
X mod p and X_2 = X mod q. Let Y_1 = X_1^d_1 mod p and Y_2 = X_2^d_2 mod
q. Use the Chinese Remainder Theorem to find Z (from 0 to pq-1) such
that Z = Y_1 mod p1 and Z = Y_2 mod p2.
Theorem: Z = Y.
Let p_1 = p and p_2 = q
a) Observe that in F_p_i, (Y^e)^d_i = Y^(e*d_i) = Y^(r*(p-1)+1) =
Y^((p-1)*r) * Y= (Y^(p-1))^r * Y = 1^r * Y = Y.
b) There exist p,q,e triples.
If we let the order of our selection be p,e,q then we observe that we are
free in our selection of p, and that our selection of e is not very
constrained. ((p-1/)2 +- 1 being obvious examples). We then observe
than any arithmatic progression of integers which does not obviously
consist entirely of composites must contain an infinite number of
primes, and observe that the condition that gcd(q-1,e) = 1 defines just
such a progression.
c) The d's can be found
See Euclid's Algorithm
c) Z_pq is the (ring) direct sum of Z_p and Z_q
(Observe that the Chinese Remainder Theorem works on arbitrary ring direct
Why this excercise? Because not _one_ of the cited theorems is modern.
The only thing in this proof unknown to Fermat, Galios, Euclid, and the
Middle Age Chinese is that bit about arithmatic progressions and primes,
which may have been known to Fermat or Euclid. If I am informed that a
theorem "prover" has "verified" this theorem, then I am led to believe
that the "prover" is not obviously broken. My confidence (as an
algorithm--this is a separate issue from decryption resistance) in RSA has
_NOTHING_ to do with what some theorem "prover" may or may not have to
say about it. Such statements serve only to inform that these "provers"
are broken (if they don't like it), or that they concievably do "verify"
proofs (if they do).
OTOH, the theorems and axiom systems corresponding to these theorem
"provers" are very complex, and quite subtle at points. Plug in the
lastest attempt at Fermat's Last (as opposed to his Little) theorem, and
tell me if its good. Do the classification of finite groups. I know,
there is a 125-page attempt at the Poincare' conjecture. Try it. If
these "provers" find heretofore unobserved flaws, THEN I'll concede that
they would be useful tools in mathematics--in uncovering flaws. But they
_still_ don't "prove" that these theorems are correct. They only
convince themselves. But convincing me that I should believe them
involves convincing me that there has been no failure in the program--at
any of the levels I've previously discussed. And, by the way, this is why
the general mathematical community is still suspicious of the 4-color
theorem. In fact, the orginal "proof" contained a number of flaws.
All discovered were all easily patched, but the fact that they existed in
the first place means that we have no reason to believe that something
subtle is yet to be discovered.