I would like to bring  to your attention the last paper by Neal Koblitz: Another Look at Automated Theorem-proving.

The history of Automated Theorem-proving goes back to Leibniz time, and is now developed in several directions. One of these includes cryptology.

In his paper Koblitz compares the results obtained by different applications of this theory to the human-mades. More specifically the author discusses three papers related, respectively, to the Full-Domain Hash signatures, to the ElGamal encryption, and to the Cramer-Shoup encryption and asks whether computer-assisted proof-writing can contribute in their security analysis.

In the first case, Koblitz points out that the general Full-Domain Hash signature scheme by Blancher and Pointcheval, which represents their main example of automated security proof, does much less than the reductionist security argument of Bellare and Rogaway from both practical and theoretical standpoints.

In the second case, the author shows how even more formalistic security proofs (as it's Nowak one) fail to notice the real-world security problems.

Finally, in the third case, Koblitz affirms, referring to Halevi's approach, that it is questionable whether a similar code-based argument represents progress towards automated theorem proving or even proof-checking.

In the conclusions, the author states that even if he doesn't discourage anyone from this approach ("as in the arts, people must be free to experiment with new ways of expressing themselves"), the term "automated theorem proving" promises a lot more than it delivers.

Comments Index (Total Messages: 0)

Post Reply
Name:	Guest
Title:
BBCode:
Comment:
Enter this security word

Powered by a Zone-H(ified) version of AkoComment 3.0!