2007/401: Deus ex Machina?
Posted by: ShaiHalevi
Date: 22 October 2007 20:05
In his latest article, Koblitz decries those naive cryptographers who "hope that a suitably designed device --- some cleverly written computer code --- will make unpleasant natural phenomena go away."
Call me naive, but I think that the main use of computers is to eliminate unpleasantnesses: Whenever you are faced with a task that requires keeping track of many simple details, it is only natural to consider "some cleverly written computer code" to do this work for you. I am guessing that Koblitz wrote this article using a word processor, a "cleverly written computer code" that helps eliminating the unpleasantness of manual typesetting.
Let me begin with a small comment: Koblitz quotes out of context a partial sentence from my ePrint note from a few years ago, regarding the reason that some published proofs have errors in them. The entire quote reads as follows:
"Some of the reasons for this problem are social (e.g., we mostly
publish in conferences rather than journals), but the true cause of
it is that our proofs are truly complex. After all, the objects that
we deal with are non-trivial algorithms, and what we try to prove
are some properties of an intricate interaction between a few of
Koblitz omitted the part about "the true cause". Indeed, the part that was omitted is more important than what was quoted: cryptographic proofs are complex mostly because they involve keeping track of an enormous number of details (most of them rather boring). I may be naive, but I would really want "some cleverly written computer code" to help me keep track of them.
On a more technical level, Koblitz completely missed the point of the work that is done in automated/computer-aided cryptographic proofs. Specifically, he writes that
"the hope of authors of recent papers on automated theorem proving
is to take the uncertainties, flaws, and human foibles out of the
process of deriving reductionist security arguments."
I seriously doubt that there is anyone working on automated proofs that has this view. We cannot even "take the uncertainties, flaws, and human foibles out of the process" of writing an essay (even with our clever word-editors), certainly we cannot hope to do so with mathematical proofs.
Instead, the hope is that computer programs can help with the task of checking the "obvious details" of a proof, making sure that there are no errors there. Errors in published proofs are often contained in exactly these "obvious details" (see the OAEP case for example), and computer software may help avoiding such errors. As I wrote in that ePrint note:
"cryptographic proofs have a creative part (e.g., describing the
simulator or the reduction) and a mundane part (e.g., checking that
the reduction actually goes through). It often happens that the
mundane parts are much harder to write and verify, and it is with
these parts that we can hope to have automated help."
Koblitz'es article consists of a few examples from the literature, where he demonstrates that proofs that can be checked by computers are all "obvious". However, contrary to his claim, this does not show that they have no value. Quite the contrary, they demonstrate that these "obvious" steps are simple enough to be checked by a computer, thus lending support to the hope that we may one day have a computer program that can actually be helpful in writing/verifying our proofs.
To be sure, none of the code written so far can really be used by cryptographers when writing their proofs. But the recent work of Blanchet and Pointcheval clearly demonstrates that a "truly useful" program is technically doable. Most of the arguments, transformations, and tools that we use in our proofs are re-used over and over again in many different analyses, and Blanchet and Pointcheval demonstrated that these can indeed be formally expressed and used by a computer program. The challenge in creating a "truly useful" program lies essentially in assembling enough of them and devising a suitable user interface.
Edited 1 time(s). Last edit at 24-Oct-2007 12:59 by ShaiHalevi.